Frama-C API - Logic_utils

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

exception raised when an unknown extension is called.

Test if the given string contains ':' (long-identifiers).

Split a long-identifier into the list of its components. eg. "A::B::(<:)" is split into ["A";"B";"(<:)"]. Returns a singleton for regular identifiers.

• since 30.0-Zinc

Check if there is a logic function with same profile in the environment.

• since 30.0-Zinc

Add a logic function in the environment. Replaces any existing logic function with the same profile. See Logic_env.add_logic_function_gen

• since 30.0-Zinc

remove any logic function with the same profile from the environment. See Logic_env.remove_logic_function_gen

• since 30.0-Zinc

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

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

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.

Predefined tests over types

• since Chlorine-20180501

• returns

  the equivalent C type.

• raises Failure

  if the type is purely logical

transforms an array into pointer.

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

• since 27.0-Cobalt

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

• since 21.0-Scandium

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

true if the term denotes a C array.

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

true if the term is a pointer.

creates either a TStartOf or the corresponding TLval.

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

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

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

\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

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.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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.

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.

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.

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

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

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

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.

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

true if \result is included in the lval.

true if \result is included in the offset.

true if \result is included in the term

returns the body of the given predicate.

• raises Not_found

  if the logic_info is not the definition of a predicate.

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

true if the predicate is Ptrue.

• since Nitrogen-20111001

true if the predicate is Pfalse

• since Nitrogen-20111001

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

• since 21.0-Scandium

add an attribute to a global annotation

• since Phosphorus-20170501-beta1

true if the behavior has only an assigns clause.

• since 22.0-Titanium

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

• since 22.0-Titanium

• since Nitrogen-20111001

• since Oxygen-20120901

hash function compatible with is_same_term

comparison compatible with is_same_term

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

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.

Reset the given funspec to empty.

• since Nitrogen-20111001

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

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

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

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