module Logic_utils: sig
.. end
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
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.
val isLogicArrayType : Cil_types.logic_type -> bool
Predefined tests over types
val isLogicCharType : Cil_types.logic_type -> bool
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 typ_to_logic_type : Cil_types.typ -> Cil_types.logic_type
C type to logic type, with implicit conversion for arithmetic types.
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.
Since Magnesium-20151001
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
val points_to_valid_string : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate
\points_to_valid_string
Since Neon-20140301
Conversion from exp to term
val expr_to_term : cast:bool -> Cil_types.exp -> Cil_types.term
translates a C expression into an "equivalent" logical term.
cast
specifies how C arithmetic operators are translated.
When
cast
is
true
, the translation returns a logic
term
having the
same semantics of the C
expr
by introducing casts (i.e. the C expr
a+b
can be translated as
(char)(((char)a)+(char)b)
to preserve the modulo
feature of the C addition).
Otherwise, no such casts are introduced and the C arithmetic operators are
translated into perfect mathematical operators (i.e. a floating point
addition is translated into an addition of
real
numbers).
Consult the Plugin Development Guide for additional details.
val expr_to_term_coerce : cast:bool -> Cil_types.exp -> Cil_types.term
same as
Logic_utils.expr_to_term
, except that if the new term has an arithmetic
type, it is automatically coerced into real (or integer for integral types).
Since Magnesium-20151001
val lval_to_term_lval : cast:bool -> Cil_types.lval -> Cil_types.term_lval
val host_to_term_host : cast:bool -> Cil_types.lhost -> Cil_types.term_lhost
val offset_to_term_offset : cast:bool -> 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 string_to_float_lconstant : string -> Cil_types.logic_constant
Parse the given string as a float logic constant, taking into account
the fact that the constant may not be exactly representable. This
function should only be called on strings that have been recognized
by the parser as valid floats
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
Predicates
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
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
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.identified_term Cil_types.deps ->
Cil_types.identified_term Cil_types.deps -> bool
val is_same_allocation : Cil_types.identified_term Cil_types.allocation ->
Cil_types.identified_term Cil_types.allocation -> bool
val is_same_assigns : Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term Cil_types.assigns -> bool
val is_same_variant : Cil_types.term Cil_types.variant -> Cil_types.term 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.term Cil_types.loop_pragma ->
Cil_types.term Cil_types.loop_pragma -> bool
val is_same_slice_pragma : Cil_types.term Cil_types.slice_pragma ->
Cil_types.term Cil_types.slice_pragma -> bool
val is_same_impact_pragma : Cil_types.term Cil_types.impact_pragma ->
Cil_types.term Cil_types.impact_pragma -> bool
val is_same_pragma : Cil_types.term Cil_types.pragma -> Cil_types.term 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
Merging contracts
val get_behavior_names : Cil_types.spec -> string list
val concat_assigns : Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term 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.identified_term Cil_types.assigns ->
Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term 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.identified_term Cil_types.allocation ->
Cil_types.identified_term Cil_types.allocation ->
Cil_types.identified_term 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.identified_term Cil_types.allocation ->
Cil_types.identified_term Cil_types.allocation ->
Cil_types.identified_term 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 : silent:bool ->
Cil_types.funbehavior list ->
Cil_types.funbehavior list -> Cil_types.funbehavior list
val merge_funspec : ?silent_about_merging_behav:bool ->
Cil_types.funspec -> Cil_types.funspec -> unit
merge_funspec 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
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_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.term Cil_types.pragma -> bool
Should this pragma be proved by plugins
: Cil_types.code_annotation list -> Cil_types.term Cil_types.loop_pragma list
: 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 register_extension : string -> unit
register a given name as a clause name for extended contract.
val is_extension : string -> bool
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