diff --git a/src/plugins/e-acsl/mmodel_translate.ml b/src/plugins/e-acsl/mmodel_translate.ml
index 1172ffc3301e07e4f97a0d8513220b66b5794219..48d63f64c47cae30751f953d22a4ecd5edb11d46 100644
--- a/src/plugins/e-acsl/mmodel_translate.ml
+++ b/src/plugins/e-acsl/mmodel_translate.ml
@@ -115,8 +115,7 @@ let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
let call ~loc kf name ctx env t =
assert (name = "base_addr" || name = "block_length"
|| name = "offset" || name ="freeable");
- let term_to_exp = !term_to_exp_ref in
- let e, env = term_to_exp kf (Env.rte env true) t in
+ let e, env = !term_to_exp_ref kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
@@ -135,10 +134,38 @@ let call ~loc kf name ctx env t =
(********************** \initialized, \valid, \valid_read ********************)
(*****************************************************************************)
-(* Call to [__e_acsl_<name>] for terms of the form [p + r]
+(* Take the term [size] thas has been typed into GMP
+ and return an expression of type [size_t].
+ The case where [!(0 <= size < SIZE_MAX)] is an UB ==> guard against it. *)
+let gmp_to_sizet ~loc kf env size p =
+ let sizet = Cil.(theMachine.typeOfSizeOf) in
+ (* The guard *)
+ let sizet_max = Logic_const.tint
+ ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
+ in
+ let guard_upper = Logic_const.prel ~loc (Rlt, size, sizet_max) in
+ let guard_lower = Logic_const.prel ~loc (Rle, Cil.lzero ~loc (), size) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ Typing.type_named_predicate ~must_clear:false guard;
+ let guard, env = !predicate_to_exp_ref kf env guard in
+ (* Translate term [size] into an exp of type [size_t] *)
+ let size, env = !term_to_exp_ref kf env size in
+ let _, e, env = Env.new_var
+ ~loc
+ ~name:"size"
+ env
+ None
+ sizet
+ (fun vi _ ->
+ [ Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf guard p;
+ Misc.mk_call ~loc ~result:(Cil.var vi) "__gmpz_get_ui" [ size ] ])
+ in
+ e, env
+
+(* Call to [__e_acsl_<name>] for terms of the form [ptr + r]
when [<name> = valid or initialized or valid_read] and
- where [p] is an address and [r] a range offset *)
-let call_memory_block ~loc kf name ctx env p r =
+ where [ptr] is an address and [r] a range offset *)
+let call_memory_block ~loc kf name ctx env ptr r p =
let n1, n2 = match r.term_node with
| Trange(Some n1, Some n2) ->
n1, n2
@@ -148,7 +175,7 @@ let call_memory_block ~loc kf name ctx env p r =
assert false
in
(* s *)
- let ty = match Cil.unrollType (Misc.cty p.term_type) with
+ let ty = match Cil.unrollType (Misc.cty ptr.term_type) with
| TPtr(ty, _) | TArray(ty, _, _, _) -> ty
| _ -> assert false
in
@@ -159,7 +186,7 @@ let call_memory_block ~loc kf name ctx env p r =
~loc
(TBinOp(
PlusPI,
- Logic_utils.mk_cast ~loc ~force:false typ_charptr p,
+ Logic_utils.mk_cast ~loc ~force:false typ_charptr ptr,
Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
(Ctype typ_charptr)
in
@@ -167,20 +194,29 @@ let call_memory_block ~loc kf name ctx env p r =
let term_to_exp = !term_to_exp_ref in
let ptr, env = term_to_exp kf (Env.rte env true) ptr in
(* size *)
- let size = Logic_const.term
- ~loc
- (TBinOp(
- Mult,
- s,
- Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
- Linteger
+ let size_term =
+ (* Since [s] and [n1] have been typed through [ptr],
+ we need to clone them in order to force retyping *)
+ let s = { s with term_node = s.term_node } in
+ let n1 = { n1 with term_node = n1.term_node } in
+ Logic_const.term
+ ~loc
+ (TBinOp(
+ Mult,
+ s,
+ Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
+ Linteger
+ in
+ Typing.type_term ~use_gmp_opt:false size_term;
+ let size, env = match Typing.get_integer_ty size_term with
+ | Typing.Gmp ->
+ gmp_to_sizet ~loc kf env size_term p
+ | Typing.C_type _ ->
+ let size, env = term_to_exp kf env size_term in
+ Cil.constFold false size, env
+ | Typing.Other ->
+ assert false
in
- let ctx_ity = Typing.integer_ty_of_typ ctx in
- Typing.type_term ~use_gmp_opt:false ~ctx:ctx_ity size;
- let ity = Typing.get_integer_ty size in
- if ity = Typing.gmp then Error.not_yet "size of memory area in GMP";
- let size, env = term_to_exp kf env size in
- let size = Cil.constFold false size in
(* base and base_addr *)
let base, _ = Misc.ptr_index ~loc ptr in
let base_addr = match base.enode with
@@ -209,7 +245,7 @@ let call_memory_block ~loc kf name ctx env p r =
(* [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
+ A: [\builtin(ptr+r)] where [ptr] is an address and [r] a range or
[\builtin(t[r])] or
[\builtin(t[i_1]...[i_n])] where [t] is dynamically allocated
and all the indexes are integers,
@@ -226,22 +262,22 @@ let call_memory_block ~loc kf name ctx env p r =
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] *)
-let call_with_ranges ~loc kf name ctx env t call_default =
+let call_with_ranges ~loc kf name ctx env t p call_default =
if Misc.is_bitfield_pointers t.term_type then
Error.not_yet "bitfield pointer";
match t.term_node with
- | TBinOp((PlusPI | IndexPI), p, ({ term_node = Trange _ } as r)) ->
- if Misc.is_set_of_ptr_or_array p.term_type then
+ | TBinOp((PlusPI | IndexPI), ptr, ({ term_node = Trange _ } as r)) ->
+ if Misc.is_set_of_ptr_or_array ptr.term_type then
Error.not_yet "arithmetic over set of pointers or arrays"
else
(* Case A *)
- call_memory_block ~loc kf name ctx env p r
+ call_memory_block ~loc kf name ctx env ptr r p
| 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
- call_memory_block ~loc kf name ctx env p r
+ let ptr = Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset in
+ call_memory_block ~loc kf name ctx env ptr r p
| TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as lv), toffset) ->
if has_set_as_index toffset then
(* Case B *)
@@ -279,8 +315,7 @@ let call_with_ranges ~loc kf name ctx env t call_default =
quantifiers
in
Typing.type_named_predicate ~must_clear:true p_quantified;
- let named_predicate_to_exp = !predicate_to_exp_ref in
- named_predicate_to_exp kf env p_quantified
+ !predicate_to_exp_ref kf env p_quantified
with Range_elimination_exception ->
(* Case C *)
call_default ~loc kf name ctx env t
@@ -292,7 +327,7 @@ let call_with_ranges ~loc kf name ctx env t call_default =
call_default ~loc kf name ctx env t
(* \initialized *)
-let call_with_size ~loc kf name ctx env t =
+let call_with_size ~loc kf name ctx env t p =
assert (name = "initialized");
let call_for_unsupported_constructs ~loc kf name ctx env t =
let term_to_exp = !term_to_exp_ref in
@@ -319,10 +354,11 @@ let call_with_size ~loc kf name ctx env t =
ctx
env
t
+ p
call_for_unsupported_constructs
(* \valid and \valid_read *)
-let call_valid ~loc kf name ctx env t =
+let call_valid ~loc kf name ctx env t p =
assert (name = "valid" || name = "valid_read");
let call_for_unsupported_constructs ~loc kf name ctx env t =
let term_to_exp = !term_to_exp_ref in
@@ -356,4 +392,5 @@ let call_valid ~loc kf name ctx env t =
ctx
env
t
+ p
call_for_unsupported_constructs
\ No newline at end of file
diff --git a/src/plugins/e-acsl/mmodel_translate.mli b/src/plugins/e-acsl/mmodel_translate.mli
index eeed2bc11209b0171d49cc813671b23e8451dc83..ee4999d28d6ab671f12fca46cf798d4dafe6d389 100644
--- a/src/plugins/e-acsl/mmodel_translate.mli
+++ b/src/plugins/e-acsl/mmodel_translate.mli
@@ -35,19 +35,21 @@ val call:
val call_with_size:
loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
- exp * Env.t
-(* [call_with_size ~loc kf name ctx env t] creates a call to the E-ACSL memory
- builtin identified by [name] which requires two arguments, namely
+ predicate -> exp * Env.t
+(* [call_with_size ~loc kf name ctx env t p] creates a call to the E-ACSL
+ memory builtin identified by [name] which requires two arguments, namely
the pointer under study and a size in bytes.
The only supported builtin is: [initialized].
- [t] can denote ranges of memory locations. *)
+ [t] can denote ranges of memory locations.
+ [p] is the predicate under testing. *)
val call_valid:
loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
- exp * Env.t
-(* [call_valid ~loc kf name ctx env t] creates a call to the E-ACSL memory
+ predicate -> exp * Env.t
+(* [call_valid ~loc kf name ctx env t p] creates a call to the E-ACSL memory
builtin [valid] or [valid_read] according to [name].
- [t] can denote ranges of memory locations. *)
+ [t] can denote ranges of memory locations.
+ [p] is the predicate under testing. *)
(**************************************************************************)
(********************** Forward references ********************************)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c
index 5686c529134aef4475afb4ed4b4715a78eeb0a3f..c632c606306cc8df1e4fb37ece7bcb7c8cf0a99d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c
@@ -14,6 +14,18 @@ void f(char *s, long n)
return;
}
+/*@ requires \valid(ptr + (0 .. size - 1));
+ ensures ¬\valid(\old(ptr) + (0 .. \old(size) + 1));
+ */
+void __gen_e_acsl_g(long *ptr, size_t size);
+
+void g(long *ptr, size_t size)
+{
+ __e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __e_acsl_delete_block((void *)(& ptr));
+ return;
+}
+
int main(void)
{
int __retres;
@@ -39,17 +51,17 @@ int main(void)
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)a + 4 * 0),
(size_t)16,(void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a + (0 .. 4))",13);
+ (char *)"\\valid(a + (0 .. 4))",19);
}
int j = 2;
/*@ assert \valid(a + (4 .. 8 + j)); */
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)a + 4 * 4),
- (size_t)((int)(4 * ((8L + j) - 4))),
+ (size_t)(4L * ((8L + j) - 4L)),
(void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a + (4 .. 8 + j))",15);
+ (char *)"\\valid(a + (4 .. 8 + j))",21);
}
/*@ assert ¬\valid(a + (10 .. 11)); */
{
@@ -57,7 +69,7 @@ int main(void)
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)((char *)a + 4 * 10),
(size_t)4,(void *)a,(void *)(& a));
__e_acsl_assert(! __gen_e_acsl_valid_3,(char *)"Assertion",
- (char *)"main",(char *)"!\\valid(a + (10 .. 11))",16);
+ (char *)"main",(char *)"!\\valid(a + (10 .. 11))",22);
}
free((void *)a);
__e_acsl_full_init((void *)(& b));
@@ -68,7 +80,7 @@ int main(void)
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),(size_t)10,
(void *)b,(void *)(& b));
__e_acsl_assert(__gen_e_acsl_valid_4,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(b + (0 .. 10))",21);
+ (char *)"\\valid(b + (0 .. 10))",27);
}
/*@ assert ¬\valid(b + (11 .. 15)); */
{
@@ -76,7 +88,7 @@ int main(void)
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 11),(size_t)4,
(void *)b,(void *)(& b));
__e_acsl_assert(! __gen_e_acsl_valid_5,(char *)"Assertion",
- (char *)"main",(char *)"!\\valid(b + (11 .. 15))",22);
+ (char *)"main",(char *)"!\\valid(b + (11 .. 15))",28);
}
long t[3] = {7l, 8l, 9l};
__e_acsl_store_block((void *)(t),(size_t)24);
@@ -87,7 +99,7 @@ int main(void)
__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);
+ (char *)"\\valid(&t[0 .. 2])",31);
}
/*@ assert ¬\valid(&t[3 .. 5]); */
{
@@ -95,8 +107,9 @@ int main(void)
__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);
+ (char *)"main",(char *)"!\\valid(&t[3 .. 5])",32);
}
+ __gen_e_acsl_g(t,(unsigned long)3);
__e_acsl_initialize((void *)(t2),sizeof(double));
t2[0] = 0.5;
__e_acsl_initialize((void *)(& t2[1]),sizeof(double));
@@ -108,7 +121,7 @@ int main(void)
8 * 0),
(size_t)8);
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&t2[0 .. 1])",31);
+ (char *)"main",(char *)"\\initialized(&t2[0 .. 1])",38);
}
/*@ assert ¬\initialized(&t2[2 .. 3]); */
{
@@ -117,7 +130,7 @@ int main(void)
8 * 2),
(size_t)8);
__e_acsl_assert(! __gen_e_acsl_initialized_2,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&t2[2 .. 3])",32);
+ (char *)"main",(char *)"!\\initialized(&t2[2 .. 3])",39);
}
/*@ assert ¬\initialized(b + (0 .. 10)); */
{
@@ -126,7 +139,7 @@ int main(void)
(size_t)10);
__e_acsl_assert(! __gen_e_acsl_initialized_3,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(b + (0 .. 10))",
- 34);
+ 41);
}
free((void *)b);
int n = 2;
@@ -169,7 +182,7 @@ int main(void)
e_acsl_end_loop2: ;
__e_acsl_assert(! __gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
(char *)"!\\initialized(&t3[n - 1 .. n + 2][1][0 .. 1])",
- 39);
+ 46);
}
/*@ assert ¬\valid_read(&t3[6][1][0] + (2 .. 10)); */
{
@@ -180,7 +193,7 @@ int main(void)
(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"main",
- (char *)"!\\valid_read(&t3[6][1][0] + (2 .. 10))",41);
+ (char *)"!\\valid_read(&t3[6][1][0] + (2 .. 10))",48);
}
/*@ assert \valid_read(&t3[n - 1 .. n + 2][1]); */
{
@@ -206,7 +219,7 @@ int main(void)
}
e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main",
- (char *)"\\valid_read(&t3[n - 1 .. n + 2][1])",42);
+ (char *)"\\valid_read(&t3[n - 1 .. n + 2][1])",49);
}
__e_acsl_initialize((void *)(& s.a[0]),sizeof(int));
s.a[0] = 7;
@@ -220,7 +233,7 @@ int main(void)
(size_t)4);
__e_acsl_assert(__gen_e_acsl_initialized_5,(char *)"Assertion",
(char *)"main",
- (char *)"\\initialized(&s.a[0] + (1 .. 2))",46);
+ (char *)"\\initialized(&s.a[0] + (1 .. 2))",53);
}
/*@ assert ¬\initialized(s.b + (0 .. 1)); */
{
@@ -230,7 +243,7 @@ int main(void)
(size_t)4);
__e_acsl_assert(! __gen_e_acsl_initialized_6,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(s.b + (0 .. 1))",
- 47);
+ 54);
}
int size1 = 5;
int size2 = 9;
@@ -252,13 +265,13 @@ int main(void)
(void *)multi_dynamic,
(void *)(& multi_dynamic));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(multi_dynamic + 4)",56);
+ (char *)"mem_access: \\valid_read(multi_dynamic + 4)",63);
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)((char *)*(multi_dynamic + 4) +
4 * 1),(size_t)24,
(void *)*(multi_dynamic + 4),
(void *)(multi_dynamic + 4));
__e_acsl_assert(__gen_e_acsl_valid_8,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(*(multi_dynamic + 4) + (1 .. 7))",56);
+ (char *)"\\valid(*(multi_dynamic + 4) + (1 .. 7))",63);
}
/*@ assert \valid(*(multi_dynamic + (2 .. 4)) + (1 .. 7)); */ ;
i --;
@@ -284,10 +297,305 @@ int main(void)
return __retres;
}
+/*@ requires \valid(ptr + (0 .. size - 1));
+ ensures ¬\valid(\old(ptr) + (0 .. \old(size) + 1));
+ */
+void __gen_e_acsl_g(long *ptr, size_t size)
+{
+ __e_acsl_mpz_t __gen_e_acsl_at_2;
+ long *__gen_e_acsl_at;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_6;
+ __gmpz_init_set_ui(__gen_e_acsl_size_6,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ __gmpz_clear(__gen_e_acsl_size_6);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_5;
+ __gmpz_init_set_ui(__gen_e_acsl_size_5,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
+ __gmpz_clear(__gen_e_acsl_size_5);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_4;
+ __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ __gmpz_clear(__gen_e_acsl_size_4);
+ }
+ __gen_e_acsl_at = ptr;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ int __gen_e_acsl_le;
+ int __gen_e_acsl_and;
+ unsigned long __gen_e_acsl_size_3;
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof,8L);
+ __gmpz_init_set_ui(__gen_e_acsl_size,size);
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_2;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_lt;
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_2,8L);
+ __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4));
+ __gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gen_e_acsl_and = __gen_e_acsl_lt < 0;
+ __gmpz_clear(__gen_e_acsl_sizeof_2);
+ __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"RTE",(char *)"g",
+ (char *)"\\valid(ptr + (0 .. size - 1))",7);
+ __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 8 * 0),
+ __gen_e_acsl_size_3,(void *)ptr,
+ (void *)(& ptr));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"g",
+ (char *)"\\valid(ptr + (0 .. size - 1))",7);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_mul);
+ }
+ g(ptr,size);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_3;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl_mul_3;
+ int __gen_e_acsl_le_2;
+ int __gen_e_acsl_and_2;
+ unsigned long __gen_e_acsl_size_7;
+ int __gen_e_acsl_valid_2;
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_3,8L);
+ __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_mul_3);
+ __gmpz_mul(__gen_e_acsl_mul_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_5));
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ if (__gen_e_acsl_le_2 <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_4;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_sub_6;
+ __e_acsl_mpz_t __gen_e_acsl_mul_4;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ int __gen_e_acsl_lt_2;
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_4,8L);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init_set_si(__gen_e_acsl__9,0L);
+ __gmpz_init(__gen_e_acsl_sub_6);
+ __gmpz_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init(__gen_e_acsl_mul_4);
+ __gmpz_mul(__gen_e_acsl_mul_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_6));
+ __gmpz_init_set_ui(__gen_e_acsl__10,18446744073709551615UL);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gen_e_acsl_and_2 = __gen_e_acsl_lt_2 < 0;
+ __gmpz_clear(__gen_e_acsl_sizeof_4);
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_sub_6);
+ __gmpz_clear(__gen_e_acsl_mul_4);
+ __gmpz_clear(__gen_e_acsl__10);
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"RTE",(char *)"g",
+ (char *)"\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",8);
+ __gen_e_acsl_size_7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at +
+ 8 * 0),
+ __gen_e_acsl_size_7,
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __e_acsl_assert(! __gen_e_acsl_valid_2,(char *)"Postcondition",
+ (char *)"g",
+ (char *)"!\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",
+ 8);
+ __e_acsl_delete_block((void *)(& ptr));
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sizeof_3);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl_mul_3);
+ __gmpz_clear(__gen_e_acsl_at_2);
+ return;
+ }
+}
+
/*@ requires ¬\valid(s + (3 .. n + 1000)); */
void __gen_e_acsl_f(char *s, long n)
{
- __e_acsl_store_block((void *)(& s),(size_t)8);
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ int __gen_e_acsl_le;
+ int __gen_e_acsl_and;
+ unsigned long __gen_e_acsl_size;
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
+ __gmpz_init_set_si(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl__2,1000L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init_set_si(__gen_e_acsl__3,3L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_2;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ int __gen_e_acsl_lt;
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_2,1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_2,n);
+ __gmpz_init_set_si(__gen_e_acsl__4,1000L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init_set_si(__gen_e_acsl__5,3L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2));
+ __gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gen_e_acsl_and = __gen_e_acsl_lt < 0;
+ __gmpz_clear(__gen_e_acsl_sizeof_2);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl__6);
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"RTE",(char *)"f",
+ (char *)"\\valid(s + (3 .. n + 1000))",5);
+ __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(s + 1 * 3),
+ __gen_e_acsl_size,(void *)s,
+ (void *)(& s));
+ __e_acsl_assert(! __gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
+ (char *)"!\\valid(s + (3 .. n + 1000))",5);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_mul);
+ }
f(s,n);
__e_acsl_delete_block((void *)(& s));
return;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
index 518f496081d4093e4591bdf88a1486cedf091b0f..465b591b22527e94c1e2353681ba04c781924dfb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
@@ -1,13 +1,10 @@
[e-acsl] beginning translation.
-[e-acsl] tests/runtime/ranges_in_builtins.c:57: Warning:
+[e-acsl] tests/runtime/ranges_in_builtins.c:64: Warning:
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
Ignoring annotation.
-[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:
+[eva:alarm] tests/runtime/ranges_in_builtins.c:19: Warning:
assertion got status unknown.
-[eva:alarm] tests/runtime/ranges_in_builtins.c:15: Warning:
+[eva:alarm] tests/runtime/ranges_in_builtins.c:21: Warning:
assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c b/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
index d3079652ccc099e02ddae76d636a935c33ec5415..7c94e87d3ceb3f39f32c651abca2c300842dd83a 100644
--- a/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
@@ -4,6 +4,12 @@
#include "stdlib.h"
/*@ requires !\valid(s + (3..n+1000)); */
void f(char *s, long n){}
+/*@ requires \valid(ptr + (0 .. size - 1));
+ ensures ! \valid(ptr + (0 .. size + 1));
+ // In pure ACSL, the following predicate is true;
+ // however at runtime, its evalulation results in UB ==> false.
+ // ensures ! \valid(ptr + (0 .. SIZE_MAX*SIZE_MAX)); */
+void g(long *ptr, size_t size) { }
extern void *malloc(size_t p);
extern void free(void* p);
struct S { int a[2]; float *b; float *c;};
@@ -24,6 +30,7 @@ int main(void) {
long t[3] = {7l, 8l, 9l};
/*@ assert \valid(&t[0..2]); */ ;
/*@ assert !\valid(&t[3..5]); */ ;
+ g(t, 3);
double t2[4];
t2[0] = 0.5;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index ea705404682cc69bcfe7e055ad1b4662cff5d2f4..4fc4f50e6201997a2bb714a745dc15ca0e331f6d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -7,21 +7,12 @@
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:
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 037ac3a4dbfc5d726e86a1ae6933835663e69c90..5d44cafba2c38b984faa2f076c858837305a67c5 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -732,7 +732,7 @@ and named_predicate_content_to_exp ?name kf env p =
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
now convert this right-most valid. *)
is_visiting_valid := false;
- call_valid t
+ call_valid t p
end else begin
match t.term_node, t.term_type with
| TLval tlv, Ctype ty ->
@@ -744,7 +744,7 @@ and named_predicate_content_to_exp ?name kf env p =
is_visiting_valid := true;
named_predicate_to_exp kf env p
| _ ->
- call_valid t
+ call_valid t p
end
| Pvalid _ -> not_yet env "labeled \\valid"
| Pvalid_read _ -> not_yet env "labeled \\valid_read"
@@ -763,7 +763,8 @@ and named_predicate_content_to_exp ?name kf env p =
"initialized"
Cil.intType
env
- t)
+ t
+ p)
| Pinitialized _ -> not_yet env "labeled \\initialized"
| Pallocable _ -> not_yet env "\\allocate"
| Pfreeable(BuiltinLabel Here, t) ->