SymbLocksDomain.ILockIndex-based symbolic lock
module Idx : sig ... endIndex in index-based symbolic lock
include sig ... endtype t =
AddressDomain.AddressBase(Mval.MakePrintable(Offset.MakePrintable(Idx))).t =
| Addr of Mval.MakePrintable(Offset.MakePrintable(Idx)).t| NullPtr| UnknownPtr| StrPtr of StringDomain.tval hash : t -> intval show : t -> stringval pretty : unit -> t -> Printable.Pretty.docval printXml : 'a BatInnerIO.output -> t -> unitval to_yojson : t -> Yojson.Safe.tval tag : t -> intval arbitrary : unit -> t QCheck.arbitraryval of_string : string -> tval to_string : t -> string optionval to_c_string : t -> string optionval to_n_c_string : int -> t -> string optionval to_string_length : t -> int optionval is_definite : t -> boolval add_offset :
t ->
Mval.MakePrintable(Offset.MakePrintable(Idx)).idx Offset.t ->
tval of_var : GoblintCil.varinfo -> tval to_var : t -> GoblintCil.varinfo optionval to_var_may : t -> GoblintCil.varinfo optionval to_var_must : t -> GoblintCil.varinfo optionval to_mval : t -> Mval.MakePrintable(Offset.MakePrintable(Idx)).t optionval to_exp : t -> GoblintCil.expval type_of : t -> GoblintCil.typval conv_const_offset :
GoblintCil.offset ->
[> `Field of GoblintCil.fieldinfo * 'a | `Index of Idx.t * 'a | `NoOffset ] as 'aval of_mval : (GoblintCil.varinfo * GoblintCil.offset) -> t