Frama-C API - Eva_ast_utils
Utilitary functions on the Eva AST of lvalues and expressions.
Conversion to Cil
val to_cil_exp : Eva_ast_types.exp -> Frama_c_kernel.Cil_types.expval to_cil_lval : Eva_ast_types.lval -> Frama_c_kernel.Cil_types.lvalQueries
val is_mutable : Eva_ast_types.lval -> boolCf Cil.is_mutable_or_initialized.
val is_initialized : Eva_ast_types.lval -> boolExpressions/Lvalue heights
val height_exp : Eva_ast_types.exp -> intComputes the height of an expression, that is the maximum number of nested operations in this expression.
val height_lval : Eva_ast_types.lval -> intComputes the height of an lvalue.
Specialized visitors
val exp_contains_volatile : Eva_ast_types.exp -> boolexp_contains_volatile e (resp. lval_contains_volatile lv is true whenever one l-value contained inside the expression e (resp. the lvalue lv) has volatile qualifier. Relational analyses should not learn anything on such values.
val lval_contains_volatile : Eva_ast_types.lval -> boolval vars_in_exp : Eva_ast_types.exp -> Frama_c_kernel.Cil_datatype.Varinfo.Set.tReturns the set of variables that syntactically appear in an expression or lvalue.
val vars_in_lval : Eva_ast_types.lval -> Frama_c_kernel.Cil_datatype.Varinfo.Set.tConstant conversion and folding.
val const_fold : Eva_ast_types.exp -> Eva_ast_types.expval fold_to_integer : Eva_ast_types.exp -> Frama_c_kernel.Z.t optionval is_zero_ptr : Eva_ast_types.exp -> boolOffsets
val last_offset : Eva_ast_types.offset -> Eva_ast_types.offsetReturns the last offset in the chain.
val is_bitfield : Eva_ast_types.lval -> boolIs an lvalue a bitfield?