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.

exception Unknown_ext

exception raised when an unknown extension is called.

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct