Module Logic_utils

module Logic_utils: sig .. end
Utilities for ACSL constructs.
Consult the Plugin Development Guide for additional details.

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 instantiate : (string * Cil_types.logic_type) list ->
Cil_types.logic_type -> Cil_types.logic_type
instantiate type variables in a logic type.
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
Change in Chlorine-20180501: old behavior renamed as isLogicAnyCharType
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


val logicCType : Cil_types.logic_type -> Cil_types.typ
Raises Failure if the type is purely logical
Returns the equivalent C type.
val array_to_ptr : Cil_types.logic_type -> Cil_types.logic_type
transforms an array into pointer.
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


val predicate_of_identified_predicate : Cil_types.identified_predicate -> Cil_types.predicate
Deprecated.use Logic_const.pred_of_id_pred instead
val translate_old_label : Cil_types.stmt -> Cil_types.predicate -> Cil_types.predicate
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.
val mk_logic_AddrOf : ?loc:Cil_types.location ->
Cil_types.term_lval -> Cil_types.logic_type -> Cil_types.term
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
Change in Aluminium-20160501: added force optional argument
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.
val numeric_coerce : Cil_types.logic_type -> Cil_types.term -> Cil_types.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
Change in 21.0-Scandium


Predicates



\valid_index

\valid_range
val pointer_comparable : ?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
\pointer_comparable
Since Fluorine-20130401

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: 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.
Change in 21.0-Scandium
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.
Since Sulfur-20171101
Raises Fatal error if the expression is not a comparison and cannot be compared to zero.
Change in 21.0-Scandium

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.
Since Sulfur-20171101
Raises Fatal error if the expression is not a comparison and cannot be compared to zero.
Change in 21.0-Scandium

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.
Since Sulfur-20171101
Raises Fatal error if the expression is not a comparison and cannot be compared to zero.
Change in 21.0-Scandium

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.
Since 21.0-Scandium
Raises Fatal error if the argument cannot be compared to 0
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.
Since Sulfur-20171101
Raises Fatal error if the argument cannot be compared to 0
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


val remove_term_offset : Cil_types.term_offset -> Cil_types.term_offset * Cil_types.term_offset
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


val add_attribute_glob_annot : Cil_types.attribute ->
Cil_types.global_annotation -> Cil_types.global_annotation
add an attribute to a global annotation
Since Phosphorus-20170501-beta1

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_constant : Cil_types.constant -> Cil_types.constant -> bool
Deprecated.Nitrogen-20111001 use Cil.compareConstant instead.
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
Since Oxygen-20120901
val is_same_model_info : Cil_types.model_info -> Cil_types.model_info -> bool
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
val concat_assigns : Cil_types.assigns -> Cil_types.assigns -> Cil_types.assigns
Concatenates two assigns if both are defined, returns WritesAny if one (or both) of them is WritesAny.
Since Nitrogen-20111001
val merge_assigns : Cil_types.assigns -> Cil_types.assigns -> Cil_types.assigns
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.
val concat_allocation : Cil_types.allocation -> Cil_types.allocation -> Cil_types.allocation
Concatenates two allocation clauses if both are defined, returns FreeAllocAny if one (or both) of them is FreeAllocAny.
Since Nitrogen-20111001
val merge_allocation : Cil_types.allocation -> Cil_types.allocation -> Cil_types.allocation
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.
Change in 20.0-Calcium: add optional parameter oldloc.
val clear_funspec : Cil_types.funspec -> unit
Reset the given funspec to empty.
Since Nitrogen-20111001

Discriminating code_annotations



Functions below allows to test a special kind of code_annotation. Use them in conjunction with Annotations.get_filter to retrieve a particular kind of annotations associated to a statement.
val is_assert : Cil_types.code_annotation -> bool
val is_check : 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_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
class simplify_const_lval : (Cil_types.varinfo -> Cil_types.init option) -> Cil.cilVisitor
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.

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

Parsing hackery



Values that control the various modes of the parser and lexer for logic. Use with care.
val kw_c_mode : bool Pervasives.ref
val enter_kw_c_mode : unit -> unit
val exit_kw_c_mode : unit -> unit
val is_kw_c_mode : unit -> bool
val rt_type_mode : bool Pervasives.ref
val enter_rt_type_mode : unit -> unit
val exit_rt_type_mode : unit -> unit
val is_rt_type_mode : unit -> bool