module Logic_utils:sig
..end
exception Not_well_formed of Cil_types.location * string
Logic_const
to build terms and predicates.val add_logic_function : Cil_types.logic_info -> unit
Logic_env.add_logic_function_gen
val instantiate : (string * Cil_types.logic_type) list ->
Cil_types.logic_type -> Cil_types.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
.val unroll_type : ?unroll_typedef:bool -> Cil_types.logic_type -> Cil_types.logic_type
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
val isLogicCharType : Cil_types.logic_type -> bool
isLogicAnyCharType
val isLogicAnyCharType : 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
val logicCType : Cil_types.logic_type -> Cil_types.typ
Failure
if the type is purely logicalval array_to_ptr : Cil_types.logic_type -> Cil_types.logic_type
val typ_to_logic_type : Cil_types.typ -> Cil_types.logic_type
val predicate_of_identified_predicate : Cil_types.identified_predicate -> Cil_types.predicate
val translate_old_label : Cil_types.stmt -> Cil_types.predicate -> Cil_types.predicate
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
val mk_logic_AddrOf : ?loc:Cil_types.location ->
Cil_types.term_lval -> Cil_types.logic_type -> Cil_types.term
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
val mk_cast : ?loc:Cil_types.location ->
?force:bool -> Cil_types.typ -> Cil_types.term -> Cil_types.term
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
force
optional argumentval 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 charval remove_logic_coerce : Cil_types.term -> Cil_types.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.val pointer_comparable : ?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
val expr_to_term : cast:bool -> Cil_types.exp -> Cil_types.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).
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
Consult the Plugin Development Guide for additional details.
val expr_to_term_coerce : cast:bool -> Cil_types.exp -> Cil_types.term
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).val expr_to_predicate : cast:bool -> Cil_types.exp -> Cil_types.identified_predicate
==
, <=
, etc) are translated directly.
Otherwise, the result of expr_to_predicate e
is the predicate
e <> 0
.Fatal
error if the expression is not a comparison and cannot be
compared to zero.val scalar_term_to_predicate : Cil_types.term -> Cil_types.predicate
e <> 0
.Fatal
error if the argument cannot be compared to 0val 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
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
val loffset_contains_result : Cil_types.term_offset -> bool
val contains_result : Cil_types.term -> bool
val get_pred_body : Cil_types.logic_info -> Cil_types.predicate
Not_found
if the logic_info is not the definition of a predicate.val is_result : Cil_types.term -> bool
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.val is_trivially_false : Cil_types.predicate -> bool
true
if the predicate is Pfalseval add_attribute_glob_annot : Cil_types.attribute ->
Cil_types.global_annotation -> Cil_types.global_annotation
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
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.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
val is_same_lexpr : Logic_ptree.lexpr -> Logic_ptree.lexpr -> bool
val hash_term : Cil_types.term -> int
val compare_term : Cil_types.term -> Cil_types.term -> int
val hash_predicate : Cil_types.predicate -> int
val compare_predicate : Cil_types.predicate -> Cil_types.predicate -> int
val get_behavior_names : Cil_types.spec -> string list
val concat_assigns : Cil_types.assigns -> Cil_types.assigns -> Cil_types.assigns
val merge_assigns : Cil_types.assigns -> Cil_types.assigns -> Cil_types.assigns
val concat_allocation : Cil_types.allocation -> Cil_types.allocation -> Cil_types.allocation
val merge_allocation : Cil_types.allocation -> Cil_types.allocation -> Cil_types.allocation
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.oldloc
.val clear_funspec : Cil_types.funspec -> unit
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
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
val constFoldTermToInt : ?machdep:bool -> Cil_types.term -> Integer.t option
class simplify_const_lval :(Cil_types.varinfo -> Cil_types.init option) ->
Cil.cilVisitor
cilVisitor
(by copy) that simplifies expressions of the type
const int x = v
, where v
is an integer and x
is a global variable.
val complete_types : Cil_types.file -> unit
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