WitnessGhost (p.goblint.2.6.0.doc.goblint.lib.Goblint

val enabled : unit -> bool

module Var : sig ... end

Ghost variables for YAML witnesses.

include module type of struct include Var end

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

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

val hash : Goblint_lib__.WitnessGhostVar.t -> int

val name_varinfo : Goblint_lib__.WitnessGhostVar.t -> string

val show : Goblint_lib__.WitnessGhostVar.t -> string

include sig ... end

val pretty : unit -> Goblint_lib__.WitnessGhostVar.t -> Printable.Pretty.doc

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

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

val typ : Goblint_lib__.WitnessGhostVar.t -> GoblintCil.typ

val initial : Goblint_lib__.WitnessGhostVar.t -> GoblintCil.exp

module Map : sig ... end

include module type of struct include Map end

type t = Var.t

type marshal = RichVarinfo.BiVarinfoMap.Make(Var).marshal

val to_varinfo : t -> GoblintCil.varinfo

val unmarshal : marshal option -> unit

val marshal : unit -> marshal

val bindings : unit -> (t * GoblintCil.varinfo) list

val from_varinfo : GoblintCil.varinfo -> t option

val mem_varinfo : GoblintCil.varinfo -> bool

val describe_varinfo : GoblintCil.varinfo -> t -> string

val variable' : 
  Goblint_lib__.WitnessGhostVar.t ->
  YamlWitnessType.GhostInstrumentation.Variable.t

val update' : 
  Goblint_lib__.WitnessGhostVar.t ->
  CilType.Exp.t ->
  YamlWitnessType.GhostInstrumentation.Update.t

val location_update' : 
  node:Node.t ->
  updates:Goblint_lib__YamlWitnessType.GhostInstrumentation.Update.t list ->
  YamlWitnessType.GhostInstrumentation.LocationUpdate.t

val instrumentation_entry : 
  task:Goblint_lib__YamlWitnessType.Task.t ->
  variables:Goblint_lib__YamlWitnessType.GhostInstrumentation.Variable.t list ->
  location_updates:
    Goblint_lib__YamlWitnessType.GhostInstrumentation.LocationUpdate.t list ->
  YamlWitnessType.Entry.t