From 20643ef668247d16ea3f12807bde63414a35bce4 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Mon, 23 Sep 2024 16:46:59 +0200
Subject: [PATCH] [e-acsl] undefine comparison for derivatives of Misc.Id_term
Make Pred_or_term depend on Misc.Term_id instead of Cil_datatype.Term.
This should have been the case all along, since Pred_or_term is used in
contexts where the physical identity of terms matter. They might be
typed differently depending on contexts (cast or no cast) and thus
require different translations.
Then we undefine the comparison function for both modules which depend
on Misc.Id_term, since there is no meaningful comparison for physical
equality.
---
.../e-acsl/src/libraries/analyses_datatype.ml | 73 +++---
.../src/libraries/analyses_datatype.mli | 4 +
.../e-acsl/tests/arith/oracle/at.res.oracle | 6 +
.../tests/arith/oracle/functions.res.oracle | 4 +
.../e-acsl/tests/arith/oracle/gen_at.c | 223 +++++++++++-------
.../e-acsl/tests/arith/oracle/gen_functions.c | 122 ++++++++++
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 51 ++--
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 76 +++---
.../e-acsl/tests/bts/oracle/gen_bts2252.c | 27 ++-
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 7 +-
.../e-acsl/tests/builtin/oracle/gen_strcmp.c | 7 +-
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 7 +-
.../e-acsl/tests/builtin/oracle/gen_strlen.c | 7 +-
.../constructs/oracle/gen_function_contract.c | 24 +-
.../tests/constructs/oracle/gen_result.c | 14 +-
.../tests/constructs/oracle/result.res.oracle | 4 +-
.../e-acsl/tests/format/oracle/gen_fprintf.c | 7 +-
.../e-acsl/tests/libc/oracle/gen_str.c | 48 ++--
.../tests/memory/oracle/gen_hidden_malloc.c | 4 +
.../memory/oracle/gen_valid_in_contract.c | 6 +-
.../tests/temporal/oracle/gen_t_fun_lib.c | 4 +
21 files changed, 480 insertions(+), 245 deletions(-)
diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
index e3d1f599319..d6a548d80f8 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 444219dfc2f..59849829d9a 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 422529ed413..c1c0d8c8094 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 b45b4d727ce..dcb1f8a7a95 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 6c066086426..f869913749c 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 9f9358add8a..490dff8e59b 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 e85da85a4b1..f67fbe8bd18 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 8e484ee47ec..e0bb405377c 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 e6397626eec..6e05c2f6131 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 a235f02b21d..f92bbb706d3 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 22c523cc0e4..34b223989b6 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 08a859cae38..12582f8bbbc 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 72856675c72..1ec8397bd9c 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 3b8e64f41ac..373c5d7a30c 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 0fdf520c053..578c1350215 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 8b89a531d8c..c154bf096dd 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 ed7d5351a40..d9fae2605f6 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 e41ebd61ec3..6076da28258 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 a7441e7b6a8..74ca57c7485 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 9144b3f2462..a5755ea9452 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 37f8bf4b801..88e6322dd66 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};
--
GitLab