package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities for ACSL constructs.

exception Not_well_formed of Cil_types.location * string

exception raised when a parsed logic expression is syntactically not well-formed.

basic utilities for logic terms and predicates. See also Logic_const to build terms and predicates.

val add_logic_function : Cil_types.logic_info -> unit

add a logic function in the environment. See Logic_env.add_logic_function_gen

Types

val is_instance_of : string list -> Cil_types.logic_type -> Cil_types.logic_type -> bool

is_instance_of poly t1 t2 returns true if t1 can be derived from t2 by instantiating some of the type variable in poly.

  • since Magnesium-20151001
val unroll_type : ?unroll_typedef:bool -> Cil_types.logic_type -> Cil_types.logic_type

expands logic type definitions. If the unroll_typedef flag is set to true (this is the default), C typedef will be expanded as well.

val isLogicType : (Cil_types.typ -> bool) -> Cil_types.logic_type -> bool

isLogicType test typ is false for pure logic types and the result of test for C types. In case of a set type, the function tests the element type.

val isLogicArrayType : Cil_types.logic_type -> bool

Predefined tests over types

val isLogicCharType : Cil_types.logic_type -> bool
val isLogicAnyCharType : Cil_types.logic_type -> bool
  • since Chlorine-20180501
val isLogicVoidType : Cil_types.logic_type -> bool
val isLogicPointerType : Cil_types.logic_type -> bool
val isLogicVoidPointerType : Cil_types.logic_type -> bool

Type conversions

  • returns

    the equivalent C type.

  • raises Failure

    if the type is purely logical

transforms an array into pointer.

val logic_type_remove_qualifiers : Cil_types.logic_type -> Cil_types.logic_type

removes qualifiers if logic_type is a C type, identity otherwise.

  • since 27.0-Cobalt
val coerce_type : Cil_types.typ -> Cil_types.logic_type

C type to logic type, with implicit conversion for arithmetic types.

  • since 21.0-Scandium

Predicates

transforms \old and \at(,Old) into \at(,L) for L a label pointing to the given statement, creating one if needed.

Terms

val is_C_array : Cil_types.term -> bool

true if the term denotes a C array.

val mk_logic_StartOf : Cil_types.term -> Cil_types.term

creates a TStartOf from an TLval.

creates an AddrOf from a TLval. The given logic type is the type of the lval.

  • since Neon-20140301
val isLogicPointer : Cil_types.term -> bool

true if the term is a pointer.

val mk_logic_pointer_or_StartOf : Cil_types.term -> Cil_types.term

creates either a TStartOf or the corresponding TLval.

val mk_cast : ?loc:Cil_types.location -> ?force:bool -> Cil_types.typ -> Cil_types.term -> Cil_types.term

creates a logic cast if required, with some automatic simplifications being performed automatically. If force is true, the cast will always be inserted. Otherwise (which is the default), mk_cast typ t will return t if it is already of type typ

val array_with_range : Cil_types.exp -> Cil_types.term -> Cil_types.term

array_with_range arr size returns the logic term array'+{0..(size-1)}, array' being array cast to a pointer to char

val remove_logic_coerce : Cil_types.term -> Cil_types.term

Removes TLogic_coerce at head of term.

numeric_coerce typ t returns a term with the same value as t and of type typ. typ which should be Linteger or Lreal. numeric_coerce tries to avoid unnecessary type conversions in t. In particular, numeric_coerce (int)cst Linteger, where cst fits in int will be directly cst, without any coercion.

Also coerce recursively the sub-terms of t-set expressions (range, union, inter and comprehension) and lift the associated set type.

  • since Magnesium-20151001
  • before 21.0-Scandium

    was ambiguous (coercion vs. conversion).

Predicates

\pointer_comparable. label defaults to Logic_const.here_label

  • since Fluorine-20130401
  • before 27.0-Cobalt

    no label argument, as the builtin did not take a label

Conversion from exp to term

val expr_to_term : ?coerce:bool -> Cil_types.exp -> Cil_types.term

