diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
index e3d1f599319d187431b2c7d54111caab3242d2b2..d6a548d80f8f3c82fbf5542d05b6e8e0542acb2e 100644
--- a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
@@ -56,7 +56,7 @@ module Pred_or_term =
List.fold_left
(fun reprs t -> PoT_term t :: reprs)
[]
- Term.reprs
+ Misc.Id_term.reprs
in
List.fold_left
(fun reprs p -> PoT_pred p :: reprs)
@@ -65,18 +65,19 @@ module Pred_or_term =
include Datatype.Undefined
- let compare pot1 pot2 =
- match pot1, pot2 with
- | PoT_pred _, PoT_term _ -> -1
- | PoT_term _, PoT_pred _ -> 1
- | PoT_pred p1, PoT_pred p2 -> PredicateStructEq.compare p1 p2
- | PoT_term t1, PoT_term t2 -> Term.compare t1 t2
+ let compare _ _ =
+ (* see [Misc.Id_term.compare] *)
+ Kernel.fatal "Pred_or_term: comparison undefined (and undefinable)"
- let equal = Datatype.from_compare
+ let equal pot1 pot2 =
+ match pot1, pot2 with
+ | PoT_pred p1, PoT_pred p2 -> PredicateStructEq.equal p1 p2
+ | PoT_term t1, PoT_term t2 -> Misc.Id_term.equal t1 t2
+ | _ -> false
let hash = function
| PoT_pred p -> 7 * PredicateStructEq.hash p
- | PoT_term t -> 97 * Term.hash t
+ | PoT_term t -> 97 * Misc.Id_term.hash t
let pretty fmt = function
| PoT_pred p -> Printer.pp_predicate fmt p
@@ -151,11 +152,10 @@ let basic_pp_kinstr fmt kinstr =
(** Basic comparison for two [kinstr], i.e. two [Kstmt] are always equal
regardless of the statement value (contrary to [Cil_datatype.Kinstr.compare]
where two [Kstmt] are compared with their included statement's [sid]). *)
-let basic_kinstr_compare kinstr1 kinstr2 =
+let basic_kinstr_equal kinstr1 kinstr2 =
match kinstr1, kinstr2 with
- | Kglobal, Kglobal | Kstmt _, Kstmt _ -> 0
- | Kglobal, _ -> 1
- | _, Kglobal -> -1
+ | Kglobal, Kglobal | Kstmt _, Kstmt _ -> true
+ | _ -> false
(** Basic hash function for a [kinstr], i.e. contrary to
[Cil_datatype.Kinstr.hash] the statement of the [Kstmt] is not considered
@@ -195,39 +195,20 @@ module At_data = struct
include Datatype.Undefined
- let compare
- { kf = kf1;
- kinstr = kinstr1;
- lscope = lscope1;
- pot = pot1;
- label = label1 }
- { kf = kf2;
- kinstr = kinstr2;
- lscope = lscope2;
- pot = pot2;
- label = label2 }
- =
- let cmp = Kf.compare kf1 kf2 in
- let cmp =
- if cmp = 0 then
- basic_kinstr_compare kinstr1 kinstr2
- else cmp
- in
- let cmp =
- if cmp = 0 then Lscope.D.compare lscope1 lscope2
- else cmp
- in
- let cmp =
- if cmp = 0 then Pred_or_term.compare pot1 pot2
- else cmp
- in
- if cmp = 0 then
- let elabel1 = Ext_logic_label.get kinstr1 label1 in
- let elabel2 = Ext_logic_label.get kinstr2 label2 in
- Ext_logic_label.compare elabel1 elabel2
- else cmp
-
- let equal = Datatype.from_compare
+ let compare _ _ =
+ (* see [Misc.Id_term.compare] *)
+ Kernel.fatal "At_data: comparison undefined (and undefinable)"
+
+ let equal
+ {kf = kf1; kinstr = kinstr1; lscope = ls1; pot = pot1; label = l1}
+ {kf = kf2; kinstr = kinstr2; lscope = ls2; pot = pot2; label = l2} =
+ Kf.equal kf1 kf2 &&
+ basic_kinstr_equal kinstr1 kinstr2 &&
+ Lscope.D.equal ls1 ls2 &&
+ Pred_or_term.equal pot1 pot2 &&
+ let elabel1 = Ext_logic_label.get kinstr1 l1 in
+ let elabel2 = Ext_logic_label.get kinstr2 l2 in
+ Ext_logic_label.equal elabel1 elabel2
let hash { kf; kinstr; lscope; pot; label } =
let elabel = Ext_logic_label.get kinstr label in
diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
index 444219dfc2f390c8d5bc874b373e4577df1100ec..59849829d9a67c32d0d86cffcf0f1c711674c002 100644
--- a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
@@ -28,6 +28,10 @@ open Cil_datatype
module Annotation_kind: Datatype.S with type t = annotation_kind
+(** Predicate or term. Note that the notion of egality for predicates is
+ structural but for terms it is physical (using [Misc.Id_term]). That means
+ that comparison is undefined and that [Map] and [Set] cannot be used. See
+ [Misc.Id_term] for more information. *)
module Pred_or_term: Datatype.S_with_collections with type t = pred_or_term
module At_data: sig
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
index 422529ed4132579b993634938b304577bfc29d2a..c1c0d8c809403a9d280978b637eb79fc82e9ef3f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
@@ -11,6 +11,12 @@
[eva:alarm] at.i:77: Warning: assertion got status unknown.
[eva:alarm] at.i:78: Warning: assertion got status unknown.
[eva:alarm] at.i:79: Warning: assertion got status unknown.
+[eva:alarm] at.i:43: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] at.i:41: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] at.i:39: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
index b45b4d727ceb341debedf941fc93c446accf8d72..dcb1f8a7a9557f5fb4b3252b13d5a637471b1d13 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,3 +1,7 @@
+[kernel:CERT:MSC:37] functions.c:122: Warning:
+ Body of function f5 falls-through. Adding a return statement
+[kernel:CERT:MSC:37] functions.c:126: Warning:
+ Body of function test_f5 falls-through. Adding a return statement
[e-acsl] beginning translation.
[e-acsl] functions.c:81: Warning:
E-ACSL construct `function application' is not yet supported.
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 6c066086426c41ccfe9d811bfc6b45a1cc1c64ec..f869913749cff6fb6e59c8ffe43152312b6e9825 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -18,26 +18,30 @@ void __gen_e_acsl_f(void);
void f(void)
{
+ int __gen_e_acsl_at_6;
+ int __gen_e_acsl_at_5;
int __gen_e_acsl_at_4;
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
__gen_e_acsl_at = A;
+ __gen_e_acsl_at_2 = A;
+ __gen_e_acsl_at_3 = A;
A = 1;
- F: __gen_e_acsl_at_2 = A;
- __gen_e_acsl_at_3 = __gen_e_acsl_at;
+ F: __gen_e_acsl_at_4 = A;
+ __gen_e_acsl_at_5 = __gen_e_acsl_at_2;
A = 2;
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"\\at(A,Pre)",0,
- __gen_e_acsl_at);
+ __gen_e_acsl_at_3);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
__gen_e_acsl_assert_data.pred_txt = "\\at(A,Pre) == 0";
__gen_e_acsl_assert_data.file = "at.i";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 16;
- __e_acsl_assert(__gen_e_acsl_at == 0,& __gen_e_acsl_assert_data);
+ __e_acsl_assert(__gen_e_acsl_at_3 == 0,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
/*@ assert \at(A,Pre) == 0; */ ;
@@ -45,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_2);
+ __gen_e_acsl_at_4);
__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_2 == 1,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_at_4 == 1,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \at(A,F) == 1; */ ;
@@ -74,21 +78,21 @@ 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_3);
+ "\\at(\\at(A,Pre),F)",0,__gen_e_acsl_at_5);
__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_3 == 0,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_at_5 == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \at(\at(A,Pre),F) == 0; */ ;
A = 3;
{
{
- __gen_e_acsl_at_4 = A;
+ __gen_e_acsl_at_6 = A;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"A",0,A);
@@ -122,14 +126,14 @@ void f(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"\\old(A)",0,
- __gen_e_acsl_at_4);
+ __gen_e_acsl_at_6);
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "Postcondition";
__gen_e_acsl_assert_data_7.pred_txt = "\\old(A) == 3";
__gen_e_acsl_assert_data_7.file = "at.i";
__gen_e_acsl_assert_data_7.fct = "f";
__gen_e_acsl_assert_data_7.line = 23;
- __e_acsl_assert(__gen_e_acsl_at_4 == 3,& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert(__gen_e_acsl_at_6 == 3,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
@@ -148,6 +152,8 @@ void f(void)
void g(int *p, int *q)
{
+ int __gen_e_acsl_at_5;
+ int __gen_e_acsl_at_4;
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
@@ -162,6 +168,8 @@ void g(int *p, int *q)
L1:
{
int __gen_e_acsl_valid_read;
+ int __gen_e_acsl_valid_read_2;
+ int __gen_e_acsl_valid_read_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,(void *)(& q));
@@ -173,88 +181,100 @@ void g(int *p, int *q)
__gen_e_acsl_assert_data.pred_txt = "\\valid_read(q)";
__gen_e_acsl_assert_data.file = "at.i";
__gen_e_acsl_assert_data.fct = "g";
- __gen_e_acsl_assert_data.line = 39;
+ __gen_e_acsl_assert_data.line = 43;
__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 = *q;
- __e_acsl_initialize((void *)p,sizeof(int));
- }
- *p = 2;
- __e_acsl_initialize((void *)(p + 1),sizeof(int));
- *(p + 1) = 3;
- __e_acsl_initialize((void *)q,sizeof(int));
- *q = 1;
- L2:
- {
- 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 *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"p",(void *)p);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "__gen_e_acsl_at",0,__gen_e_acsl_at);
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"q",(void *)q);
__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(p + __gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(q)";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "g";
- __gen_e_acsl_assert_data_2.line = 39;
+ __gen_e_acsl_assert_data_2.line = 41;
__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 = *(p + __gen_e_acsl_at);
- }
- A = 4;
- {
+ __gen_e_acsl_at_2 = *q;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "\\at(*(p + \\at(*q,L1)),L2)",0,
- __gen_e_acsl_at_2);
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"q",(void *)q);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
+ "sizeof(int)",0,sizeof(int));
__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(*(p + \\at(*q,L1)),L2) == 2";
+ __gen_e_acsl_assert_data_3.kind = "RTE";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(q)";
__gen_e_acsl_assert_data_3.file = "at.i";
__gen_e_acsl_assert_data_3.fct = "g";
__gen_e_acsl_assert_data_3.line = 39;
- __e_acsl_assert(__gen_e_acsl_at_2 == 2,& __gen_e_acsl_assert_data_3);
+ __gen_e_acsl_assert_data_3.name = "mem_access";
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __gen_e_acsl_at_3 = *q;
+ __e_acsl_initialize((void *)p,sizeof(int));
}
- /*@ assert \at(*(p + \at(*q,L1)),L2) == 2; */ ;
- L3:
+ *p = 2;
+ __e_acsl_initialize((void *)(p + 1),sizeof(int));
+ *(p + 1) = 3;
+ __e_acsl_initialize((void *)q,sizeof(int));
+ *q = 1;
+ L2:
{
- int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_read_4;
__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 *)(p + __gen_e_acsl_at),
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"p",(void *)p);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
- "__gen_e_acsl_at",0,__gen_e_acsl_at);
+ "__gen_e_acsl_at_3",0,__gen_e_acsl_at_3);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
__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(p + __gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(p + __gen_e_acsl_at_3)";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "g";
- __gen_e_acsl_assert_data_4.line = 43;
+ __gen_e_acsl_assert_data_4.line = 39;
__gen_e_acsl_assert_data_4.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_3,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
- __gen_e_acsl_at_3 = *(p + __gen_e_acsl_at);
+ __gen_e_acsl_at_4 = *(p + __gen_e_acsl_at_3);
+ }
+ A = 4;
+ {
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
+ "\\at(*(p + \\at(*q,L1)),L2)",0,
+ __gen_e_acsl_at_4);
+ __gen_e_acsl_assert_data_5.blocking = 1;
+ __gen_e_acsl_assert_data_5.kind = "Assertion";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\at(*(p + \\at(*q,L1)),L2) == 2";
+ __gen_e_acsl_assert_data_5.file = "at.i";
+ __gen_e_acsl_assert_data_5.fct = "g";
+ __gen_e_acsl_assert_data_5.line = 39;
+ __e_acsl_assert(__gen_e_acsl_at_4 == 2,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ }
+ /*@ assert \at(*(p + \at(*q,L1)),L2) == 2; */ ;
+ L3:
+ {
+ int __gen_e_acsl_valid_read_5;
+ int __gen_e_acsl_valid_read_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"p",(void *)p);
@@ -267,38 +287,61 @@ void g(int *p, int *q)
__gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(p + __gen_e_acsl_at)";
__gen_e_acsl_assert_data_6.file = "at.i";
__gen_e_acsl_assert_data_6.fct = "g";
- __gen_e_acsl_assert_data_6.line = 41;
+ __gen_e_acsl_assert_data_6.line = 43;
__gen_e_acsl_assert_data_6.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_4,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__gen_e_acsl_valid_read_5,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
- "*(p + \\at(*q,L1))",0,
- *(p + __gen_e_acsl_at));
- __gen_e_acsl_assert_data_5.blocking = 1;
- __gen_e_acsl_assert_data_5.kind = "Assertion";
- __gen_e_acsl_assert_data_5.pred_txt = "\\at(*(p + \\at(*q,L1)),Here) == 2";
- __gen_e_acsl_assert_data_5.file = "at.i";
- __gen_e_acsl_assert_data_5.fct = "g";
- __gen_e_acsl_assert_data_5.line = 41;
- __e_acsl_assert(*(p + __gen_e_acsl_at) == 2,& __gen_e_acsl_assert_data_5);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- }
- /*@ assert \at(*(p + \at(*q,L1)),Here) == 2; */ ;
- {
+ __gen_e_acsl_at_5 = *(p + __gen_e_acsl_at);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
+ {.values = (void *)0};
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_2),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,"p",(void *)p);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
+ "__gen_e_acsl_at_2",0,__gen_e_acsl_at_2);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_8,
+ "sizeof(int)",0,sizeof(int));
+ __gen_e_acsl_assert_data_8.blocking = 1;
+ __gen_e_acsl_assert_data_8.kind = "RTE";
+ __gen_e_acsl_assert_data_8.pred_txt = "\\valid_read(p + __gen_e_acsl_at_2)";
+ __gen_e_acsl_assert_data_8.file = "at.i";
+ __gen_e_acsl_assert_data_8.fct = "g";
+ __gen_e_acsl_assert_data_8.line = 41;
+ __gen_e_acsl_assert_data_8.name = "mem_access";
+ __e_acsl_assert(__gen_e_acsl_valid_read_6,& __gen_e_acsl_assert_data_8);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
- "\\at(*(p + \\at(*q,L1)),L3)",0,
- __gen_e_acsl_at_3);
+ "*(p + \\at(*q,L1))",0,
+ *(p + __gen_e_acsl_at_2));
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "Assertion";
- __gen_e_acsl_assert_data_7.pred_txt = "\\at(*(p + \\at(*q,L1)),L3) == 2";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\at(*(p + \\at(*q,L1)),Here) == 2";
__gen_e_acsl_assert_data_7.file = "at.i";
__gen_e_acsl_assert_data_7.fct = "g";
- __gen_e_acsl_assert_data_7.line = 43;
- __e_acsl_assert(__gen_e_acsl_at_3 == 2,& __gen_e_acsl_assert_data_7);
+ __gen_e_acsl_assert_data_7.line = 41;
+ __e_acsl_assert(*(p + __gen_e_acsl_at_2) == 2,
+ & __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
}
+ /*@ assert \at(*(p + \at(*q,L1)),Here) == 2; */ ;
+ {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,
+ "\\at(*(p + \\at(*q,L1)),L3)",0,
+ __gen_e_acsl_at_5);
+ __gen_e_acsl_assert_data_9.blocking = 1;
+ __gen_e_acsl_assert_data_9.kind = "Assertion";
+ __gen_e_acsl_assert_data_9.pred_txt = "\\at(*(p + \\at(*q,L1)),L3) == 2";
+ __gen_e_acsl_assert_data_9.file = "at.i";
+ __gen_e_acsl_assert_data_9.fct = "g";
+ __gen_e_acsl_assert_data_9.line = 43;
+ __e_acsl_assert(__gen_e_acsl_at_5 == 2,& __gen_e_acsl_assert_data_9);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
+ }
/*@ assert \at(*(p + \at(*q,L1)),L3) == 2; */ ;
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
@@ -362,8 +405,9 @@ void i(void)
int main(void)
{
- long __gen_e_acsl_at_2;
- int __gen_e_acsl_at;
+ long __gen_e_acsl_at_3;
+ int __gen_e_acsl_at_2;
+ long __gen_e_acsl_at;
int __retres;
int x;
int t[2];
@@ -374,8 +418,9 @@ int main(void)
x = __gen_e_acsl_h(0);
L:
{
- __gen_e_acsl_at = x;
- __gen_e_acsl_at_2 = x + 1L;
+ __gen_e_acsl_at = (long)x;
+ __gen_e_acsl_at_2 = x;
+ __gen_e_acsl_at_3 = x + 1L;
__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;
@@ -397,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);
+ __gen_e_acsl_at_2);
__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 == 0,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_at_2 == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \at(x,L) == 0; */ ;
@@ -412,30 +457,29 @@ 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_2);
+ "\\at(x + 1,L)",0,__gen_e_acsl_at_3);
__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_2 == 1L,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert(__gen_e_acsl_at_3 == 1L,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
/*@ assert \at(x + 1,L) == 1; */ ;
{
__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(x,L)",0,
- __gen_e_acsl_at);
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_4,"\\at(x,L)",0,
+ __gen_e_acsl_at);
__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(x,L) + 1 == 1";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 79;
- __e_acsl_assert((long)__gen_e_acsl_at + 1L == 1L,
- & __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_at + 1L == 1L,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \at(x,L) + 1 == 1; */ ;
@@ -484,11 +528,13 @@ int __gen_e_acsl_h(int x)
*/
void __gen_e_acsl_f(void)
{
+ int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
{
__gen_e_acsl_at = A;
__gen_e_acsl_at_2 = A;
+ __gen_e_acsl_at_3 = A;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"A",0,A);
__gen_e_acsl_assert_data.blocking = 1;
@@ -501,15 +547,14 @@ void __gen_e_acsl_f(void)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__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,Pre)",
- 0,__gen_e_acsl_at_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"A",0,A);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "\\at(A,Pre) == 0";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 9;
- __e_acsl_assert(__gen_e_acsl_at_2 == 0,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(A == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
f();
@@ -518,10 +563,10 @@ void __gen_e_acsl_f(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"\\at(A,Pre)",
- 0,__gen_e_acsl_at_2);
+ 0,__gen_e_acsl_at_3);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"\\old(A)",0,
- __gen_e_acsl_at);
- if (__gen_e_acsl_at_2 == __gen_e_acsl_at) {
+ __gen_e_acsl_at_2);
+ if (__gen_e_acsl_at_3 == __gen_e_acsl_at_2) {
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"\\old(A)",0,
__gen_e_acsl_at);
__gen_e_acsl_and = __gen_e_acsl_at == 0;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index 9f9358add8a131caac5f6a515f64a5a15ecf2a75..490dff8e59b38f16b30b4401ed5d7866fac82e67 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -613,6 +613,128 @@ void test_f4(void)
return;
}
+/*@ behavior a:
+ ensures 1 == -\old(j);
+
+ behavior b:
+ ensures 2 == \old(j); */
+int __gen_e_acsl_f5(long j);
+
+int f5(long j)
+{
+ int __retres;
+ {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "\\false";
+ __gen_e_acsl_assert_data.file = "functions.c";
+ __gen_e_acsl_assert_data.fct = "f5";
+ __gen_e_acsl_assert_data.line = 122;
+ __gen_e_acsl_assert_data.name = "missing_return";
+ __e_acsl_assert(0,& __gen_e_acsl_assert_data);
+ }
+ /*@ assert missing_return: \false; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+int test_f5(void)
+{
+ int __retres;
+ __gen_e_acsl_f5((long)1);
+ {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "\\false";
+ __gen_e_acsl_assert_data.file = "functions.c";
+ __gen_e_acsl_assert_data.fct = "test_f5";
+ __gen_e_acsl_assert_data.line = 126;
+ __gen_e_acsl_assert_data.name = "missing_return";
+ __e_acsl_assert(0,& __gen_e_acsl_assert_data);
+ }
+ /*@ assert missing_return: \false; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+/*@ behavior a:
+ ensures 1 == -\old(j);
+
+ behavior b:
+ ensures 2 == \old(j); */
+int __gen_e_acsl_f5(long j)
+{
+ __e_acsl_contract_t *__gen_e_acsl_contract;
+ __e_acsl_mpz_t __gen_e_acsl_at_2;
+ long __gen_e_acsl_at;
+ int __retres;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_j;
+ __gen_e_acsl_at = j;
+ __gmpz_init_set_si(__gen_e_acsl_j,j);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_j));
+ __gen_e_acsl_contract = __e_acsl_contract_init(2UL);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL,1);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,1UL,1);
+ __gmpz_clear(__gen_e_acsl_j);
+ }
+ __retres = f5(j);
+ {
+ int __gen_e_acsl_assumes_value;
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,0UL);
+ if (__gen_e_acsl_assumes_value) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_neg;
+ int __gen_e_acsl_eq;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data =
+ {.values = (void *)0};
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_neg);
+ __gmpz_neg(__gen_e_acsl_neg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"\\old(j)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Postcondition";
+ __gen_e_acsl_assert_data.pred_txt = "1 == -\\old(j)";
+ __gen_e_acsl_assert_data.file = "functions.c";
+ __gen_e_acsl_assert_data.fct = "f5";
+ __gen_e_acsl_assert_data.line = 118;
+ __gen_e_acsl_assert_data.name = "a";
+ __e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_neg);
+ }
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,1UL);
+ if (__gen_e_acsl_assumes_value) {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_2,"\\old(j)",
+ 0,__gen_e_acsl_at);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Postcondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "2 == \\old(j)";
+ __gen_e_acsl_assert_data_2.file = "functions.c";
+ __gen_e_acsl_assert_data_2.fct = "f5";
+ __gen_e_acsl_assert_data_2.line = 120;
+ __gen_e_acsl_assert_data_2.name = "b";
+ __e_acsl_assert(2L == __gen_e_acsl_at,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ }
+ __e_acsl_contract_clean(__gen_e_acsl_contract);
+ __gmpz_clear(__gen_e_acsl_at_2);
+ return __retres;
+ }
+}
+
/*@ requires k_pred(x); */
void __gen_e_acsl_k(int x)
{
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 e85da85a4b1381606d700317bcae52f1e401da71..f67fbe8bd183ba14e1360edd8f20bd6fc8a42478 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -96,6 +96,9 @@ int main(void)
void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ float *__gen_e_acsl_at_6;
+ float *__gen_e_acsl_at_5;
+ float *__gen_e_acsl_at_4;
float *__gen_e_acsl_at_3;
float *__gen_e_acsl_at_2;
float *__gen_e_acsl_at;
@@ -107,8 +110,11 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__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_2 = Mwmin;
- __gen_e_acsl_at_3 = Mtmin_out;
+ __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_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};
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float),
@@ -181,17 +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,
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
sizeof(float),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_3",
+ (void *)__gen_e_acsl_at_3);
__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)";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(__gen_e_acsl_at_3)";
__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;
@@ -200,36 +207,36 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_6,
sizeof(float),
- (void *)__gen_e_acsl_at_3,
- (void *)(& __gen_e_acsl_at_3));
+ (void *)__gen_e_acsl_at_6,
+ (void *)(& __gen_e_acsl_at_6));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_at_3",
- (void *)__gen_e_acsl_at_3);
+ "__gen_e_acsl_at_6",
+ (void *)__gen_e_acsl_at_6);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"sizeof(float)",0,sizeof(float));
__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_3)";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_6)";
__gen_e_acsl_assert_data_6.file = "bts1307.i";
__gen_e_acsl_assert_data_6.fct = "bar";
__gen_e_acsl_assert_data_6.line = 26;
__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_3 == *__gen_e_acsl_at) {
+ if (*__gen_e_acsl_at_6 == *__gen_e_acsl_at_3) {
__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);
+ __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at_2);
__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_2);
+ __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_5);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
@@ -279,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_2);
+ __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_4);
__gmpq_init(__gen_e_acsl_mul_2);
__gmpq_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
@@ -289,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_2);
+ "*\\old(Mwmin)",*__gen_e_acsl_at_4);
__gen_e_acsl_if = __gen_e_acsl_ne != 0;
__gmpq_clear(__gen_e_acsl__4);
__gmpq_clear(__gen_e_acsl__5);
@@ -297,13 +304,13 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gmpq_clear(__gen_e_acsl__6);
}
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_out)",*__gen_e_acsl_at_3);
+ "*\\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);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at_3);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at_2);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmin)",*__gen_e_acsl_at_2);
+ "*\\old(Mwmin)",*__gen_e_acsl_at_5);
__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.";
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index 8e484ee47ec4cd7a3330c0f58ebd3b89f29d5d1e..e0bb405377cf09009ebedf1983e392a11cecb843 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -57,12 +57,20 @@ int main(void)
void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int *AverageAccel)
{
- int *__gen_e_acsl_at_2;
+ int *__gen_e_acsl_at_6;
+ ArrayInt *__gen_e_acsl_at_5;
+ ArrayInt *__gen_e_acsl_at_4;
+ ArrayInt *__gen_e_acsl_at_3;
+ ArrayInt *__gen_e_acsl_at_2;
ArrayInt *__gen_e_acsl_at;
__e_acsl_store_block((void *)(& AverageAccel),8UL);
__e_acsl_store_block((void *)(& Accel),8UL);
__gen_e_acsl_at = Accel;
- __gen_e_acsl_at_2 = AverageAccel;
+ __gen_e_acsl_at_2 = Accel;
+ __gen_e_acsl_at_3 = Accel;
+ __gen_e_acsl_at_4 = Accel;
+ __gen_e_acsl_at_5 = Accel;
+ __gen_e_acsl_at_6 = AverageAccel;
atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
{
int __gen_e_acsl_valid_read;
@@ -94,18 +102,18 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[1]),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[1]),
sizeof(int),
- (void *)(*__gen_e_acsl_at),
+ (void *)(*__gen_e_acsl_at_2),
(void *)0);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "&(*__gen_e_acsl_at)[1]",
- (void *)(& (*__gen_e_acsl_at)[1]));
+ "&(*__gen_e_acsl_at_2)[1]",
+ (void *)(& (*__gen_e_acsl_at_2)[1]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "RTE";
- __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(&(*__gen_e_acsl_at)[1])";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(&(*__gen_e_acsl_at_2)[1])";
__gen_e_acsl_assert_data_3.file = "bts1326.i";
__gen_e_acsl_assert_data_3.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_3.line = 8;
@@ -114,18 +122,18 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_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 *)(& (*__gen_e_acsl_at)[2]),
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[2]),
sizeof(int),
- (void *)(*__gen_e_acsl_at),
+ (void *)(*__gen_e_acsl_at_3),
(void *)0);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
- "&(*__gen_e_acsl_at)[2]",
- (void *)(& (*__gen_e_acsl_at)[2]));
+ "&(*__gen_e_acsl_at_3)[2]",
+ (void *)(& (*__gen_e_acsl_at_3)[2]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
__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(&(*__gen_e_acsl_at)[2])";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(&(*__gen_e_acsl_at_3)[2])";
__gen_e_acsl_assert_data_4.file = "bts1326.i";
__gen_e_acsl_assert_data_4.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_4.line = 8;
@@ -134,18 +142,18 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[3]),
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[3]),
sizeof(int),
- (void *)(*__gen_e_acsl_at),
+ (void *)(*__gen_e_acsl_at_4),
(void *)0);
__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_4)[3]",
+ (void *)(& (*__gen_e_acsl_at_4)[3]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
"sizeof(int)",0,sizeof(int));
__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_4)[3])";
__gen_e_acsl_assert_data_5.file = "bts1326.i";
__gen_e_acsl_assert_data_5.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_5.line = 8;
@@ -154,18 +162,18 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[4]),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[4]),
sizeof(int),
- (void *)(*__gen_e_acsl_at),
+ (void *)(*__gen_e_acsl_at_5),
(void *)0);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
- "&(*__gen_e_acsl_at)[4]",
- (void *)(& (*__gen_e_acsl_at)[4]));
+ "&(*__gen_e_acsl_at_5)[4]",
+ (void *)(& (*__gen_e_acsl_at_5)[4]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"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)[4])";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(&(*__gen_e_acsl_at_5)[4])";
__gen_e_acsl_assert_data_6.file = "bts1326.i";
__gen_e_acsl_assert_data_6.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_6.line = 8;
@@ -174,18 +182,18 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_6,
sizeof(int),
- (void *)__gen_e_acsl_at_2,
- (void *)(& __gen_e_acsl_at_2));
+ (void *)__gen_e_acsl_at_6,
+ (void *)(& __gen_e_acsl_at_6));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,
- "__gen_e_acsl_at_2",
- (void *)__gen_e_acsl_at_2);
+ "__gen_e_acsl_at_6",
+ (void *)__gen_e_acsl_at_6);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,
"sizeof(int)",0,sizeof(int));
__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_2)";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at_6)";
__gen_e_acsl_assert_data_7.file = "bts1326.i";
__gen_e_acsl_assert_data_7.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_7.line = 8;
@@ -193,19 +201,19 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert(__gen_e_acsl_valid_read_6,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "*\\old(AverageAccel)",0,*__gen_e_acsl_at_2);
+ "*\\old(AverageAccel)",0,*__gen_e_acsl_at_6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[4]",0,
- (*__gen_e_acsl_at)[4]);
+ (*__gen_e_acsl_at_5)[4]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[3]",0,
- (*__gen_e_acsl_at)[3]);
+ (*__gen_e_acsl_at_4)[3]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[2]",0,
- (*__gen_e_acsl_at)[2]);
+ (*__gen_e_acsl_at_3)[2]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[1]",0,
- (*__gen_e_acsl_at)[1]);
+ (*__gen_e_acsl_at_2)[1]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[0]",0,
(*__gen_e_acsl_at)[0]);
@@ -215,7 +223,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__gen_e_acsl_assert_data.file = "bts1326.i";
__gen_e_acsl_assert_data.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data.line = 8;
- __e_acsl_assert(*__gen_e_acsl_at_2 == (int)((((((*__gen_e_acsl_at)[4] + (long)(*__gen_e_acsl_at)[3]) + (*__gen_e_acsl_at)[2]) + (*__gen_e_acsl_at)[1]) + (*__gen_e_acsl_at)[0]) / 5L),
+ __e_acsl_assert(*__gen_e_acsl_at_6 == (int)((((((*__gen_e_acsl_at_5)[4] + (long)(*__gen_e_acsl_at_4)[3]) + (*__gen_e_acsl_at_3)[2]) + (*__gen_e_acsl_at_2)[1]) + (*__gen_e_acsl_at)[0]) / 5L),
& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__e_acsl_delete_block((void *)(& AverageAccel));
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 e6397626eec5ed493b37b2127175735ac0c77c8c..6e05c2f6131c2059f99403a0199e8e14f392efbe 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -54,8 +54,10 @@ 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_3;
- char const *__gen_e_acsl_at_2;
+ __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_2;
char *__gen_e_acsl_at;
char *__retres;
{
@@ -88,9 +90,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
- __gen_e_acsl_at_2 = 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_3,
+ __gmpz_init_set(__gen_e_acsl_at_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -273,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);
+ (void *)__gen_e_acsl_at_3);
__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)";
@@ -281,14 +285,15 @@ 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,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__retres == __gen_e_acsl_at_3,
+ & __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 =
{.values = (void *)0};
__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_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5),
(__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);
@@ -303,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 +
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
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);
+ (void *)__gen_e_acsl_at_2);
__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_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5));
__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,
@@ -338,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_3);
+ __gmpz_clear(__gen_e_acsl_at_5);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index a235f02b21d675b3f6fdc259092829b4b98cbcea..f92bbb706d36669f2be8f6696f20b6de5315fb33 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -678,12 +678,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);
@@ -745,8 +747,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/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 22c523cc0e400b2f2d32a346ef8fafb958ff87f6..34b223989b6af19038935a1480037b00ca2df386 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -248,12 +248,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);
@@ -315,8 +317,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/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 08a859cae3870b75595d0c5de2dc1ed0efd8a12f..12582f8bbbcb1d14ca53dc4ea75a32af35ff6cf8 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -661,12 +661,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);
@@ -728,8 +730,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/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 72856675c7256d5ff38179c189fcb2ddcbc1675e..1ec8397bd9c73ab13b40420be2a072ab14b535dc 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -222,12 +222,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);
@@ -289,8 +291,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/constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
index 3b8e64f41acc0ee9952ffd244849dc326049ee49..373c5d7a30c32a68abc02346380835d42632842a 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
@@ -229,11 +229,19 @@ int main(void)
void __gen_e_acsl_o(void)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int __gen_e_acsl_at_5;
+ int __gen_e_acsl_at_4;
+ int __gen_e_acsl_at_3;
+ int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
{
int __gen_e_acsl_assumes_value;
int __gen_e_acsl_active_bhvrs;
__gen_e_acsl_at = Y;
+ __gen_e_acsl_at_2 = Y;
+ __gen_e_acsl_at_3 = Y;
+ __gen_e_acsl_at_4 = Y;
+ __gen_e_acsl_at_5 = Y;
__gen_e_acsl_contract = __e_acsl_contract_init(4UL);
__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);
@@ -390,14 +398,14 @@ void __gen_e_acsl_o(void)
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_12,"X",0,X);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_12,"\\old(Y)",0,
- __gen_e_acsl_at);
+ __gen_e_acsl_at_5);
__gen_e_acsl_assert_data_12.blocking = 1;
__gen_e_acsl_assert_data_12.kind = "Postcondition";
__gen_e_acsl_assert_data_12.pred_txt = "X == \\old(Y)";
__gen_e_acsl_assert_data_12.file = "function_contract.i";
__gen_e_acsl_assert_data_12.fct = "o";
__gen_e_acsl_assert_data_12.line = 94;
- __e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_12);
+ __e_acsl_assert(X == __gen_e_acsl_at_5,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
__gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,0UL);
@@ -406,7 +414,7 @@ void __gen_e_acsl_o(void)
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,"X",0,X);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,"\\old(Y)",
- 0,__gen_e_acsl_at);
+ 0,__gen_e_acsl_at_4);
__gen_e_acsl_assert_data_13.blocking = 1;
__gen_e_acsl_assert_data_13.kind = "Postcondition";
__gen_e_acsl_assert_data_13.pred_txt = "X == \\old(Y)";
@@ -414,7 +422,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_13.fct = "o";
__gen_e_acsl_assert_data_13.line = 99;
__gen_e_acsl_assert_data_13.name = "neg";
- __e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_13);
+ __e_acsl_assert(X == __gen_e_acsl_at_4,& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
}
__gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
@@ -424,7 +432,7 @@ void __gen_e_acsl_o(void)
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,"X",0,X);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,"\\old(Y)",
- 0,__gen_e_acsl_at);
+ 0,__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_14.blocking = 1;
__gen_e_acsl_assert_data_14.kind = "Postcondition";
__gen_e_acsl_assert_data_14.pred_txt = "X == \\old(Y)";
@@ -432,7 +440,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_14.fct = "o";
__gen_e_acsl_assert_data_14.line = 104;
__gen_e_acsl_assert_data_14.name = "pos";
- __e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_14);
+ __e_acsl_assert(X == __gen_e_acsl_at_3,& __gen_e_acsl_assert_data_14);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
}
__gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
@@ -442,7 +450,7 @@ void __gen_e_acsl_o(void)
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_15,"X",0,X);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_15,"\\old(Y)",
- 0,__gen_e_acsl_at);
+ 0,__gen_e_acsl_at_2);
__gen_e_acsl_assert_data_15.blocking = 1;
__gen_e_acsl_assert_data_15.kind = "Postcondition";
__gen_e_acsl_assert_data_15.pred_txt = "X == \\old(Y)";
@@ -450,7 +458,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_15.fct = "o";
__gen_e_acsl_assert_data_15.line = 109;
__gen_e_acsl_assert_data_15.name = "odd";
- __e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_15);
+ __e_acsl_assert(X == __gen_e_acsl_at_2,& __gen_e_acsl_assert_data_15);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
}
__gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
index 0fdf520c053564fee249660efb0d726f42be6925..578c1350215e2912fa47560fd59ee61786c92d33 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
@@ -112,25 +112,27 @@ int __gen_e_acsl_g(int x)
/*@ ensures \result == (int)(\old(x) - \old(x)); */
int __gen_e_acsl_f(int x)
{
- long __gen_e_acsl_at;
+ long __gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
int __retres;
- __gen_e_acsl_at = (long)x;
+ __gen_e_acsl_at = x;
+ __gen_e_acsl_at_2 = (long)x;
__retres = f(x);
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"\\result",0,
__retres);
__e_acsl_assert_register_long(& __gen_e_acsl_assert_data,"\\old(x)",0,
- __gen_e_acsl_at);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,"\\old(x)",0,
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"\\old(x)",0,
+ __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 = "\\result == (int)(\\old(x) - \\old(x))";
__gen_e_acsl_assert_data.file = "result.i";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 5;
- __e_acsl_assert(__retres == (int)(__gen_e_acsl_at - __gen_e_acsl_at),
+ __e_acsl_assert(__retres == (int)(__gen_e_acsl_at_2 - __gen_e_acsl_at),
& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
return __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle
index 8b89a531d8c6f7499c7c29b67f3416e881c3809a..c154bf096dd6e181a09a9350cf0c8e3b0ed7ab83 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle
@@ -4,8 +4,8 @@
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] result.i:5: Warning:
- function __e_acsl_assert_register_long: precondition data->values == \null ||
- \valid(data->values) got status unknown.
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] result.i:13: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index ed7d5351a40d9b0e83800814275cc156bb380ccf..d9fae2605f627267a48f805d6f16e740b5bbe420 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -156,12 +156,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);
@@ -223,8 +225,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_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
index e41ebd61ec3c6acf70f8a66e6dde2be3f68edbfb..6076da2825889a309e1dabd99c585fb4720a596c 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -169,11 +169,15 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
unsigned long __gen_e_acsl_strcat_dest_size;
unsigned long __gen_e_acsl_strcat_src_size;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at_3;
+ char *__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 = dest;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__gen_e_acsl_strcat_src_size = __e_acsl_builtin_strlen(src);
if (n < __gen_e_acsl_strcat_src_size) __gen_e_acsl_strcat_src_size = n;
@@ -236,7 +240,7 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,"\\result",
(void *)__retres);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,"\\old(dest)",
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "Postcondition";
__gen_e_acsl_assert_data_9.pred_txt = "\\result == \\old(dest)";
@@ -244,7 +248,8 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_9.fct = "strncat";
__gen_e_acsl_assert_data_9.line = 504;
__gen_e_acsl_assert_data_9.name = "result_ptr";
- __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_9);
+ __e_acsl_assert(__retres == __gen_e_acsl_at_3,
+ & __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
__e_acsl_contract_clean(__gen_e_acsl_contract);
__e_acsl_delete_block((void *)(& src));
@@ -282,11 +287,17 @@ char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
{
unsigned long __gen_e_acsl_strcat_dest_size;
unsigned long __gen_e_acsl_strcat_src_size;
+ char *__gen_e_acsl_at_4;
+ char *__gen_e_acsl_at_3;
+ char *__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 = dest;
+ __gen_e_acsl_at_4 = dest;
__gen_e_acsl_strcat_src_size = __e_acsl_builtin_strlen(src);
__gen_e_acsl_strcat_dest_size = __e_acsl_builtin_strlen((char const *)dest);
__retres = strcat(dest,src);
@@ -386,8 +397,10 @@ 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_3;
- char const *__gen_e_acsl_at_2;
+ __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_2;
char *__gen_e_acsl_at;
char *__retres;
{
@@ -420,9 +433,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
- __gen_e_acsl_at_2 = 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_3,
+ __gmpz_init_set(__gen_e_acsl_at_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -605,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);
+ (void *)__gen_e_acsl_at_3);
__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)";
@@ -613,14 +628,15 @@ 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,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__retres == __gen_e_acsl_at_3,
+ & __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 =
{.values = (void *)0};
__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_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5),
(__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);
@@ -635,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 +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
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);
+ (void *)__gen_e_acsl_at_2);
__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_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_5));
__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,
@@ -670,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_3);
+ __gmpz_clear(__gen_e_acsl_at_5);
return __retres;
}
}
@@ -690,13 +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_2;
+ char const *__gen_e_acsl_at_3;
+ char *__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 = src;
+ __gen_e_acsl_at_2 = dest;
+ __gen_e_acsl_at_3 = src;
__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_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
index a7441e7b6a81ce5051ab1e0986b7a939cb251c96..74ca57c74855673e01f41a3142e5f0b8b72391c0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
@@ -162,12 +162,16 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
char * restrict resolved_name)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at_3;
+ char *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
{
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& resolved_name),8UL);
__gen_e_acsl_at = resolved_name;
+ __gen_e_acsl_at_2 = resolved_name;
+ __gen_e_acsl_at_3 = resolved_name;
__gen_e_acsl_contract = __e_acsl_contract_init(5UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
index 9144b3f24622922ec31f020dcc41bea85eccf996..a5755ea9452cd88a117645f197d4841d7d3c10e3 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
@@ -67,6 +67,7 @@ int main(void)
struct list *__gen_e_acsl_f(struct list *l)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ struct list *__gen_e_acsl_at_2;
struct list *__gen_e_acsl_at;
struct list *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
@@ -75,6 +76,7 @@ struct list *__gen_e_acsl_f(struct list *l)
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& l),8UL);
__gen_e_acsl_at = l;
+ __gen_e_acsl_at_2 = l;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL,
l == (struct list *)0);
@@ -132,7 +134,7 @@ struct list *__gen_e_acsl_f(struct list *l)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"\\result",
(void *)__retres);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"\\old(l)",
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at_2);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Postcondition";
__gen_e_acsl_assert_data_2.pred_txt = "\\result == \\old(l)";
@@ -140,7 +142,7 @@ struct list *__gen_e_acsl_f(struct list *l)
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 15;
__gen_e_acsl_assert_data_2.name = "B1";
- __e_acsl_assert(__retres == __gen_e_acsl_at,
+ __e_acsl_assert(__retres == __gen_e_acsl_at_2,
& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
index 37f8bf4b80130d318c5bc4c330c21b1b1ed6b1b6..88e6322dd66a98fd9333240ccfba691fe0ae4f71 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
@@ -162,6 +162,8 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
char * restrict resolved_name)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at_3;
+ char *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
@@ -170,6 +172,8 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__e_acsl_store_block((void *)(& resolved_name),8UL);
__e_acsl_temporal_pull_parameter((void *)(& resolved_name),1U,8UL);
__gen_e_acsl_at = resolved_name;
+ __gen_e_acsl_at_2 = resolved_name;
+ __gen_e_acsl_at_3 = resolved_name;
__gen_e_acsl_contract = __e_acsl_contract_init(5UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};