Module `ValueDomain.Offs`

type t = (Cil.fieldinfo, IndexDomain.t) Lval.offs

type group = Printable.Std.group = |

val show_group : group -> 'a

val to_group : 'a -> 'b option

val trace_enabled : bool

val invariant : 'a -> 'b -> Invariant.t

val tag : 'a -> 'b

val arbitrary : unit -> 'a

val relift : 'a -> 'a

val is_first_field : CilType.Fieldinfo.t -> bool

val cmp_zero_offset : t -> [ `MayZero | `MustNonzero | `MustZero ]

val equal : t -> t -> bool

val show : 
  [< `Field of Cil.fieldinfo * 'a | `Index of IndexDomain.t * 'a | `NoOffset ] as 'a ->
  string

val pretty : 
  unit ->
  [< `Field of Cil.fieldinfo * 'a | `Index of IndexDomain.t * 'a | `NoOffset ] as 'a ->
  Pretty.doc

val pretty_diff : 
  unit ->
  ([< `Field of Cil.fieldinfo * 'a | `Index of IndexDomain.t * 'a | `NoOffset ] as 'a
   * [< `Field of Cil.fieldinfo * 'b
     | `Index of IndexDomain.t * 'b
     | `NoOffset ] as 'b) ->
  Pretty.doc

val hash : 
  [< `Field of CilType.Fieldinfo.t * 'a | `Index of 'b * 'a | `NoOffset ] as 'a ->
  int

val name : unit -> string

val from_offset : 'a -> 'a

val to_offset : 'a -> 'a list

val is_definite : 
  [< `Field of 'b * 'a | `Index of IndexDomain.t * 'a | `NoOffset ] as 'a ->
  bool

val add_offset : 
  [< `Field of 'b * 'a | `Index of 'c * 'a | `NoOffset ] as 'a ->
  [> `Field of 'b * 'd | `Index of 'c * 'd ] as 'd ->
  'd

val compare : 
  [< `Field of CilType.Fieldinfo.t * 'a
  | `Index of IndexDomain.t * 'a
  | `NoOffset ] as 'a ->
  [< `Field of CilType.Fieldinfo.t * 'b
  | `Index of IndexDomain.t * 'b
  | `NoOffset ] as 'b ->
  int

val leq : t -> t -> bool

val merge : [ `Join | `Meet | `Narrow | `Widen ] -> t -> t -> t

val to_cil_offset : t -> Cil.offset

val join : t -> t -> t

val meet : t -> t -> t

val widen : t -> t -> t

val narrow : t -> t -> t

val drop_ints : 
  [< `Field of 'b * 'a | `Index of 'c * 'a | `NoOffset ] as 'a ->
  [> `Field of 'b * 'd | `Index of IndexDomain.t * 'd | `NoOffset ] as 'd

val printXml : 
  'a BatInnerIO.output ->
  [< `Field of Cil.fieldinfo * 'b | `Index of IndexDomain.t * 'b | `NoOffset ] as 'b ->
  unit

val to_yojson : 
  [< `Field of Cil.fieldinfo * 'a | `Index of IndexDomain.t * 'a | `NoOffset ] as 'a ->
  [> `String of string ]

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ValueDomain/Offs/index.html

Module `ValueDomain.Offs`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ValueDomain/Offs/index.html

Module ValueDomain.Offs

Module `ValueDomain.Offs`