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 coerce_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.
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
val pointer_comparable : ?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
val expr_to_term : ?coerce:bool -> Cil_types.exp -> Cil_types.term
~coerce
flag as follows:~coerce:false
is given (the default) the term has the same
c-type as the original expression.~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.int
or an integer
depending on the ~coerce
flag.
To obtain a boolean or predicate, use expr_to_boolean
or
expr_to_predicate
instead.val expr_to_predicate : Cil_types.exp -> Cil_types.predicate
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
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
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).val scalar_term_to_boolean : Cil_types.term -> Cil_types.term
e <> 0
as a boolean term.Fatal
error if the argument cannot be compared to 0val 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 : 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
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.
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 is_annot_next_stmt : Cil_types.code_annotation -> bool
val 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