Returns a logic term that has exactly the same semantics as the original C-expression. The type of the resulting term is determined by the ~coerce flag as follows:

  • when ~coerce:false is given (the default) the term has the same c-type as the original expression.
  • when ~coerce:true is given, if the original expression has an int or float type, then the returned term is coerced into the integer or real logic type, respectively.

Remark: when the original expression is a comparison, it is evaluated as an int or an integer depending on the ~coerce flag. To obtain a boolean or predicate, use expr_to_boolean or expr_to_predicate instead.

  • before 21.0-Scandium

    was unsound in many cases.

val expr_to_predicate : Cil_types.exp -> Cil_types.predicate

Returns a predicate semantically equivalent to the condition of the original C-expression.

This is different from expr_to_term e |> scalar_term_to_predicate since C-relations are translated into logic ones.

  • raises Fatal

    error if the expression is not a comparison and cannot be compared to zero.

  • since Sulfur-20171101
  • before 21.0-Scandium

    was unsound in many cases.

val expr_to_ipredicate : Cil_types.exp -> Cil_types.identified_predicate

Returns a predicate semantically equivalent to the condition of the original C-expression.

Identical to expr_to_predicate e |> Logic_const.new_predicate.

  • raises Fatal

    error if the expression is not a comparison and cannot be compared to zero.

  • since Sulfur-20171101
  • before 21.0-Scandium

    was unsound in many cases.

val expr_to_boolean : Cil_types.exp -> Cil_types.term

Returns a boolean term semantically equivalent to the condition of the original C-expression.

This is different from expr_to_term e |> scalar_term_to_predicate since C-relations are translated into logic ones.

  • raises Fatal

    error if the expression is not a comparison and cannot be compared to zero.

  • since Sulfur-20171101
  • before 21.0-Scandium

    was unsound in many cases.

val is_zero_comparable : Cil_types.term -> bool

true if the given term has a type for which a comparison to 0 exists (i.e. scalar C types, logic integers and reals).

  • since Sulfur-20171101
val scalar_term_to_boolean : Cil_types.term -> Cil_types.term

Compare the given term with the constant 0 (of the appropriate type) to return the result of the comparison e <> 0 as a boolean term.

  • raises Fatal

    error if the argument cannot be compared to 0

  • since 21.0-Scandium
val scalar_term_to_predicate : Cil_types.term -> Cil_types.predicate

Compare the given term with the constant 0 (of the appropriate type) to return the result of the comparison e <> 0.

  • raises Fatal

    error if the argument cannot be compared to 0

  • since Sulfur-20171101
val lval_to_term_lval : Cil_types.lval -> Cil_types.term_lval
val host_to_term_lhost : Cil_types.lhost -> Cil_types.term_lhost
val offset_to_term_offset : Cil_types.offset -> Cil_types.term_offset
val constant_to_lconstant : Cil_types.constant -> Cil_types.logic_constant
val lconstant_to_constant : Cil_types.logic_constant -> Cil_types.constant
val parse_float : ?loc:Cil_types.location -> string -> Cil_types.term

Parse the given string as a float or real logic constant.

The parsed literal is always kept as it is in the resulting term. The returned term is either a real constant or real constant casted into a C-float type.

Unsuffixed literals are considered as real numbers. Literals suffixed by f|d|l or F|D|L are considered as float constants of the associated kind.

Various Utilities

remove_term_offset o returns o without its last offset and this last offset.

val lval_contains_result : Cil_types.term_lhost -> bool

true if \result is included in the lval.

val loffset_contains_result : Cil_types.term_offset -> bool

true if \result is included in the offset.

val contains_result : Cil_types.term -> bool

true if \result is included in the term

val get_pred_body : Cil_types.logic_info -> Cil_types.predicate

returns the body of the given predicate.

  • raises Not_found

    if the logic_info is not the definition of a predicate.

val is_result : Cil_types.term -> bool

true if the term is \result or an offset of \result.

val lhost_c_type : Cil_types.term_lhost -> Cil_types.typ
val is_trivially_true : Cil_types.predicate -> bool

true if the predicate is Ptrue.

  • since Nitrogen-20111001
val is_trivially_false : Cil_types.predicate -> bool

