diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index f5f780dd7d02bf57a3c44434d4fb7f2e60cd61f2..ab6ca4885ad499bb3af93b8159fdb54860fc428d 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,9 @@
Plugin E-ACSL <next-release>
###############################################################################
+-* E-ACSL [2024-09-26] fix usage of structural equality of terms;
+ By using physical equality we ensure that structurally
+ identical terms are translated according to their context.
-* E-ACSL [2024-09-16] fix logic variable escaping its scope
-* E-ACSL [2024-09-03] handle negative integers generated by RTE
- E-ACSL [2024-09-03] add support for labelled logic functions in case
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index ad5a3600c9e441c2ed9675ef887191f9c8bff5ba..05320831cb2ba5cfce57e5d7559654b5e8cb92b2 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -217,7 +217,7 @@ let replace_all_args_ival li args_ival =
List.iter
(fun x ->
let i = Logic_var.Map.find x args_ival in
- (Misc.Id_term.Map.iter
+ (Misc.Id_term.Hashtbl.iter
(fun t profile -> Memo.replace profile t i)
(Logic_var.Map.find x args_map)))
li.l_profile
diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml
index afca5076f37a87bf7ff513a5d848aa0fb1a751b5..9fc9626a8429ee408b64305c23afcdcba6483389 100644
--- a/src/plugins/e-acsl/src/analyses/labels.ml
+++ b/src/plugins/e-acsl/src/analyses/labels.ml
@@ -58,34 +58,36 @@ let preprocess_done = ref false
(** Associate a statement with the [at_data] that need to be translated on
this statement. *)
-let at_data_for_stmts: At_data.Set.t ref Stmt.Hashtbl.t =
+let at_data_for_stmts: At_data.t list ref Stmt.Hashtbl.t =
Stmt.Hashtbl.create 17
(** Add [data] to the list of [at_data] that must be translated on the
statement [stmt]. *)
let add_at_for_stmt data stmt =
let stmt = get_first_inner_stmt stmt in
+ (* Note that the error field is not taken into account in At_data.equal.
+ Therefore we cannot just write:
+ At_data.Hashtbl.replace ats_tbl data data; let old_data = data in *)
let ats_ref =
try
Stmt.Hashtbl.find at_data_for_stmts stmt
with Not_found ->
- let ats_ref = ref At_data.Set.empty in
+ let ats_ref = ref [] in
Stmt.Hashtbl.add at_data_for_stmts stmt ats_ref;
ats_ref
in
let old_data =
try
- At_data.Set.find data !ats_ref
+ List.find (At_data.equal data) !ats_ref
with Not_found ->
- ats_ref := At_data.Set.add data !ats_ref;
+ ats_ref := data :: !ats_ref;
data
in
match old_data.error, data.error with
| Some _, None ->
(* Replace the old data that has an error with the new data that do not
have one. *)
- ats_ref := At_data.Set.remove old_data !ats_ref;
- ats_ref := At_data.Set.add data !ats_ref
+ ats_ref := data :: List.filter (fun d -> not @@ At_data.equal d old_data) !ats_ref;
| Some _, Some _
| None, Some _
| None, None ->
@@ -97,7 +99,7 @@ let add_at_for_stmt data stmt =
let at_for_stmt stmt =
if !preprocess_done then
let ats_ref =
- Stmt.Hashtbl.find_def at_data_for_stmts stmt (ref At_data.Set.empty)
+ Stmt.Hashtbl.find_def at_data_for_stmts stmt (ref [])
in
Result.Ok !ats_ref
else
@@ -558,7 +560,7 @@ let _debug () =
Options.feedback ~level:2 "| - stmt %d at %a"
stmt.sid
Printer.pp_location (Stmt.loc stmt);
- At_data.Set.iter
+ List.iter
(fun at ->
Options.feedback ~level:2 "| - at %a"
At_data.pretty at)
diff --git a/src/plugins/e-acsl/src/analyses/labels.mli b/src/plugins/e-acsl/src/analyses/labels.mli
index 1c9a7951d7f6ec09658a45ceaf76108306983fc9..40627c15b5d5991bba11f4e1cee35a1d88ed5da5 100644
--- a/src/plugins/e-acsl/src/analyses/labels.mli
+++ b/src/plugins/e-acsl/src/analyses/labels.mli
@@ -35,7 +35,7 @@ val get_first_inner_stmt: stmt -> stmt
(** If the given statement has a label, return the first statement of the block.
Otherwise return the given statement. *)
-val at_for_stmt: stmt -> At_data.Set.t Error.result
+val at_for_stmt: stmt -> At_data.t list Error.result
(** @return the set of labeled predicates and terms to be translated on the
given statement.
@raise Not_memoized if the labels pre-analysis was not run. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 58c424efd6d6a3b5344bade03cf8978db2faec40..1b26cd2d50308a6055e3f3eb4bfb914872a423fb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -484,8 +484,8 @@ let for_stmt env kf stmt =
(* Translate the [\at()]. *)
let stmt_translations = Pred_or_term.Hashtbl.create 7 in
- At_data.Set.fold
- (fun ({ lscope; pot; error } as at_data) env ->
+ List.fold_left
+ (fun env ({ lscope; pot; error } as at_data) ->
let open Current_loc.Operators in
let<> UpdatedCurrentLoc = match pot with
| PoT_pred p -> p.pred_loc
@@ -519,8 +519,8 @@ let for_stmt env kf stmt =
Pred_or_term.Hashtbl.replace stmt_translations pot vi_or_err;
At_data.Hashtbl.replace translations at_data vi_or_err;
env)
- at_for_stmt
env
+ at_for_stmt
let to_exp ~loc ~adata kf env pot label =
let kinstr = Env.get_kinstr env in
diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
index e3d1f599319d187431b2c7d54111caab3242d2b2..2385a3bc6e6951d791b70cc817022f03846bd07e 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
@@ -483,9 +464,12 @@ module LF_env
Logic_var.Map.update
lv
(fun m -> match m with
- | Some m ->
- Some (Misc.Id_term.Map.update t (fun _ -> Some profile) m)
- | None -> Some (Misc.Id_term.Map.(add t profile empty)))
+ | Some tbl ->
+ Misc.Id_term.Hashtbl.replace tbl t profile; Some tbl
+ | None ->
+ let tbl = Misc.Id_term.Hashtbl.create 9 in
+ Misc.Id_term.Hashtbl.add tbl t profile;
+ Some tbl)
map)
map
li.l_profile
diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
index 444219dfc2f390c8d5bc874b373e4577df1100ec..5720f1a3f3ff29bdce6ce6a1b12fa79b97d782a6 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
@@ -134,7 +138,7 @@ module LF_env : sig
(** find all the arguments a recursive function or predicate has been
called with*)
- val find_args : logic_info -> (Profile.t Misc.Id_term.Map.t) Logic_var.Map.t
+ val find_args : logic_info -> Profile.t Misc.Id_term.Hashtbl.t Logic_var.Map.t
(** clear the table of intervals for logic function *)
val clear : unit -> unit
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 839b26676fdf56b33b4c4b0fd58f62755f2e762a..e1ea93a8e4b694429e13b6f8980df08e7b9b5e1a 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -217,8 +217,9 @@ module Id_term =
(struct
include Cil_datatype.Term
let name = "E_ACSL.Id_term"
- let compare (t1:term) t2 =
- if t1 == t2 then 0 else Cil_datatype.Term.compare t1 t2
+ let compare _ _ =
+ (* There is no sound comparison based on physical identity. *)
+ Kernel.fatal "Id_term: comparison undefined (and undefinable)"
let equal (t1:term) t2 = t1 == t2
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 16706184a7f1a478815d49234773f5ae1defedc2..b1bff7698f6d4a770e6b006247363b17e599d369 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -82,7 +82,10 @@ val finite_min_and_max: Ival.t -> Integer.t * Integer.t
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds. *)
module Id_term: Datatype.S_with_collections with type t = term
-(** Datatype for terms that relies on physical equality. *)
+(** Datatype for terms that relies on physical equality.
+ Note that of its collections only [Hashtbl] can be used.
+ Using [Map] and [Set] raises a fatal error as they require a comparison
+ function, which cannot be defined in a sound way for physical equality. *)
val extract_uncoerced_lval: exp -> exp option
(** Unroll the [CastE] part of the expression until an [Lval] is found, and
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index b02c5f9baca3095a13b63ba8a8e5c4bce77fbca5..66e0968c07197d14c9890358bdb3ca41895ed664 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -111,3 +111,16 @@ int main(void) {
void test_f4() {
/*@ assert f4 (0) ≡ 0; */
}
+
+// same term \at(j, Old) twice in different typing contexts
+/*@
+ behavior a:
+ ensures 1 == -j;
+ behavior b:
+ ensures 2 == j;
+ */
+int f5(long int j) {}
+
+int test_f5() {
+ f5(1);
+}
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..b9b1b2d81696756053d10fba479a8bb46283e583 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 = __gen_e_acsl_at_2;
+ __gen_e_acsl_at_5 = A;
A = 2;
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__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_5);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "\\at(A,F) == 1";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 17;
- __e_acsl_assert(__gen_e_acsl_at_2 == 1,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_at_5 == 1,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \at(A,F) == 1; */ ;
@@ -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_4);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Assertion";
__gen_e_acsl_assert_data_4.pred_txt = "\\at(\\at(A,Pre),F) == 0";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "f";
__gen_e_acsl_assert_data_4.line = 19;
- __e_acsl_assert(__gen_e_acsl_at_3 == 0,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_at_4 == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \at(\at(A,Pre),F) == 0; */ ;
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)
{
+ int __gen_e_acsl_at_3;
long __gen_e_acsl_at_2;
- int __gen_e_acsl_at;
+ 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 = (long)x;
__gen_e_acsl_at_2 = x + 1L;
+ __gen_e_acsl_at_3 = x;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"x",0,x);
__gen_e_acsl_assert_data.blocking = 1;
@@ -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_3);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "\\at(x,L) == 0";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 77;
- __e_acsl_assert(__gen_e_acsl_at == 0,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_at_3 == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \at(x,L) == 0; */ ;
@@ -426,16 +471,15 @@ int main(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(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_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index 54abb67f00134052a63240bbff4b4cf8de25563b..3850002297e31c2857172366f0c352b776b1589b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -105,19 +105,19 @@ int main(void)
int *__gen_e_acsl_at_7;
long *__gen_e_acsl_at_6;
int *__gen_e_acsl_at_5;
+ int *__gen_e_acsl_at_4;
int *__gen_e_acsl_at_3;
long *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
int __retres;
int n;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__gen_e_acsl_at_8 = (long *)malloc(64UL);
- __gen_e_acsl_at_7 = (int *)malloc(12000UL);
+ __gen_e_acsl_at_7 = (int *)malloc(528UL);
__gen_e_acsl_at_6 = (long *)malloc(2496UL);
- __gen_e_acsl_at_5 = (int *)malloc(528UL);
+ __gen_e_acsl_at_5 = (int *)malloc(12000UL);
+ __gen_e_acsl_at_4 = (int *)malloc(4UL);
__gen_e_acsl_at_3 = (int *)malloc(12UL);
__gen_e_acsl_at_2 = (long *)malloc(8UL);
- __gen_e_acsl_at = (int *)malloc(4UL);
__e_acsl_store_block((void *)(& n),4UL);
__e_acsl_full_init((void *)(& n));
n = 7;
@@ -125,12 +125,7 @@ int main(void)
{
int __gen_e_acsl_i;
__gen_e_acsl_i = 3;
- *(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i == 10L;
- }
- {
- int __gen_e_acsl_i_2;
- __gen_e_acsl_i_2 = 3;
- *(__gen_e_acsl_at_2 + 0) = n + (long)__gen_e_acsl_i_2;
+ *(__gen_e_acsl_at_2 + 0) = n + (long)__gen_e_acsl_i;
}
{
int __gen_e_acsl_j;
@@ -141,27 +136,40 @@ int main(void)
__gen_e_acsl_j ++;
}
}
+ {
+ int __gen_e_acsl_i_2;
+ __gen_e_acsl_i_2 = 3;
+ *(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_2 == 10L;
+ }
;
__e_acsl_full_init((void *)(& n));
n = 9;
K:
{
- int __gen_e_acsl_k;
int __gen_e_acsl_u;
int __gen_e_acsl_v;
- __gen_e_acsl_k = -7;
- __gen_e_acsl_u = 9;
+ int __gen_e_acsl_w;
+ __gen_e_acsl_u = 10;
while (1) {
- if (__gen_e_acsl_u < 21) ; else break;
- __gen_e_acsl_v = -5 + 1;
+ if (__gen_e_acsl_u < 20) ; else break;
+ __gen_e_acsl_v = -10 + 1;
while (1) {
- if (__gen_e_acsl_v <= 6) ; else break;
{
- long __gen_e_acsl_if;
- if (__gen_e_acsl_u > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k;
- else __gen_e_acsl_if = __gen_e_acsl_u + __gen_e_acsl_v;
- *(__gen_e_acsl_at_5 + ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4))) =
- __gen_e_acsl_if > 0L;
+ int __gen_e_acsl_u_3;
+ __gen_e_acsl_u_3 = -2;
+ if (__gen_e_acsl_v <= -5 + __gen_e_acsl_u_3) ; else break;
+ }
+ __gen_e_acsl_w = 100 + 1;
+ while (1) {
+ if (__gen_e_acsl_w <= 200) ; else break;
+ {
+ int __gen_e_acsl_u_2;
+ __gen_e_acsl_u_2 = 42;
+ *(__gen_e_acsl_at_5 + ((__gen_e_acsl_u - 10) * 300 + ((__gen_e_acsl_v - -9) * 100 + (
+ __gen_e_acsl_w - 101)))) =
+ (((n - (long)__gen_e_acsl_u) + __gen_e_acsl_u_2) + __gen_e_acsl_v) + __gen_e_acsl_w > 0L;
+ }
+ __gen_e_acsl_w ++;
}
__gen_e_acsl_v ++;
}
@@ -169,56 +177,47 @@ int main(void)
}
}
{
- int __gen_e_acsl_u_2;
+ int __gen_e_acsl_u_4;
int __gen_e_acsl_v_2;
- __gen_e_acsl_u_2 = 9;
+ __gen_e_acsl_u_4 = 9;
while (1) {
- if (__gen_e_acsl_u_2 < 21) ; else break;
+ if (__gen_e_acsl_u_4 < 21) ; else break;
__gen_e_acsl_v_2 = -5 + 1;
while (1) {
{
- int __gen_e_acsl_if_2;
- if (__gen_e_acsl_u_2 < 15) __gen_e_acsl_if_2 = __gen_e_acsl_u_2 + 6;
- else __gen_e_acsl_if_2 = 3;
- if (__gen_e_acsl_v_2 <= __gen_e_acsl_if_2) ; else break;
+ int __gen_e_acsl_if;
+ if (__gen_e_acsl_u_4 < 15) __gen_e_acsl_if = __gen_e_acsl_u_4 + 6;
+ else __gen_e_acsl_if = 3;
+ if (__gen_e_acsl_v_2 <= __gen_e_acsl_if) ; else break;
}
- *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 26 + (__gen_e_acsl_v_2 - -4))) =
- (n + (long)__gen_e_acsl_u_2) + __gen_e_acsl_v_2;
+ *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 26 + (__gen_e_acsl_v_2 - -4))) =
+ (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_2;
__gen_e_acsl_v_2 ++;
}
- __gen_e_acsl_u_2 ++;
+ __gen_e_acsl_u_4 ++;
}
}
{
- int __gen_e_acsl_u_3;
+ int __gen_e_acsl_k;
+ int __gen_e_acsl_u_5;
int __gen_e_acsl_v_3;
- int __gen_e_acsl_w;
- __gen_e_acsl_u_3 = 10;
+ __gen_e_acsl_k = -7;
+ __gen_e_acsl_u_5 = 9;
while (1) {
- if (__gen_e_acsl_u_3 < 20) ; else break;
- __gen_e_acsl_v_3 = -10 + 1;
+ if (__gen_e_acsl_u_5 < 21) ; else break;
+ __gen_e_acsl_v_3 = -5 + 1;
while (1) {
+ if (__gen_e_acsl_v_3 <= 6) ; else break;
{
- int __gen_e_acsl_u_5;
- __gen_e_acsl_u_5 = -2;
- if (__gen_e_acsl_v_3 <= -5 + __gen_e_acsl_u_5) ; else break;
- }
- __gen_e_acsl_w = 100 + 1;
- while (1) {
- if (__gen_e_acsl_w <= 200) ; else break;
- {
- int __gen_e_acsl_u_4;
- __gen_e_acsl_u_4 = 42;
- *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_3 - 10) * 300 + ((
- __gen_e_acsl_v_3 - -9) * 100 + (
- __gen_e_acsl_w - 101)))) =
- (((n - (long)__gen_e_acsl_u_3) + __gen_e_acsl_u_4) + __gen_e_acsl_v_3) + __gen_e_acsl_w > 0L;
- }
- __gen_e_acsl_w ++;
+ long __gen_e_acsl_if_2;
+ if (__gen_e_acsl_u_5 > 0) __gen_e_acsl_if_2 = n + (long)__gen_e_acsl_k;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_u_5 + __gen_e_acsl_v_3;
+ *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 9) * 11 + (__gen_e_acsl_v_3 - -4))) =
+ __gen_e_acsl_if_2 > 0L;
}
__gen_e_acsl_v_3 ++;
}
- __gen_e_acsl_u_3 ++;
+ __gen_e_acsl_u_5 ++;
}
}
;
@@ -231,20 +230,21 @@ int main(void)
__gen_e_acsl_i_3 = 3;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"\\at(n + i == 10,L)",0,
- *(__gen_e_acsl_at + 0));
+ *(__gen_e_acsl_at_4 + 0));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_4",
+ (void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__gen_e_acsl_at_4 + 0)";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 28;
@@ -257,7 +257,7 @@ int main(void)
__gen_e_acsl_assert_data.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 28;
- __e_acsl_assert(*(__gen_e_acsl_at + 0),& __gen_e_acsl_assert_data);
+ __e_acsl_assert(*(__gen_e_acsl_at_4 + 0),& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
/*@ assert \let i = 3; \at(n + i == 10,L); */ ;
@@ -341,17 +341,17 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(
- __gen_e_acsl_at_5 + (int)(
+ __gen_e_acsl_at_7 + (int)(
(long)((int)(
(long)((int)(
__gen_e_acsl_u_6 - 9L)) * 11L)) + (int)(
__gen_e_acsl_v_4 - -4L))),
sizeof(int),
- (void *)__gen_e_acsl_at_5,
- (void *)(& __gen_e_acsl_at_5));
+ (void *)__gen_e_acsl_at_7,
+ (void *)(& __gen_e_acsl_at_7));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_at_5",
- (void *)__gen_e_acsl_at_5);
+ "__gen_e_acsl_at_7",
+ (void *)__gen_e_acsl_at_7);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
"__gen_e_acsl_u_6",0,
__gen_e_acsl_u_6);
@@ -362,7 +362,7 @@ int main(void)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_5 +\n (int)((int)((int)(__gen_e_acsl_u_6 - 9) * 11) +\n (int)(__gen_e_acsl_v_4 - -4)))";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_6 - 9) * 11) +\n (int)(__gen_e_acsl_v_4 - -4)))";
__gen_e_acsl_assert_data_6.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 34;
@@ -370,7 +370,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_3,
& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- if (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_u_6 - 9) * 11 + (
+ if (*(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_6 - 9) * 11 + (
__gen_e_acsl_v_4 - -4)))) ;
else {
__gen_e_acsl_forall = 0;
@@ -656,7 +656,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_14 =
{.values = (void *)0};
__gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(
- __gen_e_acsl_at_7 + (int)(
+ __gen_e_acsl_at_5 + (int)(
(long)((int)(
(long)((int)(
__gen_e_acsl_u_8 - 10L)) * 300L)) + (int)(
@@ -665,11 +665,11 @@ int main(void)
__gen_e_acsl_v_6 - -9L)) * 100L)) + (int)(
__gen_e_acsl_w_2 - 101L)))),
sizeof(int),
- (void *)__gen_e_acsl_at_7,
- (void *)(& __gen_e_acsl_at_7));
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_14,
- "__gen_e_acsl_at_7",
- (void *)__gen_e_acsl_at_7);
+ "__gen_e_acsl_at_5",
+ (void *)__gen_e_acsl_at_5);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,
"__gen_e_acsl_u_8",0,
__gen_e_acsl_u_8);
@@ -683,7 +683,7 @@ int main(void)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_14.blocking = 1;
__gen_e_acsl_assert_data_14.kind = "RTE";
- __gen_e_acsl_assert_data_14.pred_txt = "\\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_8 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_6 - -9) * 100) +\n (int)(__gen_e_acsl_w_2 - 101))))";
+ __gen_e_acsl_assert_data_14.pred_txt = "\\valid_read(__gen_e_acsl_at_5 +\n (int)((int)((int)(__gen_e_acsl_u_8 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_6 - -9) * 100) +\n (int)(__gen_e_acsl_w_2 - 101))))";
__gen_e_acsl_assert_data_14.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_14.fct = "main";
__gen_e_acsl_assert_data_14.line = 59;
@@ -691,7 +691,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_7,
& __gen_e_acsl_assert_data_14);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
- if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_8 - 10) * 300 + (
+ if (! *(__gen_e_acsl_at_5 + ((__gen_e_acsl_u_8 - 10) * 300 + (
(__gen_e_acsl_v_6 - -9) * 100 + (
__gen_e_acsl_w_2 - 101)))))
;
@@ -751,9 +751,9 @@ int main(void)
__retres = 0;
__e_acsl_delete_block((void *)(t));
__e_acsl_delete_block((void *)(& n));
- free((void *)__gen_e_acsl_at);
free((void *)__gen_e_acsl_at_2);
free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_4);
free((void *)__gen_e_acsl_at_5);
free((void *)__gen_e_acsl_at_6);
free((void *)__gen_e_acsl_at_7);
@@ -785,7 +785,8 @@ void __gen_e_acsl_f(int *t)
int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (int)(
+ __gen_e_acsl_m - 4L)),
sizeof(int),(void *)t,
(void *)(& t));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"t",(void *)t);
@@ -795,14 +796,14 @@ void __gen_e_acsl_f(int *t)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "\\valid_read(t + __gen_e_acsl_m)";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid_read(t + (int)(__gen_e_acsl_m - 4))";
__gen_e_acsl_assert_data.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 8;
__gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- *(__gen_e_acsl_at + 0) = *(t + __gen_e_acsl_m) == -4;
+ *(__gen_e_acsl_at + 0) = *(t + (__gen_e_acsl_m - 4));
}
}
{
@@ -812,8 +813,7 @@ void __gen_e_acsl_f(int *t)
int __gen_e_acsl_valid_read_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (int)(
- __gen_e_acsl_m_2 - 4L)),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m_2),
sizeof(int),(void *)t,
(void *)(& t));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"t",
@@ -824,14 +824,14 @@ void __gen_e_acsl_f(int *t)
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(t + (int)(__gen_e_acsl_m_2 - 4))";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(t + __gen_e_acsl_m_2)";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 8;
__gen_e_acsl_assert_data_2.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- *(__gen_e_acsl_at_2 + 0) = *(t + (__gen_e_acsl_m_2 - 4));
+ *(__gen_e_acsl_at_2 + 0) = *(t + __gen_e_acsl_m_2) == -4;
}
}
{
@@ -997,17 +997,18 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_m_3 = 4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + 0),
sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_9,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "RTE";
- __gen_e_acsl_assert_data_9.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
+ __gen_e_acsl_assert_data_9.pred_txt = "\\valid_read(__gen_e_acsl_at_2 + 0)";
__gen_e_acsl_assert_data_9.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_9.fct = "f";
__gen_e_acsl_assert_data_9.line = 8;
@@ -1016,23 +1017,22 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
"\\old(*(t + m) == -4)",0,
- *(__gen_e_acsl_at + 0));
- if (*(__gen_e_acsl_at + 0)) {
+ *(__gen_e_acsl_at_2 + 0));
+ if (*(__gen_e_acsl_at_2 + 0)) {
int __gen_e_acsl_valid_read_8;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + 0),
+ __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
sizeof(int),
- (void *)__gen_e_acsl_at_2,
- (void *)(& __gen_e_acsl_at_2));
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_10,
- "__gen_e_acsl_at_2",
- (void *)__gen_e_acsl_at_2);
+ "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_10,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_assert_data_10.blocking = 1;
__gen_e_acsl_assert_data_10.kind = "RTE";
- __gen_e_acsl_assert_data_10.pred_txt = "\\valid_read(__gen_e_acsl_at_2 + 0)";
+ __gen_e_acsl_assert_data_10.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
__gen_e_acsl_assert_data_10.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_10.fct = "f";
__gen_e_acsl_assert_data_10.line = 8;
@@ -1042,8 +1042,8 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
"\\old(*(t + (m - 4)))",0,
- *(__gen_e_acsl_at_2 + 0));
- __gen_e_acsl_and_2 = *(__gen_e_acsl_at_2 + 0) == 9;
+ *(__gen_e_acsl_at + 0));
+ __gen_e_acsl_and_2 = *(__gen_e_acsl_at + 0) == 9;
}
else __gen_e_acsl_and_2 = 0;
__gen_e_acsl_assert_data_8.blocking = 1;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_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/arith/oracle/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
index 40e395ec27c766a1c5613115a1828868132a118b..b301bf239fc22186aeaf8dc676523e050afb0f7e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
@@ -356,19 +356,19 @@ double __gen_e_acsl_avg(double a, double b)
__e_acsl_mpq_t __gen_e_acsl_at;
double __retres;
{
- __e_acsl_mpq_t __gen_e_acsl_a;
__e_acsl_mpq_t __gen_e_acsl_b;
- __gmpq_init(__gen_e_acsl_a);
- __gmpq_set_d(__gen_e_acsl_a,a);
- __gmpq_init(__gen_e_acsl_at);
- __gmpq_set(__gen_e_acsl_at,(__e_acsl_mpq_struct const *)(__gen_e_acsl_a));
+ __e_acsl_mpq_t __gen_e_acsl_a;
__gmpq_init(__gen_e_acsl_b);
__gmpq_set_d(__gen_e_acsl_b,b);
+ __gmpq_init(__gen_e_acsl_at);
+ __gmpq_set(__gen_e_acsl_at,(__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
+ __gmpq_init(__gen_e_acsl_a);
+ __gmpq_set_d(__gen_e_acsl_a,a);
__gmpq_init(__gen_e_acsl_at_2);
__gmpq_set(__gen_e_acsl_at_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
- __gmpq_clear(__gen_e_acsl_a);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_a));
__gmpq_clear(__gen_e_acsl_b);
+ __gmpq_clear(__gen_e_acsl_a);
}
__retres = avg(a,b);
{
@@ -386,8 +386,8 @@ double __gen_e_acsl_avg(double a, double b)
__gen_e_acsl_delta = 1;
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_at));
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"2",10);
__gmpq_init(__gen_e_acsl_div);
@@ -441,9 +441,9 @@ double __gen_e_acsl_avg(double a, double b)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"\\old(a)",
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at));
- __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"\\old(b)",
(__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2));
+ __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"\\old(b)",
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_at));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Postcondition";
__gen_e_acsl_assert_data.pred_txt = "\\let delta = 1;\n\\let avg_real = (\\old(a) + \\old(b)) / 2;\n avg_real - delta < \\result < avg_real + delta";
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index e85da85a4b1381606d700317bcae52f1e401da71..ba7fd848e53192e39a03df7416f9a3aad97b81f2 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;
@@ -106,9 +109,12 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_store_block((void *)(& Mtmin_out),8UL);
__e_acsl_store_block((void *)(& Mwmin),8UL);
__e_acsl_store_block((void *)(& Mtmin_in),8UL);
- __gen_e_acsl_at = Mtmin_in;
- __gen_e_acsl_at_2 = Mwmin;
- __gen_e_acsl_at_3 = Mtmin_out;
+ __gen_e_acsl_at = Mwmin;
+ __gen_e_acsl_at_2 = Mtmin_in;
+ __gen_e_acsl_at_3 = Mwmin;
+ __gen_e_acsl_at_4 = Mtmin_in;
+ __gen_e_acsl_at_5 = Mtmin_in;
+ __gen_e_acsl_at_6 = Mtmin_out;
__gen_e_acsl_contract = __e_acsl_contract_init(1UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__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_5,
sizeof(float),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_5",
+ (void *)__gen_e_acsl_at_5);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
"sizeof(float)",0,sizeof(float));
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "RTE";
- __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(__gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(__gen_e_acsl_at_5)";
__gen_e_acsl_assert_data_5.file = "bts1307.i";
__gen_e_acsl_assert_data_5.fct = "bar";
__gen_e_acsl_assert_data_5.line = 26;
@@ -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_5) {
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl__3;
__e_acsl_mpq_t __gen_e_acsl_mul;
int __gen_e_acsl_lt;
__gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at);
+ __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at_4);
__gmpq_init(__gen_e_acsl__2);
__gmpq_set_str(__gen_e_acsl__2,"085/100",10);
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_2);
+ __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
@@ -247,18 +254,18 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid_read_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
sizeof(float),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,
- "__gen_e_acsl_at",
- (void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,
"sizeof(float)",0,sizeof(float));
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at_2)";
__gen_e_acsl_assert_data_7.file = "bts1307.i";
__gen_e_acsl_assert_data_7.fct = "bar";
__gen_e_acsl_assert_data_7.line = 26;
@@ -267,8 +274,8 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at);
- __gen_e_acsl_if = (double)*__gen_e_acsl_at != 0.;
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at_2);
+ __gen_e_acsl_if = (double)*__gen_e_acsl_at_2 != 0.;
}
else {
__e_acsl_mpq_t __gen_e_acsl__4;
@@ -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);
__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);
__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_5);
__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_4);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmin)",*__gen_e_acsl_at_2);
+ "*\\old(Mwmin)",*__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Postcondition";
__gen_e_acsl_assert_data_4.pred_txt = "*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85 * *\\old(Mwmin) != 0.";
@@ -345,8 +352,8 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_store_block((void *)(& Mtmax_out),8UL);
__e_acsl_store_block((void *)(& Mwmax),8UL);
__e_acsl_store_block((void *)(& Mtmax_in),8UL);
- __gen_e_acsl_at = Mtmax_in;
- __gen_e_acsl_at_2 = Mwmax;
+ __gen_e_acsl_at = Mwmax;
+ __gen_e_acsl_at_2 = Mtmax_in;
__gen_e_acsl_at_3 = Mtmax_out;
__gen_e_acsl_contract = __e_acsl_contract_init(1UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
@@ -430,7 +437,7 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gmpq_init(__gen_e_acsl_);
__gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at_3);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at);
+ __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl__3);
__gmpq_set_str(__gen_e_acsl__3,"5",10);
__gmpq_init(__gen_e_acsl__4);
@@ -442,7 +449,7 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gmpq_init(__gen_e_acsl__6);
- __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_2);
+ __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div),
@@ -466,9 +473,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
"*\\old(Mtmax_out)",*__gen_e_acsl_at_3);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmax_in)",*__gen_e_acsl_at);
+ "*\\old(Mtmax_in)",*__gen_e_acsl_at_2);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmax)",*__gen_e_acsl_at_2);
+ "*\\old(Mwmax)",*__gen_e_acsl_at);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Postcondition";
__gen_e_acsl_assert_data_4.pred_txt = "*\\old(Mtmax_out) != *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)";
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_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_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 73c880a96c69d88ef21b70357a687cf4a8799d7a..27cb9dd93446728ef196bf56a59425b8462883f0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -71,8 +71,8 @@ void *memchr(void const *buf, int c, size_t n)
void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- int __gen_e_acsl_at_2;
- void const *__gen_e_acsl_at;
+ void const *__gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
void *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
{
@@ -81,8 +81,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall;
int __gen_e_acsl_k;
__e_acsl_store_block((void *)(& buf),8UL);
- __gen_e_acsl_at = buf;
- __gen_e_acsl_at_2 = c;
+ __gen_e_acsl_at = c;
+ __gen_e_acsl_at_2 = buf;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__gen_e_acsl_exists = 0;
__gen_e_acsl_i = 0;
@@ -186,20 +186,20 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_valid_read_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at + __gen_e_acsl_j),
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j),
sizeof(char),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
- "__gen_e_acsl_at",
- (void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_uint(& __gen_e_acsl_assert_data_4,
"__gen_e_acsl_j",0,__gen_e_acsl_j);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(char)",0,sizeof(char));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read((char *)__gen_e_acsl_at + __gen_e_acsl_j)";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j)";
__gen_e_acsl_assert_data_4.file = "bts1390.c";
__gen_e_acsl_assert_data_4.fct = "memchr";
__gen_e_acsl_assert_data_4.line = 9;
@@ -207,7 +207,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_3,
& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
- if ((int)*((char *)__gen_e_acsl_at + __gen_e_acsl_j) != __gen_e_acsl_at_2)
+ if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at)
;
else {
__gen_e_acsl_forall_2 = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index e6397626eec5ed493b37b2127175735ac0c77c8c..ed9c13bf241340f6e7447a8d8d28dede54037e03 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -54,9 +54,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at_5;
+ char *__gen_e_acsl_at_4;
__e_acsl_mpz_t __gen_e_acsl_at_3;
- char const *__gen_e_acsl_at_2;
- char *__gen_e_acsl_at;
+ char *__gen_e_acsl_at_2;
+ char const *__gen_e_acsl_at;
char *__retres;
{
__e_acsl_mpz_t __gen_e_acsl_n;
@@ -87,11 +89,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
- __gen_e_acsl_at = dest;
- __gen_e_acsl_at_2 = src;
+ __gen_e_acsl_at = src;
+ __gen_e_acsl_at_2 = dest;
__gmpz_init_set_ui(__gen_e_acsl_n,n);
__gmpz_init_set(__gen_e_acsl_at_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gen_e_acsl_at_4 = dest;
+ __gen_e_acsl_at_5 = dest;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -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_5);
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "Postcondition";
__gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(dest)";
@@ -281,7 +285,8 @@ 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_5,
+ & __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
@@ -303,11 +308,11 @@ 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_4 +
1 * 0),
__gen_e_acsl_if_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
index 7c44d029d13b4a608006582414c005f68a03fe45..128027b11265ff5b5202c3073a1d642db6844789 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
@@ -38,12 +38,11 @@ int main(void)
/*@ ensures *\old(item) == \old(*item); */
void __gen_e_acsl_f(struct X *item)
{
- struct X __gen_e_acsl_at_2;
- struct X *__gen_e_acsl_at;
+ struct X *__gen_e_acsl_at_2;
+ struct X __gen_e_acsl_at;
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& item),8UL);
- __gen_e_acsl_at = item;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)item,
sizeof(struct X),
@@ -62,7 +61,8 @@ void __gen_e_acsl_f(struct X *item)
__gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- __gen_e_acsl_at_2 = *item;
+ __gen_e_acsl_at = *item;
+ __gen_e_acsl_at_2 = item;
}
f(item);
__e_acsl_delete_block((void *)(& item));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
index 3929c369e311404b5864331f7b2cd16d1fa41f72..da2c84457fbf645025b2ff3696bcd5fb4c6edda8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
@@ -63,8 +63,8 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
FILE * restrict stream)
{
size_t __gen_e_acsl_at_3;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- void *__gen_e_acsl_at;
+ void *__gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at;
size_t __retres;
{
__e_acsl_mpz_t __gen_e_acsl_size;
@@ -88,10 +88,10 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& stream),8UL);
__e_acsl_store_block((void *)(& ptr),8UL);
- __gen_e_acsl_at = ptr;
__gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_2 = ptr;
__gen_e_acsl_at_3 = nmemb;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
@@ -293,7 +293,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init(__gen_e_acsl_mul_4);
__gmpz_mul(__gen_e_acsl_mul_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
@@ -343,11 +343,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert(__gen_e_acsl_le_5 <= 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gen_e_acsl_size_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at_2 +
1 * 0),
__gen_e_acsl_size_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(ptr)",
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
@@ -356,7 +356,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__retres);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
@@ -390,7 +390,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_clear(__gen_e_acsl_mul_5);
__gmpz_clear(__gen_e_acsl_if_2);
__gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/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/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
index a89b03788ba4bdb0ffcb6a3e64e5b4e6825ffd5a..9f2896b4fee3591fe4dc47a6d3e5e44b764be591 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
@@ -61,8 +61,8 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
int __gen_e_acsl_at;
{
int __gen_e_acsl_assumes_value;
- __gen_e_acsl_at = b;
- __gen_e_acsl_at_2 = e;
+ __gen_e_acsl_at = e;
+ __gen_e_acsl_at_2 = b;
__gen_e_acsl_contract = __e_acsl_contract_init(1UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -334,25 +334,25 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_19 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_19,
- "__gen_e_acsl_at",0,__gen_e_acsl_at);
+ "__gen_e_acsl_at_2",0,__gen_e_acsl_at_2);
__gen_e_acsl_assert_data_19.blocking = 1;
__gen_e_acsl_assert_data_19.kind = "RTE";
- __gen_e_acsl_assert_data_19.pred_txt = "__gen_e_acsl_at != 0";
+ __gen_e_acsl_assert_data_19.pred_txt = "__gen_e_acsl_at_2 != 0";
__gen_e_acsl_assert_data_19.file = "rte.i";
__gen_e_acsl_assert_data_19.fct = "test";
__gen_e_acsl_assert_data_19.line = 8;
__gen_e_acsl_assert_data_19.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_at != 0,& __gen_e_acsl_assert_data_19);
+ __e_acsl_assert(__gen_e_acsl_at_2 != 0,& __gen_e_acsl_assert_data_19);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_19);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_18,"\\old(b)",0,
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__gen_e_acsl_assert_data_18.blocking = 1;
__gen_e_acsl_assert_data_18.kind = "Postcondition";
__gen_e_acsl_assert_data_18.pred_txt = "1 % \\old(b) == 1";
__gen_e_acsl_assert_data_18.file = "rte.i";
__gen_e_acsl_assert_data_18.fct = "test";
__gen_e_acsl_assert_data_18.line = 8;
- __e_acsl_assert(1 % __gen_e_acsl_at == 1,& __gen_e_acsl_assert_data_18);
+ __e_acsl_assert(1 % __gen_e_acsl_at_2 == 1,& __gen_e_acsl_assert_data_18);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_18);
__gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,0UL);
@@ -362,18 +362,18 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_21 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_21,
- "__gen_e_acsl_at_2",0,__gen_e_acsl_at_2);
+ "__gen_e_acsl_at",0,__gen_e_acsl_at);
__gen_e_acsl_assert_data_21.blocking = 1;
__gen_e_acsl_assert_data_21.kind = "RTE";
- __gen_e_acsl_assert_data_21.pred_txt = "__gen_e_acsl_at_2 != 0";
+ __gen_e_acsl_assert_data_21.pred_txt = "__gen_e_acsl_at != 0";
__gen_e_acsl_assert_data_21.file = "rte.i";
__gen_e_acsl_assert_data_21.fct = "test";
__gen_e_acsl_assert_data_21.line = 18;
__gen_e_acsl_assert_data_21.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_at_2 != 0,& __gen_e_acsl_assert_data_21);
+ __e_acsl_assert(__gen_e_acsl_at != 0,& __gen_e_acsl_assert_data_21);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_21);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_20,"\\old(e)",
- 0,__gen_e_acsl_at_2);
+ 0,__gen_e_acsl_at);
__gen_e_acsl_assert_data_20.blocking = 1;
__gen_e_acsl_assert_data_20.kind = "Postcondition";
__gen_e_acsl_assert_data_20.pred_txt = "1 % \\old(e) == 1";
@@ -381,8 +381,7 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__gen_e_acsl_assert_data_20.fct = "test";
__gen_e_acsl_assert_data_20.line = 18;
__gen_e_acsl_assert_data_20.name = "bhvr";
- __e_acsl_assert(1 % __gen_e_acsl_at_2 == 1,
- & __gen_e_acsl_assert_data_20);
+ __e_acsl_assert(1 % __gen_e_acsl_at == 1,& __gen_e_acsl_assert_data_20);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_20);
}
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/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/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 498e8881d33844d2151eea6f3457761ecf70eb49..8558e51e17a8de854f50382b249b38653d819419 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -736,6 +736,7 @@ void test_specifier_application(char const *allowed, char const *fmt,
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
unsigned long __gen_e_acsl_strcpy_src_size;
+ char *__gen_e_acsl_at_3;
char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
@@ -743,6 +744,7 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
__gen_e_acsl_at_2 = src;
+ __gen_e_acsl_at_3 = dest;
__gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
@@ -831,13 +833,19 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
char *__gen_e_acsl_strchr(char const *s, int c)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- int __gen_e_acsl_at_2;
+ int __gen_e_acsl_at_5;
+ char const *__gen_e_acsl_at_4;
+ char const *__gen_e_acsl_at_3;
+ char const *__gen_e_acsl_at_2;
char const *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
__e_acsl_store_block((void *)(& s),8UL);
__gen_e_acsl_at = s;
- __gen_e_acsl_at_2 = c;
+ __gen_e_acsl_at_2 = s;
+ __gen_e_acsl_at_3 = s;
+ __gen_e_acsl_at_4 = s;
+ __gen_e_acsl_at_5 = c;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__retres = strchr(s,c);
{
@@ -884,11 +892,11 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_3,"*\\result",
0,*__retres);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"\\old(c)",0,
- __gen_e_acsl_at_2);
+ __gen_e_acsl_at_5);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
__gen_e_acsl_base_addr = __e_acsl_base_addr((void *)__retres);
- __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at);
+ __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
"\\base_addr(\\result)",
__gen_e_acsl_base_addr);
@@ -912,7 +920,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__gen_e_acsl_assert_data_3.fct = "strchr";
__gen_e_acsl_assert_data_3.line = 198;
__gen_e_acsl_assert_data_3.name = "found/result_char";
- __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at_2),
+ __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at_5),
& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
@@ -1017,12 +1025,14 @@ pid_t __gen_e_acsl_fork(void)
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),8UL);
__gen_e_acsl_at = stat_loc;
+ __gen_e_acsl_at_2 = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL,
stat_loc == (int *)0);
@@ -1084,8 +1094,9 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__retres);
if (__retres >= 0) {
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",(void *)__gen_e_acsl_at);
- __gen_e_acsl_and = __gen_e_acsl_at != (int *)0;
+ "\\old(stat_loc)",
+ (void *)__gen_e_acsl_at_2);
+ __gen_e_acsl_and = __gen_e_acsl_at_2 != (int *)0;
}
else __gen_e_acsl_and = 0;
if (! __gen_e_acsl_and) __gen_e_acsl_implies = 1;
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
index c71892de48014543d30c8555794adacf3a65e450..667933a94dbeb38cd0bd72751672019c24045d62 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -63,8 +63,8 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
FILE * restrict stream)
{
size_t __gen_e_acsl_at_3;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- void *__gen_e_acsl_at;
+ void *__gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at;
size_t __retres;
{
__e_acsl_mpz_t __gen_e_acsl_size;
@@ -88,10 +88,10 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& stream),8UL);
__e_acsl_store_block((void *)(& ptr),8UL);
- __gen_e_acsl_at = ptr;
__gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_2 = ptr;
__gen_e_acsl_at_3 = nmemb;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
@@ -293,7 +293,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init(__gen_e_acsl_mul_4);
__gmpz_mul(__gen_e_acsl_mul_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
@@ -343,11 +343,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert(__gen_e_acsl_le_5 <= 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gen_e_acsl_size_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at_2 +
1 * 0),
__gen_e_acsl_size_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(ptr)",
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
@@ -356,7 +356,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__retres);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
@@ -390,7 +390,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_clear(__gen_e_acsl_mul_5);
__gmpz_clear(__gen_e_acsl_if_2);
__gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
index 81522c937fe323622587aadf2e3d27d16dad21fc..2080a3093e2a5d4d02b7d926e23ad669630ec33e 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -404,16 +404,18 @@ int main(void)
*/
void *__gen_e_acsl_memset(void *s, int c, size_t n)
{
- size_t __gen_e_acsl_at_3;
- int __gen_e_acsl_at_2;
+ void *__gen_e_acsl_at_4;
+ int __gen_e_acsl_at_3;
+ size_t __gen_e_acsl_at_2;
void *__gen_e_acsl_at;
void *__retres;
{
int __gen_e_acsl_valid_or_empty_here_2;
__e_acsl_store_block((void *)(& s),8UL);
__gen_e_acsl_at = s;
- __gen_e_acsl_at_2 = c;
- __gen_e_acsl_at_3 = n;
+ __gen_e_acsl_at_2 = n;
+ __gen_e_acsl_at_3 = c;
+ __gen_e_acsl_at_4 = s;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_or_empty_here_2 = __gen_e_acsl_valid_or_empty_here
(s,n);
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
index e41ebd61ec3c6acf70f8a66e6dde2be3f68edbfb..a4b1a052376bf9ef8b517c0f475d19f8ed5df1e5 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,9 +397,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at_5;
+ char *__gen_e_acsl_at_4;
__e_acsl_mpz_t __gen_e_acsl_at_3;
- char const *__gen_e_acsl_at_2;
- char *__gen_e_acsl_at;
+ char *__gen_e_acsl_at_2;
+ char const *__gen_e_acsl_at;
char *__retres;
{
__e_acsl_mpz_t __gen_e_acsl_n;
@@ -419,11 +432,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
- __gen_e_acsl_at = dest;
- __gen_e_acsl_at_2 = src;
+ __gen_e_acsl_at = src;
+ __gen_e_acsl_at_2 = dest;
__gmpz_init_set_ui(__gen_e_acsl_n,n);
__gmpz_init_set(__gen_e_acsl_at_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gen_e_acsl_at_4 = dest;
+ __gen_e_acsl_at_5 = dest;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -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_5);
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "Postcondition";
__gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(dest)";
@@ -613,7 +628,8 @@ 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_5,
+ & __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
@@ -635,11 +651,11 @@ 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_4 +
1 * 0),
__gen_e_acsl_if_6);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at_4);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
@@ -690,6 +706,7 @@ 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 *__gen_e_acsl_at_3;
char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
@@ -697,6 +714,7 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
__gen_e_acsl_at_2 = src;
+ __gen_e_acsl_at_3 = dest;
__gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
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_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
index 6fb11fbc1086ecc71d844419e4c02596e54227d5..b61de0193365722eb37c1ef30d0b5f15fd5fb131 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
@@ -801,8 +801,8 @@ int main(void)
*/
void __gen_e_acsl_g(long *ptr, size_t size)
{
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- long *__gen_e_acsl_at;
+ long *__gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at;
{
__e_acsl_mpz_t __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_size_2;
@@ -821,10 +821,10 @@ void __gen_e_acsl_g(long *ptr, size_t size)
unsigned long __gen_e_acsl_size_4;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& ptr),8UL);
- __gen_e_acsl_at = ptr;
__gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_2 = ptr;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gmpz_init_set_si(__gen_e_acsl_sizeof,8L);
__gmpz_init_set_ui(__gen_e_acsl_size_3,size);
@@ -940,7 +940,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_init_set_si(__gen_e_acsl__5,1L);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__gmpz_init_set_si(__gen_e_acsl__6,0L);
__gmpz_init(__gen_e_acsl_sub_3);
@@ -986,20 +986,20 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_assert(__gen_e_acsl_le_4 <= 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__gen_e_acsl_size_6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at +
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at_2 +
8 * 0),
__gen_e_acsl_size_6,
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"\\old(ptr)",
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(long)",
0,8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(long)",
0,8);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"size",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"size",0,
@@ -1029,7 +1029,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl_mul_2);
__gmpz_clear(__gen_e_acsl_if_2);
__gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at);
return;
}
}
diff --git a/src/plugins/e-acsl/tests/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};
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index e03df15a615064ed5a156a094c597055581026d7..b801bccbed31cf76400fa73cdb7fb16d9c2c6331 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -739,8 +739,9 @@ int main(void)
*/
void *__gen_e_acsl_memset(void *s, int c, size_t n)
{
- size_t __gen_e_acsl_at_3;
- int __gen_e_acsl_at_2;
+ void *__gen_e_acsl_at_4;
+ int __gen_e_acsl_at_3;
+ size_t __gen_e_acsl_at_2;
void *__gen_e_acsl_at;
void *__retres;
{
@@ -748,8 +749,9 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_store_block((void *)(& s),8UL);
__e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
__gen_e_acsl_at = s;
- __gen_e_acsl_at_2 = c;
- __gen_e_acsl_at_3 = n;
+ __gen_e_acsl_at_2 = n;
+ __gen_e_acsl_at_3 = c;
+ __gen_e_acsl_at_4 = s;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_valid_or_empty_here_2 = __gen_e_acsl_valid_or_empty_here
(s,n);