Module Ast_info

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.assigns
Since Oxygen-20120901
Returns the assigns of an unguarded behavior (when unguarded=true) or a set of complete behaviors.
val merge_assigns_from_spec : ?warn:bool -> Cil_types.funspec -> 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.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_domain_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