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 be415a777f7fb66cf91060d6acf4cfa2fe63d271..3ab8f51b1b5c794751636bf00dccf01b91b52a22 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
@@ -19,8 +19,7 @@ int main(void)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)a + 4 * 0),
- (size_t)(4 * (4 - 0)),(void *)a,
- (void *)(& a));
+ (size_t)16,(void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(a + (0 .. 4))",13);
}
@@ -38,8 +37,7 @@ int main(void)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)((char *)a + 4 * 10),
- (size_t)(4 * (11 - 10)),(void *)a,
- (void *)(& a));
+ (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);
}
@@ -49,18 +47,16 @@ int main(void)
/*@ assert \valid(b + (0 .. 10)); */
{
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),
- (size_t)(1 * (10 - 0)),(void *)b,
- (void *)(& b));
+ __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);
}
/*@ assert ¬\valid(b + (11 .. 15)); */
{
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 11),
- (size_t)(1 * (15 - 11)),(void *)b,
- (void *)(& b));
+ __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);
}
@@ -71,8 +67,7 @@ int main(void)
{
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(t) + 8 * 0),
- (size_t)(8 * (2 - 0)),(void *)(t),
- (void *)(t));
+ (size_t)16,(void *)(t),(void *)(t));
__e_acsl_assert(__gen_e_acsl_valid_6,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&t[0 .. 2])",25);
}
@@ -80,8 +75,7 @@ int main(void)
{
int __gen_e_acsl_valid_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(t) + 8 * 3),
- (size_t)(8 * (5 - 3)),(void *)(t),
- (void *)(t));
+ (size_t)16,(void *)(t),(void *)(t));
__e_acsl_assert(! __gen_e_acsl_valid_7,(char *)"Assertion",
(char *)"main",(char *)"!\\valid(&t[3 .. 5])",26);
}
@@ -94,7 +88,7 @@ int main(void)
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(t2) +
8 * 0),
- (size_t)(8 * (1 - 0)));
+ (size_t)8);
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
(char *)"main",(char *)"\\initialized(&t2[0 .. 1])",31);
}
@@ -103,7 +97,7 @@ int main(void)
int __gen_e_acsl_initialized_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(t2) +
8 * 2),
- (size_t)(8 * (3 - 2)));
+ (size_t)8);
__e_acsl_assert(! __gen_e_acsl_initialized_2,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(&t2[2 .. 3])",32);
}
@@ -111,7 +105,7 @@ int main(void)
{
int __gen_e_acsl_initialized_3;
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(b + 1 * 0),
- (size_t)(1 * (10 - 0)));
+ (size_t)10);
__e_acsl_assert(! __gen_e_acsl_initialized_3,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(b + (0 .. 10))",
34);
@@ -121,21 +115,21 @@ int main(void)
/*@ assert ¬\initialized(&t3[n - 1 .. n + 2][1][0 .. 1]); */
{
int __gen_e_acsl_forall;
- int __gen_e_acsl_range_5429;
+ int __gen_e_acsl_range_2;
__gen_e_acsl_forall = 1;
- __gen_e_acsl_range_5429 = 0;
+ __gen_e_acsl_range_2 = 0;
while (1) {
- if (__gen_e_acsl_range_5429 <= 1) ; else break;
+ if (__gen_e_acsl_range_2 <= 1) ; else break;
{
int __gen_e_acsl_forall_2;
- long __gen_e_acsl_range_5428;
+ long __gen_e_acsl_range;
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_range_5428 = n - 1L;
+ __gen_e_acsl_range = n - 1L;
while (1) {
- if (__gen_e_acsl_range_5428 <= n + 2L) ; else break;
+ if (__gen_e_acsl_range <= n + 2L) ; else break;
{
int __gen_e_acsl_initialized_4;
- __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& t3[__gen_e_acsl_range_5428][1][__gen_e_acsl_range_5429]),
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& t3[__gen_e_acsl_range][1][__gen_e_acsl_range_2]),
sizeof(float));
if (__gen_e_acsl_initialized_4) ;
else {
@@ -143,7 +137,7 @@ int main(void)
goto e_acsl_end_loop1;
}
}
- __gen_e_acsl_range_5428 ++;
+ __gen_e_acsl_range ++;
}
e_acsl_end_loop1: ;
if (__gen_e_acsl_forall_2) ;
@@ -152,13 +146,50 @@ int main(void)
goto e_acsl_end_loop2;
}
}
- __gen_e_acsl_range_5429 ++;
+ __gen_e_acsl_range_2 ++;
}
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);
}
+ /*@ assert ¬\valid_read(&t3[6][1][0] + (2 .. 10)); */
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)(& t3[6][1][0]) +
+ 4 * 2),(size_t)32,
+ (void *)(& t3[6][1][0]),
+ (void *)0);
+ __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
+ (char *)"main",
+ (char *)"!\\valid_read(&t3[6][1][0] + (2 .. 10))",41);
+ }
+ /*@ assert \valid_read(&t3[n - 1 .. n + 2][1]); */
+ {
+ int __gen_e_acsl_forall_3;
+ long __gen_e_acsl_range_3;
+ __gen_e_acsl_forall_3 = 1;
+ __gen_e_acsl_range_3 = n - 1L;
+ while (1) {
+ if (__gen_e_acsl_range_3 <= n + 2L) ; else break;
+ {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t3[__gen_e_acsl_range_3][1]),
+ sizeof(float [4]),
+ (void *)(& t3[__gen_e_acsl_range_3][1]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_2) ;
+ else {
+ __gen_e_acsl_forall_3 = 0;
+ goto e_acsl_end_loop3;
+ }
+ }
+ __gen_e_acsl_range_3 ++;
+ }
+ 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);
+ }
__retres = 0;
__e_acsl_delete_block((void *)(t3));
__e_acsl_delete_block((void *)(t2));
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 ee1064b721b011ff12c6fb71954dd04b3e09730d..8332495491577b9b6880b9083cbc396ef0e402ba 100644
--- a/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
@@ -37,4 +37,7 @@ int main(void) {
int n = 2;
float t3[7][2][4];
/*@ assert !\initialized(&t3[(n-1)..(n+2)][1][0..1]); */ ;
+
+ /*@ assert !\valid_read(&t3[6][1][0] + (2..10)); */
+ /*@ assert \valid_read(&t3[(n-1)..(n+2)][1]); */
}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 029ff74f8bc74a16094fa0498539884959c9ccc1..a3d2bbae2a53f0cd1ad35c85174a4639f7478a32 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -650,8 +650,8 @@ and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
from set<lty> to lty *)
| Ltype(lti, [lty]) when lti.lt_name = "set" ->
lty
- | Ltype _ | Ctype _ | Linteger | Lreal | Larrow _ | Lvar _ ->
- assert false
+ | Ltype _ | Ctype _ | Linteger | Lreal | Larrow _ | Lvar _ as lty ->
+ lty
in
let t' = Logic_const.term
~loc
@@ -663,8 +663,10 @@ and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
Logic_const.pvalid ~loc (Logic_const.here_label, t')
| "initialized" ->
Logic_const.pinitialized ~loc (Logic_const.here_label, t')
- | _ ->
- assert false
+ | "valid_read" ->
+ Logic_const.pvalid_read ~loc (Logic_const.here_label, t')
+ | _ as s ->
+ Options.fatal "unexpected builtin %s during range elimination" s;
in
let p_quantified = List.fold_left
(fun p (tmin, lv, tmax) ->
@@ -688,7 +690,7 @@ and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
and mmodel_call_memory_block ~loc kf name ctx env p r =
(* Call to [__e_acsl_<name>] for term of the form [p + r]
- when [<name> = valid or initialized] (TODO: valid_read) and
+ when [<name> = valid or initialized or valid_read] and
where [p] is an address, [r] a range offset *)
let n1, n2 = match r.term_node with
| Trange(Some n1, Some n2) ->
@@ -728,6 +730,7 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
let ctx_ity = Typing.integer_ty_of_typ ctx in
Typing.type_term ~use_gmp_opt:true ~ctx:ctx_ity size;
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
@@ -748,7 +751,7 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
let args = match name with
| "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
| "initialized" -> [ ptr; size ]
- | _ -> not_yet env ("builtin" ^ name)
+ | _ -> not_yet env ("builtin " ^ name)
in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
@@ -820,8 +823,9 @@ and bounded_lv_of_range t =
match t.term_node with
| Trange(Some n1, Some n2) ->
let id = Cil_const.new_raw_id () in
+ let name = Env.Varname.get ~scope:Env.Local_block "range" in
let lv = {
- lv_name = "range_" ^ (string_of_int id);
+ lv_name = name;
lv_id = id;
lv_type = Linteger;
lv_kind = LVQuant;