package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Expressions
Logical terms
Statements
Types
Functions
Predefined

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Ast_info/index.html

Module `Frama_c_kernel.Ast_info`

AST manipulation utilities.

Expressions

val is_integral_const : Cil_types.constant -> bool

true iff the constant is an integer constant (i.e. neither a float nor a string). Enum tags and chars are integer constants.

val possible_value_of_integral_const : Cil_types.constant -> Integer.t option

returns the value of the corresponding integer literal or None if the constant is not an integer (i.e. is_integral_const returns false).

val possible_value_of_integral_expr : Cil_types.exp -> Integer.t option

returns the value of the corresponding integer constant expression, or None if the expression is not a constant expression or does not evaluate to an integer constant.

before 26.0-Iron
the function only returned Some v when the expression was an integer literal (i.e. Const c).

val value_of_integral_const : Cil_types.constant -> Integer.t

returns the value of the corresponding integer literal. It is the responsability of the caller to ensure the constant is indeed an integer constant. If unsure, use possible_value_of_integral_const.

val value_of_integral_expr : Cil_types.exp -> Integer.t

returns the value of the corresponding integer constant expression. It is the responsibility of the caller to ensure that the argument is indeed an integer constant expression. If unsure, use possible_value_of_integral_expr.

before 26.0-Iron
the function would fail if the expression was not an integer literal (see possible_value_of_integral_expr).

val is_null_expr : Cil_types.exp -> bool

true iff the expression is a constant expression that evaluates to a null pointer, i.e. 0 or a cast to 0.

before 26.0-Iron
the function would return false as soon as the expression was not an integer literal (possibly casted).

val is_non_null_expr : Cil_types.exp -> bool

true iff the expression is a constant expression that evaluates to a non-null pointer.

Warning: note that for the purpose of this function &x is not a constant expression, hence the function will return false in this case.

before 26.0-Iron
the function would return false as soon as the expression was not an integer literal (possibly casted).

Logical terms

val is_integral_logic_const : Cil_types.logic_constant -> bool

returns
true if the constant has integral type (integer, char, enum). false otherwise.

since Oxygen-20120901

val possible_value_of_integral_logic_const : 
  Cil_types.logic_constant ->
  Integer.t option

returns
Some n if the constant has integral type (integer, char, enum). None otherwise.

since Oxygen-20120901

val value_of_integral_logic_const : Cil_types.logic_constant -> Integer.t

returns
the value of the constant. Assume the argument is an integral constant.

since Oxygen-20120901

val possible_value_of_integral_term : Cil_types.term -> Integer.t option

returns
Some n if the term has integral type (integer, char, enum). None Otherwise.

since Oxygen-20120901

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 : goal:bool -> Cil_types.funspec -> Cil_types.predicate

Builds the precondition from b_assumes and b_requires clauses. With ~goal:true, only returns assert and check predicates. With ~goal:false, only returns assert and admit predicates.

since Carbon-20101201

before 23.0-Vanadium
no goal flag.

val behavior_assumes : Cil_types.funbehavior -> Cil_types.predicate

Builds the conjunction of the b_assumes.

since Nitrogen-20111001

val behavior_precondition : 
  goal:bool ->
  Cil_types.funbehavior ->
  Cil_types.predicate

Builds the precondition from b_assumes and b_requires clauses. For flag ~goal see Ast_info.precondition above.

since Carbon-20101201

before 23.0-Vanadium
no goal flag.

val behavior_postcondition : 
  goal:bool ->
  Cil_types.funbehavior ->
  Cil_types.termination_kind ->
  Cil_types.predicate

Builds the postcondition from b_assumes and b_post_cond clauses. For flag ~goal see Ast_info.precondition above.

before 23.0-Vanadium
no goal flag.

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

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.

since Oxygen-20120901

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

returns
the assigns of an unguarded behavior or a set of complete behaviors.

since Oxygen-20120901

val merge_assigns : 
  ?warn:bool ->
  Cil_types.funbehavior list ->
  Cil_types.assigns

Returns the assigns of an unguarded behavior. Optional warn argument 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