diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml
index afca5076f37a87bf7ff513a5d848aa0fb1a751b5..adc84060c757cbc13e40932b813a3cf9276a4f00 100644
--- a/src/plugins/e-acsl/src/analyses/labels.ml
+++ b/src/plugins/e-acsl/src/analyses/labels.ml
@@ -58,7 +58,7 @@ let preprocess_done = ref false
(** Associate a statement with the [at_data] that need to be translated on
this statement. *)
-let at_data_for_stmts: At_data.Set.t ref Stmt.Hashtbl.t =
+let at_data_for_stmts: At_data.t list ref Stmt.Hashtbl.t =
Stmt.Hashtbl.create 17
(** Add [data] to the list of [at_data] that must be translated on the
@@ -69,23 +69,22 @@ let add_at_for_stmt data stmt =
try
Stmt.Hashtbl.find at_data_for_stmts stmt
with Not_found ->
- let ats_ref = ref At_data.Set.empty in
+ let ats_ref = ref [] in
Stmt.Hashtbl.add at_data_for_stmts stmt ats_ref;
ats_ref
in
let old_data =
try
- At_data.Set.find data !ats_ref
+ List.find (At_data.equal data) !ats_ref
with Not_found ->
- ats_ref := At_data.Set.add data !ats_ref;
+ ats_ref := data :: !ats_ref;
data
in
match old_data.error, data.error with
| Some _, None ->
(* Replace the old data that has an error with the new data that do not
have one. *)
- ats_ref := At_data.Set.remove old_data !ats_ref;
- ats_ref := At_data.Set.add data !ats_ref
+ ats_ref := data :: List.filter (fun d -> not @@ At_data.equal d old_data) !ats_ref;
| Some _, Some _
| None, Some _
| None, None ->
@@ -97,7 +96,7 @@ let add_at_for_stmt data stmt =
let at_for_stmt stmt =
if !preprocess_done then
let ats_ref =
- Stmt.Hashtbl.find_def at_data_for_stmts stmt (ref At_data.Set.empty)
+ Stmt.Hashtbl.find_def at_data_for_stmts stmt (ref [])
in
Result.Ok !ats_ref
else
@@ -558,7 +557,7 @@ let _debug () =
Options.feedback ~level:2 "| - stmt %d at %a"
stmt.sid
Printer.pp_location (Stmt.loc stmt);
- At_data.Set.iter
+ List.iter
(fun at ->
Options.feedback ~level:2 "| - at %a"
At_data.pretty at)
diff --git a/src/plugins/e-acsl/src/analyses/labels.mli b/src/plugins/e-acsl/src/analyses/labels.mli
index 1c9a7951d7f6ec09658a45ceaf76108306983fc9..40627c15b5d5991bba11f4e1cee35a1d88ed5da5 100644
--- a/src/plugins/e-acsl/src/analyses/labels.mli
+++ b/src/plugins/e-acsl/src/analyses/labels.mli
@@ -35,7 +35,7 @@ val get_first_inner_stmt: stmt -> stmt
(** If the given statement has a label, return the first statement of the block.
Otherwise return the given statement. *)
-val at_for_stmt: stmt -> At_data.Set.t Error.result
+val at_for_stmt: stmt -> At_data.t list Error.result
(** @return the set of labeled predicates and terms to be translated on the
given statement.
@raise Not_memoized if the labels pre-analysis was not run. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 58c424efd6d6a3b5344bade03cf8978db2faec40..1b26cd2d50308a6055e3f3eb4bfb914872a423fb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -484,8 +484,8 @@ let for_stmt env kf stmt =
(* Translate the [\at()]. *)
let stmt_translations = Pred_or_term.Hashtbl.create 7 in
- At_data.Set.fold
- (fun ({ lscope; pot; error } as at_data) env ->
+ List.fold_left
+ (fun env ({ lscope; pot; error } as at_data) ->
let open Current_loc.Operators in
let<> UpdatedCurrentLoc = match pot with
| PoT_pred p -> p.pred_loc
@@ -519,8 +519,8 @@ let for_stmt env kf stmt =
Pred_or_term.Hashtbl.replace stmt_translations pot vi_or_err;
At_data.Hashtbl.replace translations at_data vi_or_err;
env)
- at_for_stmt
env
+ at_for_stmt
let to_exp ~loc ~adata kf env pot label =
let kinstr = Env.get_kinstr env in
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
index f869913749cff6fb6e59c8ffe43152312b6e9825..b9b1b2d81696756053d10fba479a8bb46283e583 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -28,8 +28,8 @@ void f(void)
__gen_e_acsl_at_2 = A;
__gen_e_acsl_at_3 = A;
A = 1;
- F: __gen_e_acsl_at_4 = A;
- __gen_e_acsl_at_5 = __gen_e_acsl_at_2;
+ F: __gen_e_acsl_at_4 = __gen_e_acsl_at_2;
+ __gen_e_acsl_at_5 = A;
A = 2;
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
@@ -49,14 +49,14 @@ void f(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"\\at(A,F)",0,
- __gen_e_acsl_at_4);
+ __gen_e_acsl_at_5);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "\\at(A,F) == 1";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 17;
- __e_acsl_assert(__gen_e_acsl_at_4 == 1,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_at_5 == 1,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \at(A,F) == 1; */ ;
@@ -78,14 +78,14 @@ void f(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
- "\\at(\\at(A,Pre),F)",0,__gen_e_acsl_at_5);
+ "\\at(\\at(A,Pre),F)",0,__gen_e_acsl_at_4);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Assertion";
__gen_e_acsl_assert_data_4.pred_txt = "\\at(\\at(A,Pre),F) == 0";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "f";
__gen_e_acsl_assert_data_4.line = 19;
- __e_acsl_assert(__gen_e_acsl_at_5 == 0,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_at_4 == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \at(\at(A,Pre),F) == 0; */ ;
@@ -405,8 +405,8 @@ void i(void)
int main(void)
{
- long __gen_e_acsl_at_3;
- int __gen_e_acsl_at_2;
+ int __gen_e_acsl_at_3;
+ long __gen_e_acsl_at_2;
long __gen_e_acsl_at;
int __retres;
int x;
@@ -419,8 +419,8 @@ int main(void)
L:
{
__gen_e_acsl_at = (long)x;
- __gen_e_acsl_at_2 = x;
- __gen_e_acsl_at_3 = x + 1L;
+ __gen_e_acsl_at_2 = x + 1L;
+ __gen_e_acsl_at_3 = x;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"x",0,x);
__gen_e_acsl_assert_data.blocking = 1;
@@ -442,14 +442,14 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"\\at(x,L)",0,
- __gen_e_acsl_at_2);
+ __gen_e_acsl_at_3);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "\\at(x,L) == 0";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 77;
- __e_acsl_assert(__gen_e_acsl_at_2 == 0,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_at_3 == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \at(x,L) == 0; */ ;
@@ -457,14 +457,14 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_register_long(& __gen_e_acsl_assert_data_3,
- "\\at(x + 1,L)",0,__gen_e_acsl_at_3);
+ "\\at(x + 1,L)",0,__gen_e_acsl_at_2);
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
__gen_e_acsl_assert_data_3.pred_txt = "\\at(x + 1,L) == 1";
__gen_e_acsl_assert_data_3.file = "at.i";
__gen_e_acsl_assert_data_3.fct = "main";
__gen_e_acsl_assert_data_3.line = 78;
- __e_acsl_assert(__gen_e_acsl_at_3 == 1L,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert(__gen_e_acsl_at_2 == 1L,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
/*@ assert \at(x + 1,L) == 1; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index 54abb67f00134052a63240bbff4b4cf8de25563b..3850002297e31c2857172366f0c352b776b1589b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -105,19 +105,19 @@ int main(void)
int *__gen_e_acsl_at_7;
long *__gen_e_acsl_at_6;
int *__gen_e_acsl_at_5;
+ int *__gen_e_acsl_at_4;
int *__gen_e_acsl_at_3;
long *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
int __retres;
int n;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__gen_e_acsl_at_8 = (long *)malloc(64UL);
- __gen_e_acsl_at_7 = (int *)malloc(12000UL);
+ __gen_e_acsl_at_7 = (int *)malloc(528UL);
__gen_e_acsl_at_6 = (long *)malloc(2496UL);
- __gen_e_acsl_at_5 = (int *)malloc(528UL);
+ __gen_e_acsl_at_5 = (int *)malloc(12000UL);
+ __gen_e_acsl_at_4 = (int *)malloc(4UL);
__gen_e_acsl_at_3 = (int *)malloc(12UL);
__gen_e_acsl_at_2 = (long *)malloc(8UL);
- __gen_e_acsl_at = (int *)malloc(4UL);
__e_acsl_store_block((void *)(& n),4UL);
__e_acsl_full_init((void *)(& n));
n = 7;
@@ -125,12 +125,7 @@ int main(void)
{
int __gen_e_acsl_i;
__gen_e_acsl_i = 3;
- *(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i == 10L;
- }
- {
- int __gen_e_acsl_i_2;
- __gen_e_acsl_i_2 = 3;
- *(__gen_e_acsl_at_2 + 0) = n + (long)__gen_e_acsl_i_2;
+ *(__gen_e_acsl_at_2 + 0) = n + (long)__gen_e_acsl_i;
}
{
int __gen_e_acsl_j;
@@ -141,27 +136,40 @@ int main(void)
__gen_e_acsl_j ++;
}
}
+ {
+ int __gen_e_acsl_i_2;
+ __gen_e_acsl_i_2 = 3;
+ *(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_2 == 10L;
+ }
;
__e_acsl_full_init((void *)(& n));
n = 9;
K:
{
- int __gen_e_acsl_k;
int __gen_e_acsl_u;
int __gen_e_acsl_v;
- __gen_e_acsl_k = -7;
- __gen_e_acsl_u = 9;
+ int __gen_e_acsl_w;
+ __gen_e_acsl_u = 10;
while (1) {
- if (__gen_e_acsl_u < 21) ; else break;
- __gen_e_acsl_v = -5 + 1;
+ if (__gen_e_acsl_u < 20) ; else break;
+ __gen_e_acsl_v = -10 + 1;
while (1) {
- if (__gen_e_acsl_v <= 6) ; else break;
{
- long __gen_e_acsl_if;
- if (__gen_e_acsl_u > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k;
- else __gen_e_acsl_if = __gen_e_acsl_u + __gen_e_acsl_v;
- *(__gen_e_acsl_at_5 + ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4))) =
- __gen_e_acsl_if > 0L;
+ int __gen_e_acsl_u_3;
+ __gen_e_acsl_u_3 = -2;
+ if (__gen_e_acsl_v <= -5 + __gen_e_acsl_u_3) ; else break;
+ }
+ __gen_e_acsl_w = 100 + 1;
+ while (1) {
+ if (__gen_e_acsl_w <= 200) ; else break;
+ {
+ int __gen_e_acsl_u_2;
+ __gen_e_acsl_u_2 = 42;
+ *(__gen_e_acsl_at_5 + ((__gen_e_acsl_u - 10) * 300 + ((__gen_e_acsl_v - -9) * 100 + (
+ __gen_e_acsl_w - 101)))) =
+ (((n - (long)__gen_e_acsl_u) + __gen_e_acsl_u_2) + __gen_e_acsl_v) + __gen_e_acsl_w > 0L;
+ }
+ __gen_e_acsl_w ++;
}
__gen_e_acsl_v ++;
}
@@ -169,56 +177,47 @@ int main(void)
}
}
{
- int __gen_e_acsl_u_2;
+ int __gen_e_acsl_u_4;
int __gen_e_acsl_v_2;
- __gen_e_acsl_u_2 = 9;
+ __gen_e_acsl_u_4 = 9;
while (1) {
- if (__gen_e_acsl_u_2 < 21) ; else break;
+ if (__gen_e_acsl_u_4 < 21) ; else break;
__gen_e_acsl_v_2 = -5 + 1;
while (1) {
{
- int __gen_e_acsl_if_2;
- if (__gen_e_acsl_u_2 < 15) __gen_e_acsl_if_2 = __gen_e_acsl_u_2 + 6;
- else __gen_e_acsl_if_2 = 3;
- if (__gen_e_acsl_v_2 <= __gen_e_acsl_if_2) ; else break;
+ int __gen_e_acsl_if;
+ if (__gen_e_acsl_u_4 < 15) __gen_e_acsl_if = __gen_e_acsl_u_4 + 6;
+ else __gen_e_acsl_if = 3;
+ if (__gen_e_acsl_v_2 <= __gen_e_acsl_if) ; else break;
}
- *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 26 + (__gen_e_acsl_v_2 - -4))) =
- (n + (long)__gen_e_acsl_u_2) + __gen_e_acsl_v_2;
+ *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 26 + (__gen_e_acsl_v_2 - -4))) =
+ (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_2;
__gen_e_acsl_v_2 ++;
}
- __gen_e_acsl_u_2 ++;
+ __gen_e_acsl_u_4 ++;
}
}
{
- int __gen_e_acsl_u_3;
+ int __gen_e_acsl_k;
+ int __gen_e_acsl_u_5;
int __gen_e_acsl_v_3;
- int __gen_e_acsl_w;
- __gen_e_acsl_u_3 = 10;
+ __gen_e_acsl_k = -7;
+ __gen_e_acsl_u_5 = 9;
while (1) {
- if (__gen_e_acsl_u_3 < 20) ; else break;
- __gen_e_acsl_v_3 = -10 + 1;
+ if (__gen_e_acsl_u_5 < 21) ; else break;
+ __gen_e_acsl_v_3 = -5 + 1;
while (1) {
+ if (__gen_e_acsl_v_3 <= 6) ; else break;
{
- int __gen_e_acsl_u_5;
- __gen_e_acsl_u_5 = -2;
- if (__gen_e_acsl_v_3 <= -5 + __gen_e_acsl_u_5) ; else break;
- }
- __gen_e_acsl_w = 100 + 1;
- while (1) {
- if (__gen_e_acsl_w <= 200) ; else break;
- {
- int __gen_e_acsl_u_4;
- __gen_e_acsl_u_4 = 42;
- *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_3 - 10) * 300 + ((
- __gen_e_acsl_v_3 - -9) * 100 + (
- __gen_e_acsl_w - 101)))) =
- (((n - (long)__gen_e_acsl_u_3) + __gen_e_acsl_u_4) + __gen_e_acsl_v_3) + __gen_e_acsl_w > 0L;
- }
- __gen_e_acsl_w ++;
+ long __gen_e_acsl_if_2;
+ if (__gen_e_acsl_u_5 > 0) __gen_e_acsl_if_2 = n + (long)__gen_e_acsl_k;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_u_5 + __gen_e_acsl_v_3;
+ *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 9) * 11 + (__gen_e_acsl_v_3 - -4))) =
+ __gen_e_acsl_if_2 > 0L;
}
__gen_e_acsl_v_3 ++;
}
- __gen_e_acsl_u_3 ++;
+ __gen_e_acsl_u_5 ++;
}
}
;
@@ -231,20 +230,21 @@ int main(void)
__gen_e_acsl_i_3 = 3;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"\\at(n + i == 10,L)",0,
- *(__gen_e_acsl_at + 0));
+ *(__gen_e_acsl_at_4 + 0));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_4",
+ (void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__gen_e_acsl_at_4 + 0)";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 28;
@@ -257,7 +257,7 @@ int main(void)
__gen_e_acsl_assert_data.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 28;
- __e_acsl_assert(*(__gen_e_acsl_at + 0),& __gen_e_acsl_assert_data);
+ __e_acsl_assert(*(__gen_e_acsl_at_4 + 0),& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
/*@ assert \let i = 3; \at(n + i == 10,L); */ ;
@@ -341,17 +341,17 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(
- __gen_e_acsl_at_5 + (int)(
+ __gen_e_acsl_at_7 + (int)(
(long)((int)(
(long)((int)(
__gen_e_acsl_u_6 - 9L)) * 11L)) + (int)(
__gen_e_acsl_v_4 - -4L))),
sizeof(int),
- (void *)__gen_e_acsl_at_5,
- (void *)(& __gen_e_acsl_at_5));
+ (void *)__gen_e_acsl_at_7,
+ (void *)(& __gen_e_acsl_at_7));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_at_5",
- (void *)__gen_e_acsl_at_5);
+ "__gen_e_acsl_at_7",
+ (void *)__gen_e_acsl_at_7);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
"__gen_e_acsl_u_6",0,
__gen_e_acsl_u_6);
@@ -362,7 +362,7 @@ int main(void)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_5 +\n (int)((int)((int)(__gen_e_acsl_u_6 - 9) * 11) +\n (int)(__gen_e_acsl_v_4 - -4)))";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_6 - 9) * 11) +\n (int)(__gen_e_acsl_v_4 - -4)))";
__gen_e_acsl_assert_data_6.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 34;
@@ -370,7 +370,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_3,
& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- if (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_u_6 - 9) * 11 + (
+ if (*(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_6 - 9) * 11 + (
__gen_e_acsl_v_4 - -4)))) ;
else {
__gen_e_acsl_forall = 0;
@@ -656,7 +656,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_14 =
{.values = (void *)0};
__gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(
- __gen_e_acsl_at_7 + (int)(
+ __gen_e_acsl_at_5 + (int)(
(long)((int)(
(long)((int)(
__gen_e_acsl_u_8 - 10L)) * 300L)) + (int)(
@@ -665,11 +665,11 @@ int main(void)
__gen_e_acsl_v_6 - -9L)) * 100L)) + (int)(
__gen_e_acsl_w_2 - 101L)))),
sizeof(int),
- (void *)__gen_e_acsl_at_7,
- (void *)(& __gen_e_acsl_at_7));
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_14,
- "__gen_e_acsl_at_7",
- (void *)__gen_e_acsl_at_7);
+ "__gen_e_acsl_at_5",
+ (void *)__gen_e_acsl_at_5);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,
"__gen_e_acsl_u_8",0,
__gen_e_acsl_u_8);
@@ -683,7 +683,7 @@ int main(void)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_14.blocking = 1;
__gen_e_acsl_assert_data_14.kind = "RTE";
- __gen_e_acsl_assert_data_14.pred_txt = "\\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_8 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_6 - -9) * 100) +\n (int)(__gen_e_acsl_w_2 - 101))))";
+ __gen_e_acsl_assert_data_14.pred_txt = "\\valid_read(__gen_e_acsl_at_5 +\n (int)((int)((int)(__gen_e_acsl_u_8 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_6 - -9) * 100) +\n (int)(__gen_e_acsl_w_2 - 101))))";
__gen_e_acsl_assert_data_14.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_14.fct = "main";
__gen_e_acsl_assert_data_14.line = 59;
@@ -691,7 +691,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_7,
& __gen_e_acsl_assert_data_14);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
- if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_8 - 10) * 300 + (
+ if (! *(__gen_e_acsl_at_5 + ((__gen_e_acsl_u_8 - 10) * 300 + (
(__gen_e_acsl_v_6 - -9) * 100 + (
__gen_e_acsl_w_2 - 101)))))
;
@@ -751,9 +751,9 @@ int main(void)
__retres = 0;
__e_acsl_delete_block((void *)(t));
__e_acsl_delete_block((void *)(& n));
- free((void *)__gen_e_acsl_at);
free((void *)__gen_e_acsl_at_2);
free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_4);
free((void *)__gen_e_acsl_at_5);
free((void *)__gen_e_acsl_at_6);
free((void *)__gen_e_acsl_at_7);
@@ -785,7 +785,8 @@ void __gen_e_acsl_f(int *t)
int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (int)(
+ __gen_e_acsl_m - 4L)),
sizeof(int),(void *)t,
(void *)(& t));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"t",(void *)t);
@@ -795,14 +796,14 @@ void __gen_e_acsl_f(int *t)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "\\valid_read(t + __gen_e_acsl_m)";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid_read(t + (int)(__gen_e_acsl_m - 4))";
__gen_e_acsl_assert_data.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 8;
__gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- *(__gen_e_acsl_at + 0) = *(t + __gen_e_acsl_m) == -4;
+ *(__gen_e_acsl_at + 0) = *(t + (__gen_e_acsl_m - 4));
}
}
{
@@ -812,8 +813,7 @@ void __gen_e_acsl_f(int *t)
int __gen_e_acsl_valid_read_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (int)(
- __gen_e_acsl_m_2 - 4L)),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m_2),
sizeof(int),(void *)t,
(void *)(& t));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"t",
@@ -824,14 +824,14 @@ void __gen_e_acsl_f(int *t)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(t + (int)(__gen_e_acsl_m_2 - 4))";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(t + __gen_e_acsl_m_2)";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 8;
__gen_e_acsl_assert_data_2.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- *(__gen_e_acsl_at_2 + 0) = *(t + (__gen_e_acsl_m_2 - 4));
+ *(__gen_e_acsl_at_2 + 0) = *(t + __gen_e_acsl_m_2) == -4;
}
}
{
@@ -997,17 +997,18 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_m_3 = 4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + 0),
sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_9,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "RTE";
- __gen_e_acsl_assert_data_9.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
+ __gen_e_acsl_assert_data_9.pred_txt = "\\valid_read(__gen_e_acsl_at_2 + 0)";
__gen_e_acsl_assert_data_9.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_9.fct = "f";
__gen_e_acsl_assert_data_9.line = 8;
@@ -1016,23 +1017,22 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
"\\old(*(t + m) == -4)",0,
- *(__gen_e_acsl_at + 0));
- if (*(__gen_e_acsl_at + 0)) {
+ *(__gen_e_acsl_at_2 + 0));
+ if (*(__gen_e_acsl_at_2 + 0)) {
int __gen_e_acsl_valid_read_8;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + 0),
+ __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
sizeof(int),
- (void *)__gen_e_acsl_at_2,
- (void *)(& __gen_e_acsl_at_2));
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_10,
- "__gen_e_acsl_at_2",
- (void *)__gen_e_acsl_at_2);
+ "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_10,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_10.blocking = 1;
__gen_e_acsl_assert_data_10.kind = "RTE";
- __gen_e_acsl_assert_data_10.pred_txt = "\\valid_read(__gen_e_acsl_at_2 + 0)";
+ __gen_e_acsl_assert_data_10.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
__gen_e_acsl_assert_data_10.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_10.fct = "f";
__gen_e_acsl_assert_data_10.line = 8;
@@ -1042,8 +1042,8 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
"\\old(*(t + (m - 4)))",0,
- *(__gen_e_acsl_at_2 + 0));
- __gen_e_acsl_and_2 = *(__gen_e_acsl_at_2 + 0) == 9;
+ *(__gen_e_acsl_at + 0));
+ __gen_e_acsl_and_2 = *(__gen_e_acsl_at + 0) == 9;
}
else __gen_e_acsl_and_2 = 0;
__gen_e_acsl_assert_data_8.blocking = 1;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
index 40e395ec27c766a1c5613115a1828868132a118b..b301bf239fc22186aeaf8dc676523e050afb0f7e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
@@ -356,19 +356,19 @@ double __gen_e_acsl_avg(double a, double b)
__e_acsl_mpq_t __gen_e_acsl_at;
double __retres;
{
- __e_acsl_mpq_t __gen_e_acsl_a;
__e_acsl_mpq_t __gen_e_acsl_b;
- __gmpq_init(__gen_e_acsl_a);
- __gmpq_set_d(__gen_e_acsl_a,a);
- __gmpq_init(__gen_e_acsl_at);
- __gmpq_set(__gen_e_acsl_at,(__e_acsl_mpq_struct const *)(__gen_e_acsl_a));
+ __e_acsl_mpq_t __gen_e_acsl_a;
__gmpq_init(__gen_e_acsl_b);
__gmpq_set_d(__gen_e_acsl_b,b);
+ __gmpq_init(__gen_e_acsl_at);
+ __gmpq_set(__gen_e_acsl_at,(__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
+ __gmpq_init(__gen_e_acsl_a);
+ __gmpq_set_d(__gen_e_acsl_a,a);
__gmpq_init(__gen_e_acsl_at_2);
__gmpq_set(__gen_e_acsl_at_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
- __gmpq_clear(__gen_e_acsl_a);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_a));
__gmpq_clear(__gen_e_acsl_b);
+ __gmpq_clear(__gen_e_acsl_a);
}
__retres = avg(a,b);
{
@@ -386,8 +386,8 @@ double __gen_e_acsl_avg(double a, double b)
__gen_e_acsl_delta = 1;
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_at));
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"2",10);
__gmpq_init(__gen_e_acsl_div);
@@ -441,9 +441,9 @@ double __gen_e_acsl_avg(double a, double b)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"\\old(a)",
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at));
- __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"\\old(b)",
(__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2));
+ __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"\\old(b)",
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_at));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Postcondition";
__gen_e_acsl_assert_data.pred_txt = "\\let delta = 1;\n\\let avg_real = (\\old(a) + \\old(b)) / 2;\n avg_real - delta < \\result < avg_real + delta";
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index f67fbe8bd183ba14e1360edd8f20bd6fc8a42478..ba7fd848e53192e39a03df7416f9a3aad97b81f2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -109,11 +109,11 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_store_block((void *)(& Mtmin_out),8UL);
__e_acsl_store_block((void *)(& Mwmin),8UL);
__e_acsl_store_block((void *)(& Mtmin_in),8UL);
- __gen_e_acsl_at = Mtmin_in;
+ __gen_e_acsl_at = Mwmin;
__gen_e_acsl_at_2 = Mtmin_in;
- __gen_e_acsl_at_3 = Mtmin_in;
- __gen_e_acsl_at_4 = Mwmin;
- __gen_e_acsl_at_5 = Mwmin;
+ __gen_e_acsl_at_3 = Mwmin;
+ __gen_e_acsl_at_4 = Mtmin_in;
+ __gen_e_acsl_at_5 = Mtmin_in;
__gen_e_acsl_at_6 = Mtmin_out;
__gen_e_acsl_contract = __e_acsl_contract_init(1UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
@@ -187,18 +187,18 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_5,
sizeof(float),
- (void *)__gen_e_acsl_at_3,
- (void *)(& __gen_e_acsl_at_3));
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
- "__gen_e_acsl_at_3",
- (void *)__gen_e_acsl_at_3);
+ "__gen_e_acsl_at_5",
+ (void *)__gen_e_acsl_at_5);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
"sizeof(float)",0,sizeof(float));
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "RTE";
- __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(__gen_e_acsl_at_3)";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(__gen_e_acsl_at_5)";
__gen_e_acsl_assert_data_5.file = "bts1307.i";
__gen_e_acsl_assert_data_5.fct = "bar";
__gen_e_acsl_assert_data_5.line = 26;
@@ -225,18 +225,18 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gen_e_acsl_assert_data_6.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- if (*__gen_e_acsl_at_6 == *__gen_e_acsl_at_3) {
+ if (*__gen_e_acsl_at_6 == *__gen_e_acsl_at_5) {
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl__3;
__e_acsl_mpq_t __gen_e_acsl_mul;
int __gen_e_acsl_lt;
__gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at_2);
+ __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at_4);
__gmpq_init(__gen_e_acsl__2);
__gmpq_set_str(__gen_e_acsl__2,"085/100",10);
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_5);
+ __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
@@ -254,18 +254,18 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid_read_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
sizeof(float),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,
- "__gen_e_acsl_at",
- (void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,
"sizeof(float)",0,sizeof(float));
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at_2)";
__gen_e_acsl_assert_data_7.file = "bts1307.i";
__gen_e_acsl_assert_data_7.fct = "bar";
__gen_e_acsl_assert_data_7.line = 26;
@@ -274,8 +274,8 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at);
- __gen_e_acsl_if = (double)*__gen_e_acsl_at != 0.;
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at_2);
+ __gen_e_acsl_if = (double)*__gen_e_acsl_at_2 != 0.;
}
else {
__e_acsl_mpq_t __gen_e_acsl__4;
@@ -286,7 +286,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gmpq_init(__gen_e_acsl__4);
__gmpq_set_str(__gen_e_acsl__4,"085/100",10);
__gmpq_init(__gen_e_acsl__5);
- __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_4);
+ __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at);
__gmpq_init(__gen_e_acsl_mul_2);
__gmpq_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
@@ -296,7 +296,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmin)",*__gen_e_acsl_at_4);
+ "*\\old(Mwmin)",*__gen_e_acsl_at);
__gen_e_acsl_if = __gen_e_acsl_ne != 0;
__gmpq_clear(__gen_e_acsl__4);
__gmpq_clear(__gen_e_acsl__5);
@@ -306,11 +306,11 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
"*\\old(Mtmin_out)",*__gen_e_acsl_at_6);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at_3);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at_5);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at_2);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at_4);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmin)",*__gen_e_acsl_at_5);
+ "*\\old(Mwmin)",*__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Postcondition";
__gen_e_acsl_assert_data_4.pred_txt = "*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85 * *\\old(Mwmin) != 0.";
@@ -352,8 +352,8 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_store_block((void *)(& Mtmax_out),8UL);
__e_acsl_store_block((void *)(& Mwmax),8UL);
__e_acsl_store_block((void *)(& Mtmax_in),8UL);
- __gen_e_acsl_at = Mtmax_in;
- __gen_e_acsl_at_2 = Mwmax;
+ __gen_e_acsl_at = Mwmax;
+ __gen_e_acsl_at_2 = Mtmax_in;
__gen_e_acsl_at_3 = Mtmax_out;
__gen_e_acsl_contract = __e_acsl_contract_init(1UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
@@ -437,7 +437,7 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gmpq_init(__gen_e_acsl_);
__gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at_3);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at);
+ __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl__3);
__gmpq_set_str(__gen_e_acsl__3,"5",10);
__gmpq_init(__gen_e_acsl__4);
@@ -449,7 +449,7 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gmpq_init(__gen_e_acsl__6);
- __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_2);
+ __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div),
@@ -473,9 +473,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
"*\\old(Mtmax_out)",*__gen_e_acsl_at_3);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmax_in)",*__gen_e_acsl_at);
+ "*\\old(Mtmax_in)",*__gen_e_acsl_at_2);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmax)",*__gen_e_acsl_at_2);
+ "*\\old(Mwmax)",*__gen_e_acsl_at);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Postcondition";
__gen_e_acsl_assert_data_4.pred_txt = "*\\old(Mtmax_out) != *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)";
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 73c880a96c69d88ef21b70357a687cf4a8799d7a..27cb9dd93446728ef196bf56a59425b8462883f0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -71,8 +71,8 @@ void *memchr(void const *buf, int c, size_t n)
void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- int __gen_e_acsl_at_2;
- void const *__gen_e_acsl_at;
+ void const *__gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
void *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
{
@@ -81,8 +81,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall;
int __gen_e_acsl_k;
__e_acsl_store_block((void *)(& buf),8UL);
- __gen_e_acsl_at = buf;
- __gen_e_acsl_at_2 = c;
+ __gen_e_acsl_at = c;
+ __gen_e_acsl_at_2 = buf;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__gen_e_acsl_exists = 0;
__gen_e_acsl_i = 0;
@@ -186,20 +186,20 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_valid_read_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at + __gen_e_acsl_j),
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j),
sizeof(char),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
- "__gen_e_acsl_at",
- (void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_uint(& __gen_e_acsl_assert_data_4,
"__gen_e_acsl_j",0,__gen_e_acsl_j);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(char)",0,sizeof(char));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read((char *)__gen_e_acsl_at + __gen_e_acsl_j)";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j)";
__gen_e_acsl_assert_data_4.file = "bts1390.c";
__gen_e_acsl_assert_data_4.fct = "memchr";
__gen_e_acsl_assert_data_4.line = 9;
@@ -207,7 +207,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_3,
& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
- if ((int)*((char *)__gen_e_acsl_at + __gen_e_acsl_j) != __gen_e_acsl_at_2)
+ if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at)
;
else {
__gen_e_acsl_forall_2 = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 6e05c2f6131c2059f99403a0199e8e14f392efbe..ed9c13bf241340f6e7447a8d8d28dede54037e03 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -54,11 +54,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- __e_acsl_mpz_t __gen_e_acsl_at_5;
- char const *__gen_e_acsl_at_4;
- char *__gen_e_acsl_at_3;
+ char *__gen_e_acsl_at_5;
+ char *__gen_e_acsl_at_4;
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
char *__gen_e_acsl_at_2;
- char *__gen_e_acsl_at;
+ char const *__gen_e_acsl_at;
char *__retres;
{
__e_acsl_mpz_t __gen_e_acsl_n;
@@ -89,13 +89,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
- __gen_e_acsl_at = dest;
+ __gen_e_acsl_at = src;
__gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at_3 = dest;
- __gen_e_acsl_at_4 = src;
__gmpz_init_set_ui(__gen_e_acsl_n,n);
- __gmpz_init_set(__gen_e_acsl_at_5,
+ __gmpz_init_set(__gen_e_acsl_at_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gen_e_acsl_at_4 = dest;
+ __gen_e_acsl_at_5 = dest;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -277,7 +277,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result",
(void *)__retres);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(dest)",
- (void *)__gen_e_acsl_at_3);
+ (void *)__gen_e_acsl_at_5);
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "Postcondition";
__gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(dest)";
@@ -285,7 +285,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_6.fct = "strncpy";
__gen_e_acsl_assert_data_6.line = 437;
__gen_e_acsl_assert_data_6.name = "result_ptr";
- __e_acsl_assert(__retres == __gen_e_acsl_at_3,
+ __e_acsl_assert(__retres == __gen_e_acsl_at_5,
& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
@@ -293,7 +293,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_init_set_si(__gen_e_acsl__14,1L);
__gmpz_init(__gen_e_acsl_sub_7);
__gmpz_sub(__gen_e_acsl_sub_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__gmpz_init_set_si(__gen_e_acsl__15,0L);
__gmpz_init(__gen_e_acsl_sub_8);
@@ -308,17 +308,17 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_size_8 = 1UL * __gen_e_acsl__16;
if (__gen_e_acsl_size_8 <= 0UL) __gen_e_acsl_if_8 = 0UL;
else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(__gen_e_acsl_at_4 +
1 * 0),
__gen_e_acsl_if_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"\\old(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
__gen_e_acsl_size_8);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
@@ -343,7 +343,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_clear(__gen_e_acsl__15);
__gmpz_clear(__gen_e_acsl_sub_8);
__gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl_at_5);
+ __gmpz_clear(__gen_e_acsl_at_3);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
index 7c44d029d13b4a608006582414c005f68a03fe45..128027b11265ff5b5202c3073a1d642db6844789 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
@@ -38,12 +38,11 @@ int main(void)
/*@ ensures *\old(item) == \old(*item); */
void __gen_e_acsl_f(struct X *item)
{
- struct X __gen_e_acsl_at_2;
- struct X *__gen_e_acsl_at;
+ struct X *__gen_e_acsl_at_2;
+ struct X __gen_e_acsl_at;
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& item),8UL);
- __gen_e_acsl_at = item;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)item,
sizeof(struct X),
@@ -62,7 +61,8 @@ void __gen_e_acsl_f(struct X *item)
__gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- __gen_e_acsl_at_2 = *item;
+ __gen_e_acsl_at = *item;
+ __gen_e_acsl_at_2 = item;
}
f(item);
__e_acsl_delete_block((void *)(& item));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
index 3929c369e311404b5864331f7b2cd16d1fa41f72..da2c84457fbf645025b2ff3696bcd5fb4c6edda8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
@@ -63,8 +63,8 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
FILE * restrict stream)
{
size_t __gen_e_acsl_at_3;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- void *__gen_e_acsl_at;
+ void *__gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at;
size_t __retres;
{
__e_acsl_mpz_t __gen_e_acsl_size;
@@ -88,10 +88,10 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& stream),8UL);
__e_acsl_store_block((void *)(& ptr),8UL);
- __gen_e_acsl_at = ptr;
__gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_2 = ptr;
__gen_e_acsl_at_3 = nmemb;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
@@ -293,7 +293,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init(__gen_e_acsl_mul_4);
__gmpz_mul(__gen_e_acsl_mul_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
@@ -343,11 +343,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert(__gen_e_acsl_le_5 <= 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gen_e_acsl_size_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at_2 +
1 * 0),
__gen_e_acsl_size_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(ptr)",
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
@@ -356,7 +356,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__retres);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
@@ -390,7 +390,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_clear(__gen_e_acsl_mul_5);
__gmpz_clear(__gen_e_acsl_if_2);
__gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
index a89b03788ba4bdb0ffcb6a3e64e5b4e6825ffd5a..9f2896b4fee3591fe4dc47a6d3e5e44b764be591 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
@@ -61,8 +61,8 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
int __gen_e_acsl_at;
{
int __gen_e_acsl_assumes_value;
- __gen_e_acsl_at = b;
- __gen_e_acsl_at_2 = e;
+ __gen_e_acsl_at = e;
+ __gen_e_acsl_at_2 = b;
__gen_e_acsl_contract = __e_acsl_contract_init(1UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -334,25 +334,25 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_19 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_19,
- "__gen_e_acsl_at",0,__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",0,__gen_e_acsl_at_2);
__gen_e_acsl_assert_data_19.blocking = 1;
__gen_e_acsl_assert_data_19.kind = "RTE";
- __gen_e_acsl_assert_data_19.pred_txt = "__gen_e_acsl_at != 0";
+ __gen_e_acsl_assert_data_19.pred_txt = "__gen_e_acsl_at_2 != 0";
__gen_e_acsl_assert_data_19.file = "rte.i";
__gen_e_acsl_assert_data_19.fct = "test";
__gen_e_acsl_assert_data_19.line = 8;
__gen_e_acsl_assert_data_19.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_at != 0,& __gen_e_acsl_assert_data_19);
+ __e_acsl_assert(__gen_e_acsl_at_2 != 0,& __gen_e_acsl_assert_data_19);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_19);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_18,"\\old(b)",0,
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__gen_e_acsl_assert_data_18.blocking = 1;
__gen_e_acsl_assert_data_18.kind = "Postcondition";
__gen_e_acsl_assert_data_18.pred_txt = "1 % \\old(b) == 1";
__gen_e_acsl_assert_data_18.file = "rte.i";
__gen_e_acsl_assert_data_18.fct = "test";
__gen_e_acsl_assert_data_18.line = 8;
- __e_acsl_assert(1 % __gen_e_acsl_at == 1,& __gen_e_acsl_assert_data_18);
+ __e_acsl_assert(1 % __gen_e_acsl_at_2 == 1,& __gen_e_acsl_assert_data_18);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_18);
__gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,0UL);
@@ -362,18 +362,18 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_21 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_21,
- "__gen_e_acsl_at_2",0,__gen_e_acsl_at_2);
+ "__gen_e_acsl_at",0,__gen_e_acsl_at);
__gen_e_acsl_assert_data_21.blocking = 1;
__gen_e_acsl_assert_data_21.kind = "RTE";
- __gen_e_acsl_assert_data_21.pred_txt = "__gen_e_acsl_at_2 != 0";
+ __gen_e_acsl_assert_data_21.pred_txt = "__gen_e_acsl_at != 0";
__gen_e_acsl_assert_data_21.file = "rte.i";
__gen_e_acsl_assert_data_21.fct = "test";
__gen_e_acsl_assert_data_21.line = 18;
__gen_e_acsl_assert_data_21.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_at_2 != 0,& __gen_e_acsl_assert_data_21);
+ __e_acsl_assert(__gen_e_acsl_at != 0,& __gen_e_acsl_assert_data_21);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_21);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_20,"\\old(e)",
- 0,__gen_e_acsl_at_2);
+ 0,__gen_e_acsl_at);
__gen_e_acsl_assert_data_20.blocking = 1;
__gen_e_acsl_assert_data_20.kind = "Postcondition";
__gen_e_acsl_assert_data_20.pred_txt = "1 % \\old(e) == 1";
@@ -381,8 +381,7 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__gen_e_acsl_assert_data_20.fct = "test";
__gen_e_acsl_assert_data_20.line = 18;
__gen_e_acsl_assert_data_20.name = "bhvr";
- __e_acsl_assert(1 % __gen_e_acsl_at_2 == 1,
- & __gen_e_acsl_assert_data_20);
+ __e_acsl_assert(1 % __gen_e_acsl_at == 1,& __gen_e_acsl_assert_data_20);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_20);
}
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 498e8881d33844d2151eea6f3457761ecf70eb49..8558e51e17a8de854f50382b249b38653d819419 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -736,6 +736,7 @@ void test_specifier_application(char const *allowed, char const *fmt,
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
unsigned long __gen_e_acsl_strcpy_src_size;
+ char *__gen_e_acsl_at_3;
char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
@@ -743,6 +744,7 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
__gen_e_acsl_at_2 = src;
+ __gen_e_acsl_at_3 = dest;
__gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
@@ -831,13 +833,19 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
char *__gen_e_acsl_strchr(char const *s, int c)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- int __gen_e_acsl_at_2;
+ int __gen_e_acsl_at_5;
+ char const *__gen_e_acsl_at_4;
+ char const *__gen_e_acsl_at_3;
+ char const *__gen_e_acsl_at_2;
char const *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
__e_acsl_store_block((void *)(& s),8UL);
__gen_e_acsl_at = s;
- __gen_e_acsl_at_2 = c;
+ __gen_e_acsl_at_2 = s;
+ __gen_e_acsl_at_3 = s;
+ __gen_e_acsl_at_4 = s;
+ __gen_e_acsl_at_5 = c;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__retres = strchr(s,c);
{
@@ -884,11 +892,11 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_3,"*\\result",
0,*__retres);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"\\old(c)",0,
- __gen_e_acsl_at_2);
+ __gen_e_acsl_at_5);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
__gen_e_acsl_base_addr = __e_acsl_base_addr((void *)__retres);
- __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at);
+ __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
"\\base_addr(\\result)",
__gen_e_acsl_base_addr);
@@ -912,7 +920,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__gen_e_acsl_assert_data_3.fct = "strchr";
__gen_e_acsl_assert_data_3.line = 198;
__gen_e_acsl_assert_data_3.name = "found/result_char";
- __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at_2),
+ __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at_5),
& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
@@ -1017,12 +1025,14 @@ pid_t __gen_e_acsl_fork(void)
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),8UL);
__gen_e_acsl_at = stat_loc;
+ __gen_e_acsl_at_2 = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL,
stat_loc == (int *)0);
@@ -1084,8 +1094,9 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__retres);
if (__retres >= 0) {
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",(void *)__gen_e_acsl_at);
- __gen_e_acsl_and = __gen_e_acsl_at != (int *)0;
+ "\\old(stat_loc)",
+ (void *)__gen_e_acsl_at_2);
+ __gen_e_acsl_and = __gen_e_acsl_at_2 != (int *)0;
}
else __gen_e_acsl_and = 0;
if (! __gen_e_acsl_and) __gen_e_acsl_implies = 1;
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
index c71892de48014543d30c8555794adacf3a65e450..667933a94dbeb38cd0bd72751672019c24045d62 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -63,8 +63,8 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
FILE * restrict stream)
{
size_t __gen_e_acsl_at_3;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- void *__gen_e_acsl_at;
+ void *__gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at;
size_t __retres;
{
__e_acsl_mpz_t __gen_e_acsl_size;
@@ -88,10 +88,10 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& stream),8UL);
__e_acsl_store_block((void *)(& ptr),8UL);
- __gen_e_acsl_at = ptr;
__gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_2 = ptr;
__gen_e_acsl_at_3 = nmemb;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
@@ -293,7 +293,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init(__gen_e_acsl_mul_4);
__gmpz_mul(__gen_e_acsl_mul_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
@@ -343,11 +343,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert(__gen_e_acsl_le_5 <= 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gen_e_acsl_size_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at_2 +
1 * 0),
__gen_e_acsl_size_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(ptr)",
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
@@ -356,7 +356,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__retres);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
@@ -390,7 +390,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_clear(__gen_e_acsl_mul_5);
__gmpz_clear(__gen_e_acsl_if_2);
__gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
index 81522c937fe323622587aadf2e3d27d16dad21fc..2080a3093e2a5d4d02b7d926e23ad669630ec33e 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -404,16 +404,18 @@ int main(void)
*/
void *__gen_e_acsl_memset(void *s, int c, size_t n)
{
- size_t __gen_e_acsl_at_3;
- int __gen_e_acsl_at_2;
+ void *__gen_e_acsl_at_4;
+ int __gen_e_acsl_at_3;
+ size_t __gen_e_acsl_at_2;
void *__gen_e_acsl_at;
void *__retres;
{
int __gen_e_acsl_valid_or_empty_here_2;
__e_acsl_store_block((void *)(& s),8UL);
__gen_e_acsl_at = s;
- __gen_e_acsl_at_2 = c;
- __gen_e_acsl_at_3 = n;
+ __gen_e_acsl_at_2 = n;
+ __gen_e_acsl_at_3 = c;
+ __gen_e_acsl_at_4 = s;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_or_empty_here_2 = __gen_e_acsl_valid_or_empty_here
(s,n);
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
index 6076da2825889a309e1dabd99c585fb4720a596c..a4b1a052376bf9ef8b517c0f475d19f8ed5df1e5 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -397,11 +397,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- __e_acsl_mpz_t __gen_e_acsl_at_5;
- char const *__gen_e_acsl_at_4;
- char *__gen_e_acsl_at_3;
+ char *__gen_e_acsl_at_5;
+ char *__gen_e_acsl_at_4;
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
char *__gen_e_acsl_at_2;
- char *__gen_e_acsl_at;
+ char const *__gen_e_acsl_at;
char *__retres;
{
__e_acsl_mpz_t __gen_e_acsl_n;
@@ -432,13 +432,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
- __gen_e_acsl_at = dest;
+ __gen_e_acsl_at = src;
__gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at_3 = dest;
- __gen_e_acsl_at_4 = src;
__gmpz_init_set_ui(__gen_e_acsl_n,n);
- __gmpz_init_set(__gen_e_acsl_at_5,
+ __gmpz_init_set(__gen_e_acsl_at_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gen_e_acsl_at_4 = dest;
+ __gen_e_acsl_at_5 = dest;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -620,7 +620,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result",
(void *)__retres);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(dest)",
- (void *)__gen_e_acsl_at_3);
+ (void *)__gen_e_acsl_at_5);
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "Postcondition";
__gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(dest)";
@@ -628,7 +628,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_6.fct = "strncpy";
__gen_e_acsl_assert_data_6.line = 437;
__gen_e_acsl_assert_data_6.name = "result_ptr";
- __e_acsl_assert(__retres == __gen_e_acsl_at_3,
+ __e_acsl_assert(__retres == __gen_e_acsl_at_5,
& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
@@ -636,7 +636,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__gen_e_acsl_sub_4);
@@ -651,17 +651,17 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_size_6 = 1UL * __gen_e_acsl__10;
if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_6 = 0UL;
else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_4 +
1 * 0),
__gen_e_acsl_if_6);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"\\old(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
__gen_e_acsl_size_6);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
@@ -686,7 +686,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_clear(__gen_e_acsl__9);
__gmpz_clear(__gen_e_acsl_sub_4);
__gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_at_5);
+ __gmpz_clear(__gen_e_acsl_at_3);
return __retres;
}
}
@@ -706,15 +706,15 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
unsigned long __gen_e_acsl_strcpy_src_size;
- char const *__gen_e_acsl_at_3;
- char *__gen_e_acsl_at_2;
+ char *__gen_e_acsl_at_3;
+ char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
- __gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at_3 = src;
+ __gen_e_acsl_at_2 = src;
+ __gen_e_acsl_at_3 = dest;
__gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
index 6fb11fbc1086ecc71d844419e4c02596e54227d5..b61de0193365722eb37c1ef30d0b5f15fd5fb131 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
@@ -801,8 +801,8 @@ int main(void)
*/
void __gen_e_acsl_g(long *ptr, size_t size)
{
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- long *__gen_e_acsl_at;
+ long *__gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at;
{
__e_acsl_mpz_t __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_size_2;
@@ -821,10 +821,10 @@ void __gen_e_acsl_g(long *ptr, size_t size)
unsigned long __gen_e_acsl_size_4;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& ptr),8UL);
- __gen_e_acsl_at = ptr;
__gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_2 = ptr;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gmpz_init_set_si(__gen_e_acsl_sizeof,8L);
__gmpz_init_set_ui(__gen_e_acsl_size_3,size);
@@ -940,7 +940,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_init_set_si(__gen_e_acsl__5,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_at),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__gmpz_init_set_si(__gen_e_acsl__6,0L);
__gmpz_init(__gen_e_acsl_sub_3);
@@ -986,20 +986,20 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_assert(__gen_e_acsl_le_4 <= 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__gen_e_acsl_size_6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at +
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at_2 +
8 * 0),
__gen_e_acsl_size_6,
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"\\old(ptr)",
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(long)",
0,8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(long)",
0,8);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"size",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"size",0,
@@ -1029,7 +1029,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl_mul_2);
__gmpz_clear(__gen_e_acsl_if_2);
__gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at);
return;
}
}
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index e03df15a615064ed5a156a094c597055581026d7..b801bccbed31cf76400fa73cdb7fb16d9c2c6331 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -739,8 +739,9 @@ int main(void)
*/
void *__gen_e_acsl_memset(void *s, int c, size_t n)
{
- size_t __gen_e_acsl_at_3;
- int __gen_e_acsl_at_2;
+ void *__gen_e_acsl_at_4;
+ int __gen_e_acsl_at_3;
+ size_t __gen_e_acsl_at_2;
void *__gen_e_acsl_at;
void *__retres;
{
@@ -748,8 +749,9 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_store_block((void *)(& s),8UL);
__e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
__gen_e_acsl_at = s;
- __gen_e_acsl_at_2 = c;
- __gen_e_acsl_at_3 = n;
+ __gen_e_acsl_at_2 = n;
+ __gen_e_acsl_at_3 = c;
+ __gen_e_acsl_at_4 = s;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_or_empty_here_2 = __gen_e_acsl_valid_or_empty_here
(s,n);