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
module Sid:sig
..end
module Eid: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 mkCompInfo : bool ->
string ->
?norig:string ->
(Cil_types.compinfo ->
(string * Cil_types.typ * int option * Cil_types.attributes *
Cil_types.location)
list) ->
Cil_types.attributes -> Cil_types.compinfo
Creates a (potentially recursive) composite type. The arguments are: (1) a boolean indicating whether it is a struct or a union, (2) the name (always non-empty), (3) a function that when given a representation of the structure type constructs the type of the fields recursive type (the first argument is only useful when some fields need to refer to the type of the structure itself), and (4) a list of attributes to be associated with the composite type. The resulting compinfo has the field "cdefined" only if the list of fields is non-empty.
val copyCompInfo : ?fresh:bool -> Cil_types.compinfo -> string -> Cil_types.compinfo
Makes a shallow copy of a Cil_types.compinfo
changing the name. It also
copies the fields, and makes sure that the copied field points back to the
copied compinfo.
If fresh
is true
(the default), it will also give a fresh id to the
copy.
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.