Commit 2567cf83 authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica
Browse files

Addresses Julien's review no.2:

 - Remove double warning for arithmetic over pointers
 - Not yet: size of memory area in GMP
 - Typing of Trange
 - Squashing pattern matchings
 - Use of has_set_as_index
 - No is_offset_of_array
 - Using exception in is_range_free
 - Using `call f`
 - Logic.is_set_type instead of catching Failure
 - Logic.const.taddrof
 - &t, instead of &t[0], is sufficient for arrays
 - No useless rec
 - Typos, useless parentheses, no camel case, comments, indentation
parent 07718350
......@@ -252,25 +252,25 @@ let term_of_li li = match li.l_body with
Options.fatal "li.l_body does not match LBterm(t) in Misc.term_of_li"
let is_set_of_ptr_or_array lty =
try
if Logic_const.is_set_type lty then
let lty = Logic_const.type_of_element lty in
(Logic_utils.isLogicPointerType lty) || (Logic_utils.isLogicArrayType lty)
with Failure _ ->
Logic_utils.isLogicPointerType lty || Logic_utils.isLogicArrayType lty
else
false
exception Range_found_exception
let is_range_free t =
let res_ref = ref true in
let has_range_visitor = object inherit Visitor.frama_c_inplace
method !vterm t = match t.term_node with
| Trange _ ->
res_ref := false;
Cil.SkipChildren
| _ ->
Cil.DoChildren
end
in
ignore (Visitor.visitFramacTerm has_range_visitor t);
!res_ref
try
let has_range_visitor = object inherit Visitor.frama_c_inplace
method !vterm t = match t.term_node with
| Trange _ -> raise Range_found_exception
| _ -> Cil.DoChildren
end
in
ignore (Visitor.visitFramacTerm has_range_visitor t);
true
with Range_found_exception ->
false
(*
Local Variables:
......
......@@ -105,7 +105,7 @@ val term_of_li: logic_info -> term
and returns [t]. *)
val is_set_of_ptr_or_array: logic_type -> bool
(* Checks whehter the given logic type is a set of pointers. *)
(* Checks whether the given logic type is a set of pointers. *)
val is_range_free: term -> bool
(* Returns [true] iff the given term does not contain any range. *)
......
......@@ -303,12 +303,13 @@ module rec Transfer
match t2.term_type with
| Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
| _ ->
if (Misc.is_set_of_ptr_or_array t1.term_type) ||
(Misc.is_set_of_ptr_or_array t2.term_type) then
if Misc.is_set_of_ptr_or_array t1.term_type ||
Misc.is_set_of_ptr_or_array t2.term_type then
(* Occurs for example from:
\valid(&multi_dynamic[2..4][1..7])
where multi_dynamic has been dynamically allocated *)
Error.not_yet "arithmetic over set of pointers or arrays"
\valid(&multi_dynamic[2..4][1..7])
where multi_dynamic has been dynamically allocated *)
let varinfos = register_term kf varinfos t1 in
register_term kf varinfos t2
else
assert false)
| TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
......@@ -329,7 +330,11 @@ module rec Transfer
| Tunion _ -> Error.not_yet "set union"
| Tinter _ -> Error.not_yet "set intersection"
| Tcomprehension _ -> Error.not_yet "set comprehension"
| Trange _ -> Error.not_yet "\\range"
| Trange(Some t1, Some t2) ->
let varinfos = register_term kf varinfos t1 in
register_term kf varinfos t2
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSL"
and register_body kf varinfos = function
| LBnone | LBreads _ -> varinfos
......
......@@ -6,6 +6,14 @@ struct S {
float *b ;
float *c ;
};
/*@ requires ¬\valid(s + (3 .. n + 1000)); */
void __gen_e_acsl_f(char *s, long n);
void f(char *s, long n)
{
return;
}
int main(void)
{
int __retres;
......@@ -76,16 +84,16 @@ int main(void)
/*@ assert \valid(&t[0 .. 2]); */
{
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(t) + 8 * 0),
(size_t)16,(void *)(t),(void *)(t));
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(& t) + 8 * 0),
(size_t)16,(void *)(& t),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_6,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&t[0 .. 2])",25);
}
/*@ assert ¬\valid(&t[3 .. 5]); */
{
int __gen_e_acsl_valid_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(t) + 8 * 3),
(size_t)16,(void *)(t),(void *)(t));
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(& t) + 8 * 3),
(size_t)16,(void *)(& t),(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_7,(char *)"Assertion",
(char *)"main",(char *)"!\\valid(&t[3 .. 5])",26);
}
......@@ -96,7 +104,7 @@ int main(void)
/*@ assert \initialized(&t2[0 .. 1]); */
{
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(t2) +
__gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 0),
(size_t)8);
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
......@@ -105,7 +113,7 @@ int main(void)
/*@ assert ¬\initialized(&t2[2 .. 3]); */
{
int __gen_e_acsl_initialized_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(t2) +
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 2),
(size_t)8);
__e_acsl_assert(! __gen_e_acsl_initialized_2,(char *)"Assertion",
......@@ -259,7 +267,12 @@ int main(void)
i --;
}
free((void *)multi_dynamic);
char c = (char)'w';
__e_acsl_store_block((void *)(& c),(size_t)1);
__e_acsl_full_init((void *)(& c));
__gen_e_acsl_f(& c,(long)5);
__retres = 0;
__e_acsl_delete_block((void *)(& c));
__e_acsl_delete_block((void *)(& multi_dynamic));
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(t3));
......@@ -271,4 +284,13 @@ int main(void)
return __retres;
}
/*@ requires ¬\valid(s + (3 .. n + 1000)); */
void __gen_e_acsl_f(char *s, long n)
{
__e_acsl_store_block((void *)(& s),(size_t)8);
f(s,n);
__e_acsl_delete_block((void *)(& s));
return;
}
......@@ -3,9 +3,8 @@
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/ranges_in_builtins.c:57: Warning:
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
[e-acsl] tests/runtime/ranges_in_builtins.c:5: Warning:
E-ACSL construct `size of memory area in GMP' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/runtime/ranges_in_builtins.c:13: Warning:
......
/* run.config
COMMENT: ranges in a few builtins
*/
#include "stdlib.h"
/*@ requires !\valid(s + (3..n+1000)); */
void f(char *s, long n){}
extern void *malloc(size_t p);
extern void free(void* p);
struct S { int a[2]; float *b; float *c;};
......@@ -60,4 +60,7 @@ int main(void) {
free(multi_dynamic[i]);
}
free(multi_dynamic);
char c = 'w';
f(&c, 5);
}
\ No newline at end of file
......@@ -154,6 +154,7 @@ int main(void)
__e_acsl_temporal_store_nblock((void *)(& q),(void *)*(& q));
__e_acsl_temporal_store_nblock((void *)p,(void *)(& a));
__e_acsl_initialize((void *)p,sizeof(int *));
/*@ assert Value: mem_access: \valid(p); */
*p = & a;
__e_acsl_temporal_store_nblock((void *)(p + 1),(void *)(& a));
__e_acsl_initialize((void *)(p + 1),sizeof(int *));
......@@ -236,6 +237,8 @@ int main(void)
else __gen_e_acsl_and_10 = 0;
__e_acsl_assert(__gen_e_acsl_and_10,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q)",44);
/*@ assert Value: initialization: \initialized(q); */
/*@ assert Value: mem_access: \valid_read(q); */
__gen_e_acsl_valid_9 = __e_acsl_valid((void *)*q,sizeof(int),
(void *)*q,(void *)q);
__gen_e_acsl_and_11 = __gen_e_acsl_valid_9;
......@@ -259,6 +262,8 @@ int main(void)
(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q + 1)",45);
/*@ assert Value: initialization: \initialized(q + 1); */
/*@ assert Value: mem_access: \valid_read(q + 1); */
__gen_e_acsl_valid_10 = __e_acsl_valid((void *)*(q + 1),sizeof(int),
(void *)*(q + 1),
(void *)(q + 1));
......@@ -273,6 +278,7 @@ int main(void)
tmp_1 = (int *)0;
__e_acsl_temporal_store_nreferent((void *)(q + 1),(void *)(& tmp_1));
__e_acsl_initialize((void *)(q + 1),sizeof(int *));
/*@ assert Value: mem_access: \valid(q + 1); */
*(q + 1) = tmp_1;
__e_acsl_temporal_store_nreferent((void *)q,(void *)(& tmp_1));
__e_acsl_initialize((void *)q,sizeof(int *));
......
......@@ -7,12 +7,21 @@
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:78: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
E-ACSL construct `size of memory area in GMP' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:104: Warning:
E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:78: Warning:
E-ACSL construct `size of memory area in GMP' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:79: Warning:
E-ACSL construct `size of memory area in GMP' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:81: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:81: Warning:
......
......@@ -39,6 +39,89 @@ let handle_error f env =
It is [true] iff we are currently visiting \valid. *)
let is_visiting_valid = ref false
(*****************************************************************************)
(*************************** Ranges in a few builtins ************************)
(*****************************************************************************)
(* We call Range Elimination the operation through which ranges are
substituted by universally quantified logic variables.
Example:
[\valid(&t[(n-1)..(n+2)][1][0..1])] can be soundly transformed into
[\forall integer q1; n-1 <= q1 <= n+2 ==>
\forall integer q2; 0 <= q2 <= 1 ==>
\valid(&t[q1][1][q2])]
However, the substition can be unsound,
in which case [Range_elimination_exception] must be raised.
Example:
[\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
since [==] refers to set equality when applied on ranges.
But Range Elimination will give a predicate equivalent to [\valid(&t[1])]
since [\forall 0 <= q1,q2 <= 2: q1==q2] is false.
Hence [Range_elimination_exception] must be raised. *)
exception Range_elimination_exception
(* Takes a [toffset] and checks whether it contains an index that is a set *)
let rec has_set_as_index = function
| TNoOffset ->
false
| TIndex(t, toffset) ->
Logic_const.is_set_type t.term_type || has_set_as_index toffset
| TModel(_, toffset) | TField(_, toffset) ->
has_set_as_index toffset
(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
Raises [Range_elimination_exception] if whether the operation is unsound or
if we don't support the construction yet. *)
let eliminate_ranges_from_index_of_term ~loc t =
match t.term_node with
| Trange(Some n1, Some n2) ->
let name = Env.Varname.get ~scope:Env.Local_block "range" in
let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
let tlv = Logic_const.tvar ~loc lv in
tlv, (n1, lv, n2)
| TBinOp(PlusA, _, {term_node = Trange _}) ->
(* t[n + (0..3)] results in a typing error:
arithmetic conversion between non arithmetic types int and set<ℤ> *)
assert false
| _ ->
raise Range_elimination_exception
(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
Raises [Range_elimination_exception], through [eliminate_ranges_from_
index_of_term], if whether the operation is unsound or
if we don't support the construction yet. *)
let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
match toffset with
| TIndex(t, TNoOffset) ->
if Misc.is_range_free t then
toffset, quantifiers
else
(* Attempt Range Elimination on [t] *)
let t', q = eliminate_ranges_from_index_of_term ~loc t in
TIndex(t', TNoOffset), q :: quantifiers
| TIndex(t, toffset') ->
if Misc.is_range_free t then
let toffset', quantifiers' =
eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
in
TIndex(t, toffset'), quantifiers'
else
(* Attempt Range Elimination on [t] *)
let t1, quantifiers1 =
eliminate_ranges_from_index_of_term ~loc t
in
let toffset2, quantifiers2 =
eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
in
let toffset3 = TIndex(t1, toffset2) in
toffset3, quantifiers1 :: quantifiers2
| TNoOffset ->
toffset, quantifiers
| TModel _ ->
Error.not_yet "range elimination on TModel"
| TField _ ->
Error.not_yet "range elimination on TField"
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
......@@ -224,23 +307,6 @@ let cast_integer_to_float lty lty_t e =
else
e
(* We call Range Elimination the operation through which ranges are
substituted by universally quantified logic variables.
Example:
[\valid(&t[(n-1)..(n+2)][1][0..1])] can be soundly transformed into
[\forall integer q1; n-1 <= q1 <= n+2 ==>
\forall integer q2; 0 <= q2 <= 1 ==>
\valid(&t[q1][1][q2])]
However, the substition can be unsound,
in which case [RangeEliminationException] must be raised.
Example:
[\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
since [==] refers to set equality when applied on ranges.
But Range Elimination will give a predicate equivalent to [\valid(&t[1])]
since [\forall 0 <= q1,q2 <= 2: q1==q2] is false.
Hence [RangeEliminationException] must be raised. *)
exception RangeEliminationException
let rec thost_to_host kf env = function
| TVar { lv_origin = Some v } ->
Var (Cil.get_varinfo (Env.get_behavior env) v), env, v.vname
......@@ -428,9 +494,11 @@ and context_insensitive_term_to_exp kf env t =
(* other logic/arith operators *)
not_yet env "missing binary bitwise operator"
| TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
if (Misc.is_set_of_ptr_or_array t1.term_type) ||
(Misc.is_set_of_ptr_or_array t2.term_type) then
Error.not_yet "arithmetic over set of pointers or arrays";
if Misc.is_set_of_ptr_or_array t1.term_type ||
Misc.is_set_of_ptr_or_array t2.term_type then
(* case of arithmetic over set of pointers (due to use of ranges)
should have already been handled in [mmodel_call_with_ranges] *)
assert false;
(* binary operation over pointers *)
let ty = match t1.term_type with
| Ctype ty -> ty
......@@ -602,155 +670,134 @@ and mk_ptr_sizeof typ loc =
and mmodel_call_with_size ~loc kf name ctx env t =
mmodel_call_with_ranges ~loc kf name ctx env t
begin fun ~loc kf name ctx env t ->
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env
end
and mmodel_call_valid ~loc kf name ctx env t =
mmodel_call_with_ranges ~loc kf name ctx env t
begin fun ~loc kf name ctx env t ->
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index ~loc e in
let base_addr = match base.enode with
| AddrOf _ | Const _ -> Cil.zero ~loc
| Lval(lv) | StartOf(lv) -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
let args = [ e; sizeof; base; base_addr ] in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index ~loc e in
let base_addr = match base.enode with
| AddrOf _ | Const _ -> Cil.zero ~loc
| Lval(lv) | StartOf(lv) -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
let args = [ e; sizeof; base; base_addr ] in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env
end
(* [mmodel_call_with_ranges] attempts to handle ranges in [t]
when calling builtin [name].
[mmodel_call_with_ranges] supports the following cases:
(* [mmodel_call_with_ranges] handles ranges in [t] when calling builtin [name].
It only supports the following cases for the time being:
A: [\builtin(p+r)] where [p] is an address and [r] a range or
[\builtin(t[r])] or
[\builtin(t[i_1]...[i_n])] where all the indexes are integers,
except the last one which is a range,
and [t] is dynamically allocated
[\builtin(t[i_1]...[i_n])] where [t] is dynamically allocated
and all the indexes are integers,
except the last one which is a range
The generated code is a SINGLE call to the corresponding E-ACSL builtin
B: [\builtin(t[i_1]...[i_n])] where the indexes are integers or ranges
and [t] is NOT dynamically allocated
B: [\builtin(t[i_1]...[i_n])] where [t] is NOT dynamically allocated
and the indexes are integers or ranges
The generated code is a SET OF calls to the corresponding E-ACSL builtin
C: Default case/Unsupported cases
[mmodel_call_with_ranges] will simply make E-ACSL behave as before
through [mmodel_call_default] for soundness and
for backward compatibility *)
C: Any other use of ranges/No range
Call [mmodel_call_default] which performs the translation for
range free terms, and raises Not_yet if it ever encouters a range.
Example for case:
A: [\valid(&t[3..5])]
Contiguous locations -> a single call to [__e_acsl_valid]
B: [\valid(&t[4][3..5][2])]
NON-contiguous locations -> multiple calls (3) to [__e_acsl_valid] *)
and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
match t.term_node with
| TAddrOf(thost, toffset) ->
begin match thost, toffset with
| TVar lv, TIndex(r, TNoOffset) ->
begin match r.term_node with
| Trange _ ->
(* Case A *)
let lty_noset =
try Logic_const.type_of_element t.term_type
with Failure _ -> assert false (* due to the range *)
in
let p = Logic_const.term
~loc
(TAddrOf(TVar lv, TIndex(Logic_const.tinteger ~loc 0, TNoOffset)))
lty_noset
in
mmodel_call_memory_block ~loc kf name ctx env p r
| _ ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
end
| TVar lv, toffset ->
if is_offset_of_array toffset && not (Misc.is_range_free t) then
(* Case B *)
begin try
let toffset', quantifiers =
eliminate_ranges_from_index_offset_of_array ~loc toffset []
in
let lty_noset =
try Logic_const.type_of_element t.term_type
with Failure _ -> t.term_type
in
let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
let p_quantified = match name with
| "valid" ->
Logic_const.pvalid ~loc (Logic_const.here_label, t')
| "initialized" ->
Logic_const.pinitialized ~loc (Logic_const.here_label, t')
| "valid_read" ->
Logic_const.pvalid_read ~loc (Logic_const.here_label, t')
| _ as s ->
Options.fatal "unexpected builtin %s during range elimination" s
| TBinOp((PlusPI | IndexPI), p, ({term_node = Trange _} as r)) ->
if Misc.is_set_of_ptr_or_array p.term_type then
not_yet env "arithmetic over set of pointers or arrays"
else
(* Case A *)
mmodel_call_memory_block ~loc kf name ctx env p r
| TAddrOf(TVar lv, TIndex({ term_node = Trange _ } as r, TNoOffset)) ->
(* Case A *)
assert (Logic_const.is_set_type t.term_type);
let lty_noset = Logic_const.type_of_element t.term_type in
let p = Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset in
mmodel_call_memory_block ~loc kf name ctx env p r
| TAddrOf(TVar ({lv_type = Ctype (TArray _)} as lv), toffset) ->
if has_set_as_index toffset then
(* Case B *)
begin try
let toffset', quantifiers =
eliminate_ranges_from_index_of_toffset ~loc toffset []
in
let lty_noset =
if Logic_const.is_set_type t.term_type then
Logic_const.type_of_element t.term_type
else
t.term_type
in
let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
let p_quantified =
let loc = Some (loc :> Cil_types.location) in
let call f = f ?loc (Logic_const.here_label, t') in
match name with
| "valid" -> call Logic_const.pvalid
| "initialized" -> call Logic_const.pinitialized
| "valid_read" -> call Logic_const.pvalid_read
| _ -> Options.fatal "[mmodel_call_with_ranges] unexpected builtin"
in
let p_quantified = List.fold_left
(fun p (tmin, lv, tmax) ->
(* \forall integer tlv; tmin <= tlv <= tmax ==> p *)
let tlv = Logic_const.tvar ~loc lv in
let bound1 = Logic_const.prel ~loc (Rle, tmin, tlv) in
let bound2 = Logic_const.prel ~loc (Rle, tlv, tmax) in
let bound = Logic_const.pand ~loc (bound1, bound2) in
let lower_bound = Logic_const.prel ~loc (Rle, tmin, tlv) in
let upper_bound = Logic_const.prel ~loc (Rle, tlv, tmax) in
let bound = Logic_const.pand ~loc (lower_bound, upper_bound) in
let bound_imp_p = Logic_const.pimplies ~loc (bound, p) in
Logic_const.pforall ~loc ([lv], bound_imp_p))
p_quantified
quantifiers
in
Typing.type_named_predicate ~must_clear:true p_quantified;
let e, env = named_predicate_to_exp kf env p_quantified in
e, env
with RangeEliminationException ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
end
else
(* Case C *)