Module Cil_const

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
Deprecated.Fluorine-20130401 You should use a specific make_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.