module Ast_info: sig
.. end
AST manipulation utilities.
Expressions
val is_integral_const : Cil_types.constant -> bool
val possible_value_of_integral_const : Cil_types.constant -> Integer.t option
val possible_value_of_integral_expr : Cil_types.exp -> Integer.t option
val value_of_integral_const : Cil_types.constant -> Integer.t
val value_of_integral_expr : Cil_types.exp -> Integer.t
val constant_expr : loc:Cil_types.location -> Integer.t -> Cil_types.exp
val is_null_expr : Cil_types.exp -> bool
val is_non_null_expr : Cil_types.exp -> bool
Logical terms
val is_integral_logic_const : Cil_types.logic_constant -> bool
Since Oxygen-20120901
Returns true
if the constant has integral type (integer, char,
enum)
. false
otherwise.
val possible_value_of_integral_logic_const : Cil_types.logic_constant -> Integer.t option
Since Oxygen-20120901
Returns Some n
if the constant has integral type (integer, char,
enum)
. None
otherwise.
val value_of_integral_logic_const : Cil_types.logic_constant -> Integer.t
Since Oxygen-20120901
Returns the value of the constant.
Assume the argument is an integral constant.
val possible_value_of_integral_term : Cil_types.term -> Integer.t option
Since Oxygen-20120901
Returns Some n
if the term has integral type (integer, char,
enum)
. None
Otherwise.
val term_lvals_of_term : Cil_types.term -> Cil_types.term_lval list
Returns the list of all the term lvals of a given term.
Purely syntactic function.
val precondition : Cil_types.funspec -> Cil_types.predicate
Builds the precondition from b_assumes
and b_requires
clauses.
Since Carbon-20101201
val behavior_assumes : Cil_types.funbehavior -> Cil_types.predicate
Builds the conjunction of the b_assumes
.
Since Nitrogen-20111001
val behavior_precondition : Cil_types.funbehavior -> Cil_types.predicate
Builds the precondition from b_assumes
and b_requires
clauses.
Since Carbon-20101201
val behavior_postcondition : Cil_types.funbehavior -> Cil_types.termination_kind -> Cil_types.predicate
Builds the postcondition from b_assumes
and b_post_cond
clauses.
Change in Boron-20100401: added termination kind as filtering argument.
val disjoint_behaviors : Cil_types.funspec -> string list -> Cil_types.predicate
Builds the disjoint_behaviors
property for the behavior names.
Since Nitrogen-20111001
val complete_behaviors : Cil_types.funspec -> string list -> Cil_types.predicate
Builds the disjoint_behaviors
property for the behavior names.
Since Nitrogen-20111001
val merge_assigns_from_complete_bhvs : ?warn:bool ->
?unguarded:bool ->
Cil_types.funbehavior list ->
string list list -> Cil_types.identified_term Cil_types.assigns
Since Oxygen-20120901
Returns the assigns of an unguarded behavior (when
unguarded
=true)
or a set of complete behaviors.
- the funbehaviors can come from either a statement contract or a function
contract.
- the list of sets of behavior names can come from the contract of the
related function.
Optional
warn
argument can be used to force emitting or cancelation of
warnings.
val merge_assigns_from_spec : ?warn:bool ->
Cil_types.funspec -> Cil_types.identified_term Cil_types.assigns
It is a shortcut for merge_assigns_from_complete_bhvs
spec.spec_complete_behaviors spec.spec_behavior
. Optional warn
argument
can be used to force emitting or cancelation of warnings
Since Oxygen-20120901
Returns the assigns of an unguarded behavior or a set of complete behaviors.
val merge_assigns : ?warn:bool ->
Cil_types.funbehavior list -> Cil_types.identified_term Cil_types.assigns
Returns the assigns of an unguarded behavior.
Change in Oxygen-20120901: Optional warn
argument added which can be used to
force emitting or cancelation of warnings.
val variable_term : Cil_types.location -> Cil_types.logic_var -> Cil_types.term
val constant_term : Cil_types.location -> Integer.t -> Cil_types.term
val is_null_term : Cil_types.term -> bool
Statements
val is_loop_statement : Cil_types.stmt -> bool
val get_sid : Cil_types.kinstr -> int
val mkassign : Cil_types.lval -> Cil_types.exp -> Cil_types.location -> Cil_types.instr
val mkassign_statement : Cil_types.lval -> Cil_types.exp -> Cil_types.location -> Cil_types.stmt
val is_block_local : Cil_types.varinfo -> Cil_types.block -> bool
determines if a var is local to a block.
val block_of_local : Cil_types.fundec -> Cil_types.varinfo -> Cil_types.block
local_block f vi
returns the block of f
in which vi
is declared.
vi
must be a variable of f
.
Types
val array_type : ?length:Cil_types.exp ->
?attr:Cil_types.attributes -> Cil_types.typ -> Cil_types.typ
val direct_array_size : Cil_types.typ -> Integer.t
val array_size : Cil_types.typ -> Integer.t
val direct_element_type : Cil_types.typ -> Cil_types.typ
val element_type : Cil_types.typ -> Cil_types.typ
val direct_pointed_type : Cil_types.typ -> Cil_types.typ
val pointed_type : Cil_types.typ -> Cil_types.typ
Functions
val is_function_type : Cil_types.varinfo -> bool
Return true
iff the type of the given varinfo is a function type.
module Function: sig
.. end
Operations on cil function.
Predefined
val can_be_cea_function : string -> bool
val is_cea_function : string -> bool
val is_cea_dump_function : string -> bool
val is_cea_dump_file_function : string -> bool
val is_frama_c_builtin : string -> bool