Frama-C API - simplify_const_lval
A cilVisitor
(by copy) that simplifies expressions of the type const int x = v
, where v
is an integer and x
is a global variable. Requires a mapping from varinfo
to init option
(e.g. based on Globals.Vars.find
).
method behavior : Frama_c_kernel.Visitor_behavior.t
the kind of behavior expected for the behavior.
method project : Frama_c_kernel.Project.t option
Project the visitor operates on. Non-nil for copy visitor.
method plain_copy_visitor : Frama_c_kernel.Cil.cilVisitor
a visitor who only does copies of the nodes according to behavior
method vfile : Frama_c_kernel.Cil_types.file -> Frama_c_kernel.Cil_types.file Frama_c_kernel.Cil.visitAction
visit a whole file.
method vvdec : Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.varinfo Frama_c_kernel.Cil.visitAction
Invoked for each variable declaration. The children to be traversed are those corresponding to the type and attributes of the variable. Note that variable declarations are GVar
, GVarDecl
, GFun
and GFunDecl
globals, the formals of functions prototypes, and the formals and locals of function definitions. This means that the list of formals of a function may be traversed multiple times if there exists both a declaration and a definition, or multiple declarations.
method vvrbl : Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.varinfo Frama_c_kernel.Cil.visitAction
Invoked on each variable use. Here only the SkipChildren
and ChangeTo
actions make sense since there are no subtrees. Note that the type and attributes of the variable are not traversed for a variable use.
method vexpr : Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp Frama_c_kernel.Cil.visitAction
Invoked on each expression occurrence. The subtrees are the subexpressions, the types (for a Cast
or SizeOf
expression) or the variable use.
method vlval : Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.lval Frama_c_kernel.Cil.visitAction
Invoked on each lvalue occurrence
method voffs : Frama_c_kernel.Cil_types.offset -> Frama_c_kernel.Cil_types.offset Frama_c_kernel.Cil.visitAction
Invoked on each offset occurrence that is *not* as part of an initializer list specification, i.e. in an lval or recursively inside an offset.
method vinitoffs : Frama_c_kernel.Cil_types.offset -> Frama_c_kernel.Cil_types.offset Frama_c_kernel.Cil.visitAction
Invoked on each offset appearing in the list of a CompoundInit initializer.
method vinst : Frama_c_kernel.Cil_types.instr -> Frama_c_kernel.Cil_types.instr list Frama_c_kernel.Cil.visitAction
Invoked on each instruction occurrence. The ChangeTo
action can replace this instruction with a list of instructions
method vstmt : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.stmt Frama_c_kernel.Cil.visitAction
Control-flow statement. The default DoChildren
action does not create a new statement when the components change. Instead it updates the contents of the original statement. This is done to preserve the sharing with Goto
and Case
statements that point to the original statement. If you use the ChangeTo
action then you should take care of preserving that sharing yourself.
method vblock : Frama_c_kernel.Cil_types.block -> Frama_c_kernel.Cil_types.block Frama_c_kernel.Cil.visitAction
Block.
method vfunc : Frama_c_kernel.Cil_types.fundec -> Frama_c_kernel.Cil_types.fundec Frama_c_kernel.Cil.visitAction
Function definition. Replaced in place.
method vglob : Frama_c_kernel.Cil_types.global -> Frama_c_kernel.Cil_types.global list Frama_c_kernel.Cil.visitAction
Global (vars, types, etc.)
method vinit : Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.offset -> Frama_c_kernel.Cil_types.init -> Frama_c_kernel.Cil_types.init Frama_c_kernel.Cil.visitAction
Initializers. Pass the global where this occurs, and the offset
method vlocal_init : Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.local_init -> Frama_c_kernel.Cil_types.local_init Frama_c_kernel.Cil.visitAction
local initializer. pass the variable under initialization.
method vtype : Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cil_types.typ Frama_c_kernel.Cil.visitAction
Use of some type. For typedef, struct, union and enum, the visit is done once at the global defining the type. Thus, children of TComp
, TEnum
and TNamed
are not visited again.
method vcompinfo : Frama_c_kernel.Cil_types.compinfo -> Frama_c_kernel.Cil_types.compinfo Frama_c_kernel.Cil.visitAction
declaration of a struct/union
method venuminfo : Frama_c_kernel.Cil_types.enuminfo -> Frama_c_kernel.Cil_types.enuminfo Frama_c_kernel.Cil.visitAction
declaration of an enumeration
method vfieldinfo : Frama_c_kernel.Cil_types.fieldinfo -> Frama_c_kernel.Cil_types.fieldinfo Frama_c_kernel.Cil.visitAction
visit the declaration of a field of a structure or union
method venumitem : Frama_c_kernel.Cil_types.enumitem -> Frama_c_kernel.Cil_types.enumitem Frama_c_kernel.Cil.visitAction
visit the declaration of an enumeration item
method vattr : Frama_c_kernel.Cil_types.attribute -> Frama_c_kernel.Cil_types.attribute list Frama_c_kernel.Cil.visitAction
Attribute. Each attribute can be replaced by a list
method vattrparam : Frama_c_kernel.Cil_types.attrparam -> Frama_c_kernel.Cil_types.attrparam Frama_c_kernel.Cil.visitAction
Attribute parameters.
method queueInstr : Frama_c_kernel.Cil_types.instr list -> unit
Add here instructions while visiting to queue them to precede the current statement being processed. Use this method only when you are visiting an expression that is inside a function body, or a statement, because otherwise there will no place for the visitor to place your instructions.
method unqueueInstr : unit -> Frama_c_kernel.Cil_types.instr list
Gets the queue of instructions and resets the queue. This is done automatically for you when you visit statements.
method current_stmt : Frama_c_kernel.Cil_types.stmt option
link to the current statement being visited.
NB: for copy visitor, the stmt is the original one (use get_stmt
to obtain the corresponding copy)
method current_kinstr : Frama_c_kernel.Cil_types.kinstr
Kstmt stmt
when visiting statement stmt, Kglobal
when called outside of a statement.
method push_stmt : Frama_c_kernel.Cil_types.stmt -> unit
method pop_stmt : Frama_c_kernel.Cil_types.stmt -> unit
method current_func : Frama_c_kernel.Cil_types.fundec option
link to the current function being visited.
NB: for copy visitors, the fundec is the original one.
method set_current_func : Frama_c_kernel.Cil_types.fundec -> unit
method vlogic_type : Frama_c_kernel.Cil_types.logic_type -> Frama_c_kernel.Cil_types.logic_type Frama_c_kernel.Cil.visitAction
method vmodel_info : Frama_c_kernel.Cil_types.model_info -> Frama_c_kernel.Cil_types.model_info Frama_c_kernel.Cil.visitAction
method videntified_term : Frama_c_kernel.Cil_types.identified_term -> Frama_c_kernel.Cil_types.identified_term Frama_c_kernel.Cil.visitAction
method vterm_node : Frama_c_kernel.Cil_types.term_node -> Frama_c_kernel.Cil_types.term_node Frama_c_kernel.Cil.visitAction
method vterm_lval : Frama_c_kernel.Cil_types.term_lval -> Frama_c_kernel.Cil_types.term_lval Frama_c_kernel.Cil.visitAction
method vterm_lhost : Frama_c_kernel.Cil_types.term_lhost -> Frama_c_kernel.Cil_types.term_lhost Frama_c_kernel.Cil.visitAction
method vterm_offset : Frama_c_kernel.Cil_types.term_offset -> Frama_c_kernel.Cil_types.term_offset Frama_c_kernel.Cil.visitAction
method vlogic_label : Frama_c_kernel.Cil_types.logic_label -> Frama_c_kernel.Cil_types.logic_label Frama_c_kernel.Cil.visitAction
method vlogic_info_decl : Frama_c_kernel.Cil_types.logic_info -> Frama_c_kernel.Cil_types.logic_info Frama_c_kernel.Cil.visitAction
method vlogic_info_use : Frama_c_kernel.Cil_types.logic_info -> Frama_c_kernel.Cil_types.logic_info Frama_c_kernel.Cil.visitAction
method vlogic_type_info_decl : Frama_c_kernel.Cil_types.logic_type_info -> Frama_c_kernel.Cil_types.logic_type_info Frama_c_kernel.Cil.visitAction
method vlogic_type_info_use : Frama_c_kernel.Cil_types.logic_type_info -> Frama_c_kernel.Cil_types.logic_type_info Frama_c_kernel.Cil.visitAction
method vlogic_type_def : Frama_c_kernel.Cil_types.logic_type_def -> Frama_c_kernel.Cil_types.logic_type_def Frama_c_kernel.Cil.visitAction
method vlogic_ctor_info_decl : Frama_c_kernel.Cil_types.logic_ctor_info -> Frama_c_kernel.Cil_types.logic_ctor_info Frama_c_kernel.Cil.visitAction
method vlogic_ctor_info_use : Frama_c_kernel.Cil_types.logic_ctor_info -> Frama_c_kernel.Cil_types.logic_ctor_info Frama_c_kernel.Cil.visitAction
method vlogic_var_decl : Frama_c_kernel.Cil_types.logic_var -> Frama_c_kernel.Cil_types.logic_var Frama_c_kernel.Cil.visitAction
method vlogic_var_use : Frama_c_kernel.Cil_types.logic_var -> Frama_c_kernel.Cil_types.logic_var Frama_c_kernel.Cil.visitAction
method vquantifiers : Frama_c_kernel.Cil_types.quantifiers -> Frama_c_kernel.Cil_types.quantifiers Frama_c_kernel.Cil.visitAction
method videntified_predicate : Frama_c_kernel.Cil_types.identified_predicate -> Frama_c_kernel.Cil_types.identified_predicate Frama_c_kernel.Cil.visitAction
method vpredicate_node : Frama_c_kernel.Cil_types.predicate_node -> Frama_c_kernel.Cil_types.predicate_node Frama_c_kernel.Cil.visitAction
method vpredicate : Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.predicate Frama_c_kernel.Cil.visitAction
method vfrees : Frama_c_kernel.Cil_types.identified_term list -> Frama_c_kernel.Cil_types.identified_term list Frama_c_kernel.Cil.visitAction
method vallocates : Frama_c_kernel.Cil_types.identified_term list -> Frama_c_kernel.Cil_types.identified_term list Frama_c_kernel.Cil.visitAction
method vallocation : Frama_c_kernel.Cil_types.allocation -> Frama_c_kernel.Cil_types.allocation Frama_c_kernel.Cil.visitAction
fill the global environment tables at the end of a full copy in a new project.