true if the predicate is Pfalse

  • since Nitrogen-20111001

Code annotations

val is_annot_next_stmt : Cil_types.code_annotation -> bool

Does the annotation apply to the next statement (e.g. a statement contract). Also false for loop-related annotations.

  • since 21.0-Scandium

Global annotations

add an attribute to a global annotation

  • since Phosphorus-20170501-beta1

Contracts

val behavior_has_only_assigns : Cil_types.behavior -> bool

true if the behavior has only an assigns clause.

  • since 22.0-Titanium
val funspec_has_only_assigns : Cil_types.funspec -> bool

true if the only non-empty fields of the contract are assigns clauses

  • since 22.0-Titanium

Structural equality between annotations

val is_same_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
val is_same_logic_label : Cil_types.logic_label -> Cil_types.logic_label -> bool
val is_same_pconstant : Logic_ptree.constant -> Logic_ptree.constant -> bool
  • since Nitrogen-20111001
val is_same_type : Cil_types.logic_type -> Cil_types.logic_type -> bool
val is_same_var : Cil_types.logic_var -> Cil_types.logic_var -> bool
val is_same_logic_signature : Cil_types.logic_info -> Cil_types.logic_info -> bool
val is_same_logic_profile : Cil_types.logic_info -> Cil_types.logic_info -> bool
val is_same_builtin_profile : Cil_types.builtin_logic_info -> Cil_types.builtin_logic_info -> bool
val is_same_logic_ctor_info : Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info -> bool
val is_same_term : Cil_types.term -> Cil_types.term -> bool
val is_same_logic_info : Cil_types.logic_info -> Cil_types.logic_info -> bool
val is_same_logic_body : Cil_types.logic_body -> Cil_types.logic_body -> bool
val is_same_indcase : (string * Cil_types.logic_label list * string list * Cil_types.predicate) -> (string * Cil_types.logic_label list * string list * Cil_types.predicate) -> bool
val is_same_tlval : Cil_types.term_lval -> Cil_types.term_lval -> bool
val is_same_lhost : Cil_types.term_lhost -> Cil_types.term_lhost -> bool
val is_same_offset : Cil_types.term_offset -> Cil_types.term_offset -> bool
val is_same_predicate_node : Cil_types.predicate_node -> Cil_types.predicate_node -> bool
val is_same_predicate : Cil_types.predicate -> Cil_types.predicate -> bool
val is_same_identified_predicate : Cil_types.identified_predicate -> Cil_types.identified_predicate -> bool
val is_same_identified_term : Cil_types.identified_term -> Cil_types.identified_term -> bool
val is_same_deps : Cil_types.deps -> Cil_types.deps -> bool
val is_same_allocation : Cil_types.allocation -> Cil_types.allocation -> bool
val is_same_assigns : Cil_types.assigns -> Cil_types.assigns -> bool
val is_same_variant : Cil_types.variant -> Cil_types.variant -> bool
val is_same_post_cond : (Cil_types.termination_kind * Cil_types.identified_predicate) -> (Cil_types.termination_kind * Cil_types.identified_predicate) -> bool
val is_same_behavior : Cil_types.funbehavior -> Cil_types.funbehavior -> bool
val is_same_spec : Cil_types.funspec -> Cil_types.funspec -> bool
val is_same_logic_type_def : Cil_types.logic_type_def -> Cil_types.logic_type_def -> bool
val is_same_logic_type_info : Cil_types.logic_type_info -> Cil_types.logic_type_info -> bool
val is_same_loop_pragma : Cil_types.loop_pragma -> Cil_types.loop_pragma -> bool
val is_same_slice_pragma : Cil_types.slice_pragma -> Cil_types.slice_pragma -> bool
val is_same_impact_pragma : Cil_types.impact_pragma -> Cil_types.impact_pragma -> bool
val is_same_pragma : Cil_types.pragma -> Cil_types.pragma -> bool
val is_same_code_annotation : Cil_types.code_annotation -> Cil_types.code_annotation -> bool
val is_same_global_annotation : Cil_types.global_annotation -> Cil_types.global_annotation -> bool
val is_same_axiomatic : Cil_types.global_annotation list -> Cil_types.global_annotation list -> bool
val is_same_model_info : Cil_types.model_info -> Cil_types.model_info -> bool
  • since Oxygen-20120901
