Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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 -> Z.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 -> Z.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 -> Z.t

returns the value of the corresponding integer literal. It is the responsibility 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 -> Z.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.

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).

val is_string_literal : Cil_types.varinfo -> bool

true if the varinfo is a global variable representing a string literal.

  • since 32.0-Germanium

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 -> Z.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 -> Z.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 -> Z.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 constant_term : Cil_types.location -> Z.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 is_block_local : Cil_types.varinfo -> Cil_types.block -> bool

determines if a var is local to a block.

local_block f vi returns the block of f in which vi is declared. vi must be a variable of f.

Types

val direct_array_size : Cil_types.typ -> Z.t
val array_size : Cil_types.typ -> Z.t

Functions

module Function : sig ... end

Operations on cil function.

Predefined

val start_with_frama_c : string -> bool
  • returns

    true if the given string starts with "Frama_C_".

  • since 29.0-Copper
val is_show_each_builtin : string -> bool
  • returns

    true if the given string starts with "Frama_C_show_each".

  • since 29.0-Copper
val is_domain_show_each_builtin : string -> bool
  • returns

    true if the given string starts with "Frama_C_domain_show_each".

  • since 29.0-Copper
val is_dump_each_builtin : string -> bool
  • returns

    true if the given string starts with "Frama_C_dump_each".

  • since 29.0-Copper
val is_dump_file_builtin : string -> bool
  • returns

    true if the given string starts with "Frama_C_dump_each_file".

  • since 29.0-Copper
val is_split_builtin : string -> bool
  • returns

    true if the given string starts with "Frama_C_builtin_split".

  • since 29.0-Copper
val start_with_frama_c_builtin : string -> bool
  • returns

    true if the given string starts with "Frama_C_".

  • since 29.0-Copper
val is_frama_c_builtin : Cil_types.varinfo -> bool