Module `Lval.Normal`

Parameters

module Idx : IdxDomain

Signature

type field = GoblintCil.fieldinfo

type idx = Idx.t

module Offs : sig ... end

type t =

| Addr of CilType.Varinfo.t * Offs.t
(*
Pointer to offset of a variable.
*)
| NullPtr
(*
NULL pointer.
*)
| UnknownPtr
(*
Unknown pointer. Could point to globals, heap and escaped variables.
*)
| StrPtr of string option
(*
String literal pointer. StrPtr None abstracts any string pointer
*)

val equal : t -> t -> Ppx_deriving_runtime.bool

val compare : t -> t -> Ppx_deriving_runtime.int

val hash : t -> int

include module type of struct include Printable.Std end

val trace_enabled : bool

val tag : 'a -> 'b

val relift : 'a -> 'a

val name : unit -> string

type group = Basetype.Variables.group

val show_group : Basetype.Variables.group -> Ppx_deriving_runtime.string

val to_group : t -> Basetype.Variables.group option

val from_var : CilType.Varinfo.t -> t

val from_var_offset : (CilType.Varinfo.t * Offs.t) -> t

val to_var : t -> CilType.Varinfo.t option

val to_var_may : t -> CilType.Varinfo.t option

val to_var_must : t -> CilType.Varinfo.t option

val to_var_offset : t -> (CilType.Varinfo.t * Offs.t) option

val from_string : string -> t

val to_string : t -> string option

val short_offs : 
  [< `Field of GoblintCil.fieldinfo * 'a | `Index of Idx.t * 'a | `NoOffset ] as 'a ->
  string

val short_addr : 
  (GoblintCil.varinfo
   * [< `Field of GoblintCil.fieldinfo * 'a & GoblintCil.fieldinfo * 'a
     | `Index of Idx.t * 'a & Idx.t * 'a
     | `NoOffset ] as 'a) ->
  string

val show : t -> string

include sig ... end

val pretty : unit -> t -> Goblint_lib__Printable.Pretty.doc

val printXml : 'a BatInnerIO.output -> t -> unit

val to_yojson : t -> [> `String of string ]

exception Type_offset of GoblintCil.typ * string

val type_offset : 
  GoblintCil.typ ->
  [ `Field of GoblintCil.fieldinfo * 'a | `Index of Idx.t * 'a | `NoOffset ] as 'a ->
  GoblintCil.typ

val get_type_addr : 
  (GoblintCil.varinfo
   * [ `Field of GoblintCil.fieldinfo * 'a | `Index of Idx.t * 'a | `NoOffset ] as 'a) ->
  GoblintCil.typ

val get_type : t -> GoblintCil.typ

val is_zero_offset : Offs.t -> bool

val to_exp : (idx -> GoblintCil.exp) -> t -> GoblintCil.exp

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

val add_offset : t -> Offs.t -> t

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

val arbitrary : unit -> t QCheck.arbitrary

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/Lval/Normal/index.html

Module `Lval.Normal`

Parameters

Signature

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/Lval/Normal/index.html

Module Lval.Normal

Parameters

Signature

Module `Lval.Normal`