module Cil_const:sig
..end
Smart constructors for some CIL data types
val voidType : Cil_types.typ
module CurrentLoc:State_builder.Ref
with type data = location
forward reference to current location (see Cil.CurrentLoc
)
module Vid:sig
..end
val set_vid : Cil_types.varinfo -> unit
set the vid to a fresh number.
val copy_with_new_vid : Cil_types.varinfo -> Cil_types.varinfo
returns a copy of the varinfo with a fresh vid. If the varinfo has an associated logic var, a copy of the logic var is made as well.
val change_varinfo_name : Cil_types.varinfo -> string -> unit
change_varinfo_name vi name
changes the name of vi
to name
. Takes
care of renaming the associated logic_var if any.
val new_raw_id : unit -> int
Generate a new ID. This will be different than any variable ID
that is generated by Cil.makeLocalVar
and friends.
Must not be used for setting vid: use Cil_const.set_vid
instead.
val make_logic_var_kind : string ->
Cil_types.logic_var_kind -> Cil_types.logic_type -> Cil_types.logic_var
Create a fresh logical variable giving its name, type and origin.
val make_logic_var : string -> Cil_types.logic_type -> Cil_types.logic_var
kind
function below, or Cil.cvar_to_lvar
Create a fresh logical variable giving its name and type.
val make_logic_var_global : string -> Cil_types.logic_type -> Cil_types.logic_var
Create a new global logic variable
val make_logic_var_formal : string -> Cil_types.logic_type -> Cil_types.logic_var
Create a new formal logic variable
val make_logic_var_quant : string -> Cil_types.logic_type -> Cil_types.logic_var
Create a new quantified logic variable
val make_logic_var_local : string -> Cil_types.logic_type -> Cil_types.logic_var
Create a new local logic variable
val make_logic_info : string -> Cil_types.logic_info
Create a fresh logical (global) variable giving its name and type.
val make_logic_info_local : string -> Cil_types.logic_info
Create a new local logic variable given its name.