val is_same_lexpr : Logic_ptree.lexpr -> Logic_ptree.lexpr -> bool
val hash_term : Cil_types.term -> int

hash function compatible with is_same_term

val compare_term : Cil_types.term -> Cil_types.term -> int

comparison compatible with is_same_term

val hash_predicate : Cil_types.predicate -> int
val compare_predicate : Cil_types.predicate -> Cil_types.predicate -> int

Merging contracts

val get_behavior_names : Cil_types.spec -> string list

Concatenates two assigns if both are defined, returns WritesAny if one (or both) of them is WritesAny.

  • since Nitrogen-20111001

merge assigns: take the one that is defined and select an arbitrary one if both are, emitting a warning unless both are syntactically the same.

Concatenates two allocation clauses if both are defined, returns FreeAllocAny if one (or both) of them is FreeAllocAny.

  • since Nitrogen-20111001

merge allocation: take the one that is defined and select an arbitrary one if both are, emitting a warning unless both are syntactically the same.

  • since Oxygen-20120901
val merge_behaviors : ?oldloc:Cil_types.location -> silent:bool -> Cil_types.funbehavior list -> Cil_types.funbehavior list -> Cil_types.funbehavior list
val merge_funspec : ?oldloc:Cil_types.location -> ?silent_about_merging_behav:bool -> Cil_types.funspec -> Cil_types.funspec -> unit

merge_funspec ?oldloc oldspec newspec merges newspec into oldspec. If the funspec belongs to a kernel function, do not forget to call Kernel_function.set_spec after merging.

val clear_funspec : Cil_types.funspec -> unit

Reset the given funspec to empty.

  • since Nitrogen-20111001

Discriminating code_annotations

val use_predicate : Cil_types.predicate_kind -> bool

Checks if a predicate kind can be used as an hypothesis or requirement. It is true for `Admit` and `Assert`, and false for `Check`.

val verify_predicate : Cil_types.predicate_kind -> bool

Checks if a predicate kind shall be put under verification. It is true for `Assert` and `Check`, and false for `Admit`.

The functions below allow testing for specific kinds of code_annotation. Use them in conjunction with iterators in Annotations to retrieve a particular kind of annotation associated to a statement.

val is_assert : Cil_types.code_annotation -> bool
val is_check : Cil_types.code_annotation -> bool
val is_admit : Cil_types.code_annotation -> bool
val is_contract : Cil_types.code_annotation -> bool
val is_stmt_invariant : Cil_types.code_annotation -> bool
val is_loop_invariant : Cil_types.code_annotation -> bool
val is_invariant : Cil_types.code_annotation -> bool
val is_variant : Cil_types.code_annotation -> bool
val is_allocation : Cil_types.code_annotation -> bool
val is_assigns : Cil_types.code_annotation -> bool
val is_pragma : Cil_types.code_annotation -> bool
val is_loop_pragma : Cil_types.code_annotation -> bool
val is_slice_pragma : Cil_types.code_annotation -> bool
val is_impact_pragma : Cil_types.code_annotation -> bool
val is_loop_annot : Cil_types.code_annotation -> bool
val is_trivial_annotation : Cil_types.code_annotation -> bool
val is_property_pragma : Cil_types.pragma -> bool

Should this pragma be proved by plugins

val extract_loop_pragma : Cil_types.code_annotation list -> Cil_types.loop_pragma list
val extract_contract : Cil_types.code_annotation list -> (string list * Cil_types.funspec) list

Constant folding

val constFoldTermToInt : ?machdep:bool -> Cil_types.term -> Integer.t option

A cilVisitor (by copy) that simplifies expressions of the type const int x = v, where v is an integer and x is a global variable. Requires a mapping from varinfo to init option (e.g. based on Globals.Vars.find).

Type-checking hackery

val complete_types : Cil_types.file -> unit

give complete types to terms that refer to a variable whose type has been completed after its use in an annotation. Internal use only.

  • since Neon-20140301