diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml
index ff1bc163c8f1c07afb893c08c85a28a4f3358d35..ecf2dad710ab28f9d08d2d8ac81989ee99fabaf6 100644
--- a/src/plugins/e-acsl/src/analyses/labels.ml
+++ b/src/plugins/e-acsl/src/analyses/labels.ml
@@ -401,7 +401,7 @@ module Process: sig
kernel_function ->
kinstr ->
stmt ->
- Smart_stmt.annotation_kind ->
+ annotation_kind ->
lscope ->
term ->
unit
@@ -416,7 +416,7 @@ module Process: sig
kernel_function ->
kinstr ->
stmt ->
- Smart_stmt.annotation_kind ->
+ annotation_kind ->
lscope ->
predicate ->
unit
@@ -438,7 +438,7 @@ end = struct
(** Statement of the predicate or term being analysed. *)
stmt: stmt;
(** King of annotation for the predicate or term being analysed. *)
- akind: Smart_stmt.annotation_kind;
+ akind: annotation_kind;
(** Logic scope for the predicate or term being analysed. *)
lscope: Lscope.t;
}
@@ -462,12 +462,12 @@ end = struct
(** @return a textual representation of the given kind of annotation. *)
let akind_to_string k =
match k with
- | Smart_stmt.Assertion -> "Assertion"
- | Smart_stmt.Precondition -> "Precondition"
- | Smart_stmt.Postcondition -> "Postcondition"
- | Smart_stmt.Invariant -> "Invariant"
- | Smart_stmt.Variant -> "Variant"
- | Smart_stmt.RTE -> "RTE"
+ | Assertion -> "Assertion"
+ | Precondition -> "Precondition"
+ | Postcondition -> "Postcondition"
+ | Invariant -> "Invariant"
+ | Variant -> "Variant"
+ | RTE -> "RTE"
(** Apply [fct ?error env] on every element of the list [args]. *)
let do_list fct ?error env args =
@@ -493,15 +493,15 @@ end = struct
(* Translate on the statement corresponding to the [Pre] label of the
enclosing function. *)
- | Kglobal, Smart_stmt.Postcondition, BuiltinLabel(Pre | Old) ->
+ | Kglobal, Postcondition, BuiltinLabel(Pre | Old) ->
error, Some env.pre_func_stmt
- | Kstmt _, Smart_stmt.(Precondition | Postcondition), BuiltinLabel(Pre) ->
+ | Kstmt _, (Precondition | Postcondition), BuiltinLabel(Pre) ->
error, Some env.pre_func_stmt
- | _, Smart_stmt.Assertion, BuiltinLabel(Pre) ->
+ | _, Assertion, BuiltinLabel(Pre) ->
error, Some env.pre_func_stmt
(* Translate before the current statement. *)
- | Kstmt stmt, Smart_stmt.Postcondition, BuiltinLabel(Old) ->
+ | Kstmt stmt, Postcondition, BuiltinLabel(Old) ->
if not (Cil_datatype.Stmt.equal stmt env.stmt) then
Options.fatal
"The statement of the kinstr and the current statement should \
@@ -511,16 +511,16 @@ end = struct
(* In-place translations *)
| _, _, BuiltinLabel(Here) ->
error, None
- | Kglobal, Smart_stmt.Precondition, BuiltinLabel(Pre | Old) ->
+ | Kglobal, Precondition, BuiltinLabel(Pre | Old) ->
error, None
- | _, Smart_stmt.Postcondition, BuiltinLabel(Post) ->
+ | _, Postcondition, BuiltinLabel(Post) ->
error, None
- | Kstmt _, Smart_stmt.Precondition, BuiltinLabel(Old) ->
+ | Kstmt _, Precondition, BuiltinLabel(Old) ->
error, None
(* Invalid position for the given label *)
- | _, Smart_stmt.Assertion, BuiltinLabel(Old | Post)
- | _, Smart_stmt.Precondition, BuiltinLabel(Post) ->
+ | _, Assertion, BuiltinLabel(Old | Post)
+ | _, Precondition, BuiltinLabel(Post) ->
let msg =
Format.asprintf "label '%a' within annotation '%s' in '%a'"
Printer.pp_logic_label label
@@ -773,7 +773,7 @@ end
class vis_at_labels () =
object (self)
- inherit E_acsl_visitor.visitor
+ inherit E_acsl_visitor.visitor dkey
(** Statement corresponding to the [Pre] label of the enclosing function*)
val mutable pre_func_stmt: stmt option = None
@@ -858,7 +858,7 @@ class vis_at_labels () =
method process_spec ?error kf kinstr stmt spec =
List.iter
(fun bhv ->
- let akind = Smart_stmt.Precondition in
+ let akind = Precondition in
List.iter
(fun assumes -> self#process_id_pred kf kinstr stmt akind assumes)
bhv.b_assumes;
@@ -868,7 +868,7 @@ class vis_at_labels () =
(Property.ip_of_requires kf kinstr bhv requires) then
self#process_id_pred kf kinstr stmt akind requires)
bhv.b_requires;
- let akind = Smart_stmt.Postcondition in
+ let akind = Postcondition in
(* The links between the [identified_property]s and the [assigns] or
[allocates] clauses are not clear. For now store a [not_yet] error
for every term of the clauses. Update the code to add the relevant
@@ -925,7 +925,7 @@ class vis_at_labels () =
kf
kinstr
stmt
- Smart_stmt.Assertion
+ Assertion
p.tp_statement
| AStmtSpec(l, spec) ->
let error =
@@ -950,13 +950,13 @@ class vis_at_labels () =
kf
kinstr
stmt
- Smart_stmt.Invariant
+ Invariant
p.tp_statement
end
| AVariant(t, _) ->
if !must_translate_ppt_ref
(Property.ip_of_code_annot_single kf stmt annot) then
- self#process_term kf kinstr stmt Smart_stmt.Variant t
+ self#process_term kf kinstr stmt Variant t
| AAssigns (_, assigns) ->
(* The link between the [identified_property] and the [assigns]
clause is not clear. For now store a [not_yet] error for every
@@ -969,7 +969,7 @@ class vis_at_labels () =
kf
kinstr
stmt
- (Smart_stmt.Postcondition)
+ Postcondition
assigns
| AAllocation (_, allocates) ->
(* The link between the [identified_property] and the [allocates]
@@ -983,7 +983,7 @@ class vis_at_labels () =
kf
kinstr
stmt
- (Smart_stmt.Postcondition)
+ Postcondition
allocates
| APragma _ -> ()
| AExtended _ -> ()
@@ -1015,3 +1015,9 @@ let pp_at_data = AtData.pretty
let _debug () =
Options.feedback ~level:2 "Labels preprocessing";
Translation._debug ()
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/analyses/labels.mli b/src/plugins/e-acsl/src/analyses/labels.mli
index dafff0e4e0dc63dafc2033a69571fe7859cdae75..92f7ee4a663e97cefd73dcbe1aeb821c710f0909 100644
--- a/src/plugins/e-acsl/src/analyses/labels.mli
+++ b/src/plugins/e-acsl/src/analyses/labels.mli
@@ -88,3 +88,9 @@ val must_translate_ppt_ref: (Property.t -> bool) ref
val must_translate_ppt_opt_ref: (Property.t option -> bool) ref
val has_empty_quantif_ref: ((term * logic_var * term) list -> bool) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
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 f3865d1f2f042441bd3124fed3575f1b75e91b29..d80d90f51a5fb5f56e02e59dd81038d7ce1da885 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
@@ -1,27 +1,37 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] at.i:38: Warning:
+[eva:alarm] at.i:48: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] at.i:13: Warning: assertion got status unknown.
-[eva:alarm] at.i:15: Warning: assertion got status unknown.
-[eva:alarm] at.i:54: Warning: assertion got status unknown.
-[eva:alarm] at.i:55: Warning: assertion got status unknown.
-[eva:alarm] at.i:56: Warning: assertion got status unknown.
-[eva:alarm] at.i:31: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] at.i:29: Warning:
+[eva:alarm] at.i:17: Warning: assertion got status unknown.
+[eva:alarm] at.i:19: Warning: assertion got status unknown.
+[eva:alarm] at.i:10: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[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:39: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] :0: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] at.i:29: Warning:
+[eva:alarm] at.i:39: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] at.i:39: 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:29: Warning: assertion got status unknown.
-[eva:alarm] at.i:31: Warning:
+[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:31: Warning: assertion got status unknown.
+[eva:alarm] at.i:41: Warning: assertion got status unknown.
+[eva:alarm] at.i:43: Warning: assertion got status unknown.
+[eva:alarm] at.i:59: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] at.i:62: 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/arith/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
index 2079be04d3c5a8254e004dbe5575667d74c81959..483ee2e7ba01554a0dd943dfc1aaa0df551c7306 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
@@ -4,7 +4,7 @@
`\at on purely logic variables that needs to allocate too much memory (bigger than int_max bytes)'
is not yet supported.
Ignoring annotation.
-[e-acsl] at_on-purely-logic-variables.c:69: Warning:
+[e-acsl] at_on-purely-logic-variables.c:70: Warning:
E-ACSL construct `\at with logic variable linked to C variable'
is not yet supported.
Ignoring annotation.
@@ -57,8 +57,8 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
- (int)(__gen_e_acsl_v_3 - -4)));
+ (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +
+ (int)(__gen_e_acsl_v_5 - -4)));
[eva:alarm] at_on-purely-logic-variables.c:44: Warning:
assertion got status unknown.
[eva:alarm] at_on-purely-logic-variables.c:8: Warning:
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 888d2c9fac9ba632c1a45380d70b369d72548fbe..9f178a13837c806c0575135acd2c7013ce7fd34c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -9,7 +9,11 @@
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
int A = 0;
-/*@ ensures \at(A,Post) == 3; */
+/*@ requires \at(A,Here) == 0;
+ requires \at(A,Pre) == 0;
+ ensures \at(A,Pre) == \old(A) == 0;
+ ensures \at(A,Post) == 4;
+ */
void __gen_e_acsl_f(void);
void f(void)
@@ -18,14 +22,11 @@ void f(void)
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __gen_e_acsl_at_3 = A;
__gen_e_acsl_at = A;
A = 1;
- F: {
- __gen_e_acsl_at_4 = __gen_e_acsl_at_3;
- __gen_e_acsl_at_2 = A;
- A = 2;
- }
+ F: __gen_e_acsl_at_2 = A;
+ __gen_e_acsl_at_3 = __gen_e_acsl_at;
+ 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,
@@ -35,7 +36,7 @@ void f(void)
__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 = 12;
+ __gen_e_acsl_assert_data.line = 16;
__e_acsl_assert(__gen_e_acsl_at == 0,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -50,7 +51,7 @@ void f(void)
__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 = 13;
+ __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_clean(& __gen_e_acsl_assert_data_2);
}
@@ -64,7 +65,7 @@ void f(void)
__gen_e_acsl_assert_data_3.pred_txt = "\\at(A,Here) == 2";
__gen_e_acsl_assert_data_3.file = "at.i";
__gen_e_acsl_assert_data_3.fct = "f";
- __gen_e_acsl_assert_data_3.line = 14;
+ __gen_e_acsl_assert_data_3.line = 18;
__e_acsl_assert(A == 2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
@@ -73,18 +74,75 @@ 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_4);
+ "\\at(\\at(A,Pre),F)",0,__gen_e_acsl_at_3);
__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 = 15;
- __e_acsl_assert(__gen_e_acsl_at_4 == 0,& __gen_e_acsl_assert_data_4);
+ __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_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \at(\at(A,Pre),F) == 0; */ ;
A = 3;
+ {
+ {
+ __gen_e_acsl_at_4 = 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);
+ __gen_e_acsl_assert_data_5.blocking = 1;
+ __gen_e_acsl_assert_data_5.kind = "Precondition";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\at(A,Here) == 3";
+ __gen_e_acsl_assert_data_5.file = "at.i";
+ __gen_e_acsl_assert_data_5.fct = "f";
+ __gen_e_acsl_assert_data_5.line = 21;
+ __e_acsl_assert(A == 3,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ }
+ /*@ requires \at(A,Here) == 3;
+ ensures \at(A,Pre) == 0;
+ ensures \old(A) == 3;
+ ensures \at(A,Post) == 4;
+ */
+ A = 4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"\\at(A,Pre)",
+ 0,__gen_e_acsl_at);
+ __gen_e_acsl_assert_data_6.blocking = 1;
+ __gen_e_acsl_assert_data_6.kind = "Postcondition";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\at(A,Pre) == 0";
+ __gen_e_acsl_assert_data_6.file = "at.i";
+ __gen_e_acsl_assert_data_6.fct = "f";
+ __gen_e_acsl_assert_data_6.line = 22;
+ __e_acsl_assert(__gen_e_acsl_at == 0,& __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};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"\\old(A)",0,
+ __gen_e_acsl_at_4);
+ __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_clean(& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,"A",0,A);
+ __gen_e_acsl_assert_data_8.blocking = 1;
+ __gen_e_acsl_assert_data_8.kind = "Postcondition";
+ __gen_e_acsl_assert_data_8.pred_txt = "\\at(A,Post) == 4";
+ __gen_e_acsl_assert_data_8.file = "at.i";
+ __gen_e_acsl_assert_data_8.fct = "f";
+ __gen_e_acsl_assert_data_8.line = 24;
+ __e_acsl_assert(A == 4,& __gen_e_acsl_assert_data_8);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
+ }
return;
}
@@ -103,137 +161,141 @@ void g(int *p, int *q)
*q = 0;
L1:
{
- {
- int __gen_e_acsl_valid_read_3;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
- {.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"q",
- (void *)q);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
- "sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,
- (void *)(& q));
- __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(q)";
- __gen_e_acsl_assert_data_5.file = "at.i";
- __gen_e_acsl_assert_data_5.fct = "g";
- __gen_e_acsl_assert_data_5.line = 31;
- __gen_e_acsl_assert_data_5.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_3,& __gen_e_acsl_assert_data_5);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- __gen_e_acsl_at_3 = *q;
- }
- {
- int __gen_e_acsl_valid_read;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
- {.values = (void *)0};
- __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_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,(void *)(& q));
- __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(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 = 29;
- __gen_e_acsl_assert_data_2.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gen_e_acsl_at = *q;
- }
+ int __gen_e_acsl_valid_read;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"q",(void *)q);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"sizeof(int)",
+ 0,sizeof(int));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "RTE";
+ __gen_e_acsl_assert_data.pred_txt = "mem_access: \\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;
+ __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;
}
+ *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_3 =
- {.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"p",
- (void *)p);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "__gen_e_acsl_at",0,__gen_e_acsl_at);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
- "sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __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(p + __gen_e_acsl_at)";
- __gen_e_acsl_assert_data_3.file = "at.i";
- __gen_e_acsl_assert_data_3.fct = "g";
- __gen_e_acsl_assert_data_3.line = 29;
- __gen_e_acsl_assert_data_3.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_3);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
- __gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
- }
- A = 4;
+ int __gen_e_acsl_valid_read_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __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);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+ "sizeof(int)",0,sizeof(int));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "RTE";
+ __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read(p + __gen_e_acsl_at)";
+ __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;
+ __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;
{
- __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ __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_assert_data.blocking = 1;
- __gen_e_acsl_assert_data.kind = "Assertion";
- __gen_e_acsl_assert_data.pred_txt = "\\at(*(p + \\at(*q,L1)),L2) == 2";
- __gen_e_acsl_assert_data.file = "at.i";
- __gen_e_acsl_assert_data.fct = "g";
- __gen_e_acsl_assert_data.line = 29;
- __e_acsl_assert(__gen_e_acsl_at_2 == 2,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __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.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);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
/*@ assert \at(*(p + \at(*q,L1)),L2) == 2; */ ;
L3:
{
+ 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};
+ __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);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
+ "sizeof(int)",0,sizeof(int));
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "RTE";
+ __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(p + __gen_e_acsl_at)";
+ __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;
+ __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);
+ __gen_e_acsl_at_3 = *(p + __gen_e_acsl_at);
+ __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,
"*(p + \\at(*q,L1))",0,
- *(p + __gen_e_acsl_at_3));
+ *(p + __gen_e_acsl_at));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"p",(void *)p);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_at_3",0,__gen_e_acsl_at_3);
+ "__gen_e_acsl_at",0,__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
sizeof(int),(void *)p,
(void *)(& p));
__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(p + __gen_e_acsl_at_3)";
+ __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\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 = 31;
- __gen_e_acsl_assert_data_6.name = "mem_access";
+ __gen_e_acsl_assert_data_6.line = 41;
__e_acsl_assert(__gen_e_acsl_valid_read_4,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- __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(*(p + \\at(*q,L1)),Here) == 2";
- __gen_e_acsl_assert_data_4.file = "at.i";
- __gen_e_acsl_assert_data_4.fct = "g";
- __gen_e_acsl_assert_data_4.line = 31;
- __e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,
- & __gen_e_acsl_assert_data_4);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_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)),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; */ ;
+ {
+ __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,
+ "\\at(*(p + \\at(*q,L1)),L3)",0,
+ __gen_e_acsl_at_3);
+ __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.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);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
+ }
+ /*@ assert \at(*(p + \at(*q,L1)),L3) == 2; */ ;
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
return;
@@ -249,9 +311,53 @@ int h(int x)
return x;
}
+void i(void)
+{
+ long __gen_e_acsl_at_2;
+ long __gen_e_acsl_at;
+ int a = 0;
+ {
+ __gen_e_acsl_at = (long)a;
+ /*@ ensures \old(a) + 1 == \at(a,Post); */
+ a ++;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,"\\old(a)",0,
+ __gen_e_acsl_at);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"a",0,a);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Postcondition";
+ __gen_e_acsl_assert_data.pred_txt = "\\old(a) + 1 == \\at(a,Post)";
+ __gen_e_acsl_assert_data.file = "at.i";
+ __gen_e_acsl_assert_data.fct = "i";
+ __gen_e_acsl_assert_data.line = 59;
+ __e_acsl_assert(__gen_e_acsl_at + 1L == (long)a,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ }
+ {
+ __gen_e_acsl_at_2 = (long)a;
+ /*@ ensures \old(a) + 1 == \at(a,Post); */
+ a ++;
+ __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(a)",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 = "Postcondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\old(a) + 1 == \\at(a,Post)";
+ __gen_e_acsl_assert_data_2.file = "at.i";
+ __gen_e_acsl_assert_data_2.fct = "i";
+ __gen_e_acsl_assert_data_2.line = 62;
+ __e_acsl_assert(__gen_e_acsl_at_2 + 1L == (long)a,
+ & __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ }
+ return;
+}
+
int main(void)
{
- long __gen_e_acsl_at_3;
long __gen_e_acsl_at_2;
int __gen_e_acsl_at;
int __retres;
@@ -264,24 +370,20 @@ int main(void)
x = __gen_e_acsl_h(0);
L:
{
- __gen_e_acsl_at_3 = (long)x;
- __gen_e_acsl_at_2 = x + 1L;
__gen_e_acsl_at = 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;
- __gen_e_acsl_assert_data.kind = "Assertion";
- __gen_e_acsl_assert_data.pred_txt = "x == 0";
- __gen_e_acsl_assert_data.file = "at.i";
- __gen_e_acsl_assert_data.fct = "main";
- __gen_e_acsl_assert_data.line = 48;
- __e_acsl_assert(x == 0,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- }
- /*@ assert x == 0; */ ;
+ __gen_e_acsl_at_2 = x + 1L;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"x",0,x);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "x == 0";
+ __gen_e_acsl_assert_data.file = "at.i";
+ __gen_e_acsl_assert_data.fct = "main";
+ __gen_e_acsl_assert_data.line = 71;
+ __e_acsl_assert(x == 0,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert x == 0; */ ;
__e_acsl_full_init((void *)(& x));
x = 1;
__e_acsl_full_init((void *)(& x));
@@ -297,7 +399,7 @@ int main(void)
__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 = 54;
+ __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_clean(& __gen_e_acsl_assert_data_2);
}
@@ -312,7 +414,7 @@ int main(void)
__gen_e_acsl_assert_data_3.pred_txt = "\\at(x + 1,L) == 1";
__gen_e_acsl_assert_data_3.file = "at.i";
__gen_e_acsl_assert_data_3.fct = "main";
- __gen_e_acsl_assert_data_3.line = 55;
+ __gen_e_acsl_assert_data_3.line = 78;
__e_acsl_assert(__gen_e_acsl_at_2 == 1L,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
@@ -320,20 +422,21 @@ int main(void)
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_4,"\\at(x,L)",0,
- __gen_e_acsl_at_3);
+ __e_acsl_assert_register_int(& __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 = 56;
- __e_acsl_assert(__gen_e_acsl_at_3 + 1L == 1L,
+ __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_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \at(x,L) + 1 == 1; */ ;
g(t,& x);
+ i();
__retres = 0;
__e_acsl_delete_block((void *)(t));
__e_acsl_delete_block((void *)(& x));
@@ -361,7 +464,7 @@ int __gen_e_acsl_h(int x)
__gen_e_acsl_assert_data.pred_txt = "\\result == \\old(x)";
__gen_e_acsl_assert_data.file = "at.i";
__gen_e_acsl_assert_data.fct = "h";
- __gen_e_acsl_assert_data.line = 38;
+ __gen_e_acsl_assert_data.line = 48;
__e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__e_acsl_delete_block((void *)(& x));
@@ -370,24 +473,75 @@ int __gen_e_acsl_h(int x)
}
}
-/*@ ensures \at(A,Post) == 3; */
+/*@ requires \at(A,Here) == 0;
+ requires \at(A,Pre) == 0;
+ ensures \at(A,Pre) == \old(A) == 0;
+ ensures \at(A,Post) == 4;
+ */
void __gen_e_acsl_f(void)
{
+ int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- f();
{
__gen_e_acsl_at = A;
+ __gen_e_acsl_at_2 = A;
__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,Post)",0,
- __gen_e_acsl_at);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"A",0,A);
__gen_e_acsl_assert_data.blocking = 1;
- __gen_e_acsl_assert_data.kind = "Postcondition";
- __gen_e_acsl_assert_data.pred_txt = "\\at(A,Post) == 3";
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "\\at(A,Here) == 0";
__gen_e_acsl_assert_data.file = "at.i";
__gen_e_acsl_assert_data.fct = "f";
- __gen_e_acsl_assert_data.line = 7;
- __e_acsl_assert(__gen_e_acsl_at == 3,& __gen_e_acsl_assert_data);
+ __gen_e_acsl_assert_data.line = 8;
+ __e_acsl_assert(A == 0,& __gen_e_acsl_assert_data);
__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);
+ __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_clean(& __gen_e_acsl_assert_data_2);
+ }
+ f();
+ {
+ int __gen_e_acsl_and;
+ __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);
+ __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) {
+ __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;
+ }
+ else __gen_e_acsl_and = 0;
+ __gen_e_acsl_assert_data_3.blocking = 1;
+ __gen_e_acsl_assert_data_3.kind = "Postcondition";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\at(A,Pre) == \\old(A) == 0";
+ __gen_e_acsl_assert_data_3.file = "at.i";
+ __gen_e_acsl_assert_data_3.fct = "f";
+ __gen_e_acsl_assert_data_3.line = 10;
+ __e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __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,"A",0,A);
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "Postcondition";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\at(A,Post) == 4";
+ __gen_e_acsl_assert_data_4.file = "at.i";
+ __gen_e_acsl_assert_data_4.fct = "f";
+ __gen_e_acsl_assert_data_4.line = 11;
+ __e_acsl_assert(A == 4,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
return;
}
}
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 9398cc676d2148b415c3b2fd7bf634e7274f861e..1e9af6023135f12963514b9fcbd469d275a408d4 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
@@ -30,26 +30,24 @@ void g(void)
m = 8;
Q:
{
- {
- int __gen_e_acsl_w_2;
- __gen_e_acsl_w_2 = 3;
- while (1) {
- if (__gen_e_acsl_w_2 < 6) ; else break;
- *(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L;
- __gen_e_acsl_w_2 ++;
- }
+ int __gen_e_acsl_w;
+ __gen_e_acsl_w = 3;
+ while (1) {
+ if (__gen_e_acsl_w < 6) ; else break;
+ *(__gen_e_acsl_at + (__gen_e_acsl_w - 3)) = m + (long)__gen_e_acsl_w == 12L;
+ __gen_e_acsl_w ++;
}
- ;
}
+ ;
m = 10;
{
int __gen_e_acsl_exists;
- int __gen_e_acsl_w;
+ int __gen_e_acsl_w_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_exists = 0;
- __gen_e_acsl_w = 3;
+ __gen_e_acsl_w_2 = 3;
while (1) {
- if (__gen_e_acsl_w < 6) ; else break;
+ if (__gen_e_acsl_w_2 < 6) ; else break;
{
int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -58,30 +56,30 @@ void g(void)
"__gen_e_acsl_at",
(void *)__gen_e_acsl_at);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "__gen_e_acsl_w",0,__gen_e_acsl_w);
+ "__gen_e_acsl_w_2",0,__gen_e_acsl_w_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
- __gen_e_acsl_w - 3L)),
+ __gen_e_acsl_w_2 - 3L)),
sizeof(int),
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
__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 + (int)(__gen_e_acsl_w - 3))";
+ __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3))";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "g";
__gen_e_acsl_assert_data_2.line = 16;
__gen_e_acsl_assert_data_2.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
+ if (! *(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3))) ;
else {
__gen_e_acsl_exists = 1;
goto e_acsl_end_loop1;
}
}
- __gen_e_acsl_w ++;
+ __gen_e_acsl_w_2 ++;
}
e_acsl_end_loop1: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
@@ -103,138 +101,134 @@ void g(void)
int main(void)
{
+ long *__gen_e_acsl_at_8;
int *__gen_e_acsl_at_7;
- int *__gen_e_acsl_at_6;
- long *__gen_e_acsl_at_5;
- long *__gen_e_acsl_at_4;
+ long *__gen_e_acsl_at_6;
+ int *__gen_e_acsl_at_5;
int *__gen_e_acsl_at_3;
- int *__gen_e_acsl_at_2;
+ long *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
int __retres;
int n;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __gen_e_acsl_at_8 = (long *)malloc((size_t)64);
__gen_e_acsl_at_7 = (int *)malloc((size_t)12000);
- __gen_e_acsl_at_6 = (int *)malloc((size_t)1536);
- __gen_e_acsl_at_5 = (long *)malloc((size_t)64);
- __gen_e_acsl_at_4 = (long *)malloc((size_t)8);
- __gen_e_acsl_at_3 = (int *)malloc((size_t)528);
- __gen_e_acsl_at_2 = (int *)malloc((size_t)12);
+ __gen_e_acsl_at_6 = (long *)malloc((size_t)3072);
+ __gen_e_acsl_at_5 = (int *)malloc((size_t)528);
+ __gen_e_acsl_at_3 = (int *)malloc((size_t)12);
+ __gen_e_acsl_at_2 = (long *)malloc((size_t)8);
__gen_e_acsl_at = (int *)malloc((size_t)4);
__e_acsl_store_block((void *)(& n),(size_t)4);
__e_acsl_full_init((void *)(& n));
n = 7;
L:
{
- {
- int __gen_e_acsl_i_4;
- __gen_e_acsl_i_4 = 3;
- *(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_4;
- }
- {
- int __gen_e_acsl_j_2;
- __gen_e_acsl_j_2 = 2;
- while (1) {
- if (__gen_e_acsl_j_2 < 5) ; else break;
- *(__gen_e_acsl_at_2 + (__gen_e_acsl_j_2 - 2)) = n + (long)__gen_e_acsl_j_2 == 11L;
- __gen_e_acsl_j_2 ++;
- }
- }
- {
- int __gen_e_acsl_i_2;
- __gen_e_acsl_i_2 = 3;
- *(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i_2 == 10L;
+ 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;
+ }
+ {
+ int __gen_e_acsl_j;
+ __gen_e_acsl_j = 2;
+ while (1) {
+ if (__gen_e_acsl_j < 5) ; else break;
+ *(__gen_e_acsl_at_3 + (__gen_e_acsl_j - 2)) = n + (long)__gen_e_acsl_j == 11L;
+ __gen_e_acsl_j ++;
}
- ;
}
+ ;
__e_acsl_full_init((void *)(& n));
n = 9;
K:
{
- {
- int __gen_e_acsl_u_6;
- int __gen_e_acsl_v_6;
- int __gen_e_acsl_w_2;
- __gen_e_acsl_u_6 = 10;
+ 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;
+ while (1) {
+ if (__gen_e_acsl_u < 21) ; else break;
+ __gen_e_acsl_v = -5 + 1;
while (1) {
- if (__gen_e_acsl_u_6 < 20) ; else break;
- __gen_e_acsl_v_6 = -10 + 1;
- while (1) {
- {
- int __gen_e_acsl_u_8;
- __gen_e_acsl_u_8 = -2;
- if (__gen_e_acsl_v_6 <= -5 + __gen_e_acsl_u_8) ; else break;
- }
- __gen_e_acsl_w_2 = 100 + 1;
- while (1) {
- if (__gen_e_acsl_w_2 <= 200) ; else break;
- {
- int __gen_e_acsl_u_7;
- __gen_e_acsl_u_7 = 42;
- *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_6 - 10) * 300 + (
- (__gen_e_acsl_v_6 - -9) * 100 + (
- __gen_e_acsl_w_2 - 101)))) = (((
- n - (long)__gen_e_acsl_u_6) + __gen_e_acsl_u_7) + __gen_e_acsl_v_6) + __gen_e_acsl_w_2 > 0L;
- }
- __gen_e_acsl_w_2 ++;
- }
- __gen_e_acsl_v_6 ++;
+ 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;
}
- __gen_e_acsl_u_6 ++;
+ __gen_e_acsl_v ++;
}
+ __gen_e_acsl_u ++;
}
- {
- int __gen_e_acsl_u_4;
- int __gen_e_acsl_v_4;
- __gen_e_acsl_u_4 = 9;
+ }
+ {
+ int __gen_e_acsl_u_2;
+ int __gen_e_acsl_v_2;
+ __gen_e_acsl_u_2 = 9;
+ while (1) {
+ if (__gen_e_acsl_u_2 < 21) ; else break;
+ __gen_e_acsl_v_2 = -5 + 1;
while (1) {
- if (__gen_e_acsl_u_4 < 21) ; else break;
- __gen_e_acsl_v_4 = -5 + 1;
- while (1) {
- {
- int __gen_e_acsl_if_2;
- if (__gen_e_acsl_u_4 < 15) __gen_e_acsl_if_2 = __gen_e_acsl_u_4 + 6;
- else __gen_e_acsl_if_2 = 3;
- if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
- }
- *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + (__gen_e_acsl_v_4 - -4))) =
- (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_4 > 0L;
- __gen_e_acsl_v_4 ++;
+ {
+ 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;
}
- __gen_e_acsl_u_4 ++;
+ *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 32 + (__gen_e_acsl_v_2 - -4))) =
+ (n + (long)__gen_e_acsl_u_2) + __gen_e_acsl_v_2;
+ __gen_e_acsl_v_2 ++;
}
+ __gen_e_acsl_u_2 ++;
}
- {
- int __gen_e_acsl_k_2;
- int __gen_e_acsl_u_2;
- int __gen_e_acsl_v_2;
- __gen_e_acsl_k_2 = -7;
- __gen_e_acsl_u_2 = 9;
+ }
+ {
+ int __gen_e_acsl_u_3;
+ int __gen_e_acsl_v_3;
+ int __gen_e_acsl_w;
+ __gen_e_acsl_u_3 = 10;
+ while (1) {
+ if (__gen_e_acsl_u_3 < 20) ; else break;
+ __gen_e_acsl_v_3 = -10 + 1;
while (1) {
- if (__gen_e_acsl_u_2 < 21) ; else break;
- __gen_e_acsl_v_2 = -5 + 1;
+ {
+ 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_v_2 <= 6) ; else break;
+ if (__gen_e_acsl_w <= 200) ; else break;
{
- long __gen_e_acsl_if;
- if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2;
- else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2;
- *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + (__gen_e_acsl_v_2 - -4))) =
- __gen_e_acsl_if > 0L;
+ 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_v_2 ++;
+ __gen_e_acsl_w ++;
}
- __gen_e_acsl_u_2 ++;
+ __gen_e_acsl_v_3 ++;
}
+ __gen_e_acsl_u_3 ++;
}
- ;
}
+ ;
__e_acsl_full_init((void *)(& n));
n = 666;
{
- int __gen_e_acsl_i;
+ int __gen_e_acsl_i_3;
int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __gen_e_acsl_i = 3;
+ __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));
@@ -269,32 +263,32 @@ int main(void)
/*@ assert \let i = 3; \at(n + i == 10,L); */ ;
{
int __gen_e_acsl_exists;
- int __gen_e_acsl_j;
+ int __gen_e_acsl_j_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__gen_e_acsl_exists = 0;
- __gen_e_acsl_j = 2;
+ __gen_e_acsl_j_2 = 2;
while (1) {
- if (__gen_e_acsl_j < 5) ; else break;
+ if (__gen_e_acsl_j_2 < 5) ; else break;
{
int __gen_e_acsl_valid_read_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (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",
+ (void *)__gen_e_acsl_at_3);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
- "__gen_e_acsl_j",0,__gen_e_acsl_j);
+ "__gen_e_acsl_j_2",0,__gen_e_acsl_j_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
- __gen_e_acsl_j - 2L)),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_3 + (int)(
+ __gen_e_acsl_j_2 - 2L)),
sizeof(int),
- (void *)__gen_e_acsl_at_2,
- (void *)(& __gen_e_acsl_at_2));
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__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 + (int)(__gen_e_acsl_j - 2))";
+ __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_3 + (int)(__gen_e_acsl_j_2 - 2))";
__gen_e_acsl_assert_data_4.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 29;
@@ -302,13 +296,13 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_2,
& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
- if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
+ if (! *(__gen_e_acsl_at_3 + (__gen_e_acsl_j_2 - 2))) ;
else {
__gen_e_acsl_exists = 1;
goto e_acsl_end_loop2;
}
}
- __gen_e_acsl_j ++;
+ __gen_e_acsl_j_2 ++;
}
e_acsl_end_loop2: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
@@ -325,48 +319,50 @@ int main(void)
}
/*@ assert \exists integer j; 2 <= j < 5 && \at(n + j == 11,L); */ ;
{
- int __gen_e_acsl_k;
+ int __gen_e_acsl_k_2;
int __gen_e_acsl_exists_2;
- int __gen_e_acsl_u;
+ int __gen_e_acsl_u_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl_k = -7;
+ __gen_e_acsl_k_2 = -7;
__gen_e_acsl_exists_2 = 0;
- __gen_e_acsl_u = 9;
+ __gen_e_acsl_u_6 = 9;
while (1) {
- if (__gen_e_acsl_u < 21) ; else break;
+ if (__gen_e_acsl_u_6 < 21) ; else break;
{
int __gen_e_acsl_forall;
- int __gen_e_acsl_v;
+ int __gen_e_acsl_v_4;
__gen_e_acsl_forall = 1;
- __gen_e_acsl_v = -5 + 1;
+ __gen_e_acsl_v_4 = -5 + 1;
while (1) {
- if (__gen_e_acsl_v <= 6) ; else break;
+ if (__gen_e_acsl_v_4 <= 6) ; else break;
{
int __gen_e_acsl_valid_read_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__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_5",
+ (void *)__gen_e_acsl_at_5);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_u",0,__gen_e_acsl_u);
+ "__gen_e_acsl_u_6",0,
+ __gen_e_acsl_u_6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_v",0,__gen_e_acsl_v);
+ "__gen_e_acsl_v_4",0,
+ __gen_e_acsl_v_4);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(
- __gen_e_acsl_at_3 + (int)(
+ __gen_e_acsl_at_5 + (int)(
(long)((int)(
(long)((int)(
- __gen_e_acsl_u - 9L)) * 11L)) + (int)(
- __gen_e_acsl_v - -4L))),
+ __gen_e_acsl_u_6 - 9L)) * 11L)) + (int)(
+ __gen_e_acsl_v_4 - -4L))),
sizeof(int),
- (void *)__gen_e_acsl_at_3,
- (void *)(& __gen_e_acsl_at_3));
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__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 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)(__gen_e_acsl_v - -4)))";
+ __gen_e_acsl_assert_data_6.pred_txt = "mem_access:\n \\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.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 34;
@@ -374,14 +370,14 @@ 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_3 + ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4))))
- ;
+ if (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_u_6 - 9) * 11 + (
+ __gen_e_acsl_v_4 - -4)))) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop3;
}
}
- __gen_e_acsl_v ++;
+ __gen_e_acsl_v_4 ++;
}
e_acsl_end_loop3: ;
if (! __gen_e_acsl_forall) ;
@@ -390,7 +386,7 @@ int main(void)
goto e_acsl_end_loop4;
}
}
- __gen_e_acsl_u ++;
+ __gen_e_acsl_u_6 ++;
}
e_acsl_end_loop4: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
@@ -413,27 +409,27 @@ int main(void)
*/
;
{
- int __gen_e_acsl_i_3;
+ int __gen_e_acsl_i_4;
int __gen_e_acsl_valid_read_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gen_e_acsl_i_3 = 3;
+ __gen_e_acsl_i_4 = 3;
__e_acsl_assert_register_long(& __gen_e_acsl_assert_data_7,
- "\\at(n + i,L)",0,*(__gen_e_acsl_at_4 + 0));
+ "\\at(n + i,L)",0,*(__gen_e_acsl_at_2 + 0));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,
- "__gen_e_acsl_at_4",
- (void *)__gen_e_acsl_at_4);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_8,
"sizeof(long)",0,sizeof(long));
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + 0),
sizeof(long),
- (void *)__gen_e_acsl_at_4,
- (void *)(& __gen_e_acsl_at_4));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__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(__gen_e_acsl_at_4 + 0)";
+ __gen_e_acsl_assert_data_8.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_2 + 0)";
__gen_e_acsl_assert_data_8.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_8.fct = "main";
__gen_e_acsl_assert_data_8.line = 38;
@@ -446,7 +442,7 @@ int main(void)
__gen_e_acsl_assert_data_7.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_7.fct = "main";
__gen_e_acsl_assert_data_7.line = 38;
- __e_acsl_assert(*(__gen_e_acsl_at_4 + 0) == 10L,
+ __e_acsl_assert(*(__gen_e_acsl_at_2 + 0) == 10L,
& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
}
@@ -454,46 +450,44 @@ int main(void)
unsigned int m = (unsigned int)3;
G:
{
- {
- int __gen_e_acsl_k_4;
- __gen_e_acsl_k_4 = -9 + 1;
- while (1) {
- if (__gen_e_acsl_k_4 < 0) ; else break;
- *(__gen_e_acsl_at_5 + (__gen_e_acsl_k_4 - -8)) = m + (long)__gen_e_acsl_k_4;
- __gen_e_acsl_k_4 ++;
- }
+ int __gen_e_acsl_k_3;
+ __gen_e_acsl_k_3 = -9 + 1;
+ while (1) {
+ if (__gen_e_acsl_k_3 < 0) ; else break;
+ *(__gen_e_acsl_at_8 + (__gen_e_acsl_k_3 - -8)) = m + (long)__gen_e_acsl_k_3;
+ __gen_e_acsl_k_3 ++;
}
- ;
}
+ ;
m = (unsigned int)(-3);
{
int __gen_e_acsl_exists_3;
- int __gen_e_acsl_k_3;
+ int __gen_e_acsl_k_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
__gen_e_acsl_exists_3 = 0;
- __gen_e_acsl_k_3 = -9 + 1;
+ __gen_e_acsl_k_4 = -9 + 1;
while (1) {
- if (__gen_e_acsl_k_3 < 0) ; else break;
+ if (__gen_e_acsl_k_4 < 0) ; else break;
{
int __gen_e_acsl_valid_read_5;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_10,
- "__gen_e_acsl_at_5",
- (void *)__gen_e_acsl_at_5);
+ "__gen_e_acsl_at_8",
+ (void *)__gen_e_acsl_at_8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_10,
- "__gen_e_acsl_k_3",0,__gen_e_acsl_k_3);
+ "__gen_e_acsl_k_4",0,__gen_e_acsl_k_4);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_10,
"sizeof(long)",0,sizeof(long));
- __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_5 + (int)(
- __gen_e_acsl_k_3 - -8L)),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_8 + (int)(
+ __gen_e_acsl_k_4 - -8L)),
sizeof(long),
- (void *)__gen_e_acsl_at_5,
- (void *)(& __gen_e_acsl_at_5));
+ (void *)__gen_e_acsl_at_8,
+ (void *)(& __gen_e_acsl_at_8));
__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_5 + (int)(__gen_e_acsl_k_3 - -8))";
+ __gen_e_acsl_assert_data_10.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_8 + (int)(__gen_e_acsl_k_4 - -8))";
__gen_e_acsl_assert_data_10.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_10.fct = "main";
__gen_e_acsl_assert_data_10.line = 42;
@@ -501,14 +495,14 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_5,
& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
- if (! (*(__gen_e_acsl_at_5 + (__gen_e_acsl_k_3 - -8)) == 0L))
+ if (! (*(__gen_e_acsl_at_8 + (__gen_e_acsl_k_4 - -8)) == 0L))
;
else {
__gen_e_acsl_exists_3 = 1;
goto e_acsl_end_loop5;
}
}
- __gen_e_acsl_k_3 ++;
+ __gen_e_acsl_k_4 ++;
}
e_acsl_end_loop5: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,
@@ -526,24 +520,24 @@ int main(void)
/*@ assert \exists integer k; -9 < k < 0 && \at(m + k,G) == 0; */ ;
{
int __gen_e_acsl_exists_4;
- int __gen_e_acsl_u_3;
+ int __gen_e_acsl_u_7;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__gen_e_acsl_exists_4 = 0;
- __gen_e_acsl_u_3 = 9;
+ __gen_e_acsl_u_7 = 9;
while (1) {
- if (__gen_e_acsl_u_3 < 21) ; else break;
+ if (__gen_e_acsl_u_7 < 21) ; else break;
{
int __gen_e_acsl_forall_2;
- int __gen_e_acsl_v_3;
+ int __gen_e_acsl_v_5;
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_v_3 = -5 + 1;
+ __gen_e_acsl_v_5 = -5 + 1;
while (1) {
{
int __gen_e_acsl_if_3;
- if (__gen_e_acsl_u_3 < 15) __gen_e_acsl_if_3 = __gen_e_acsl_u_3 + 6;
+ if (__gen_e_acsl_u_7 < 15) __gen_e_acsl_if_3 = __gen_e_acsl_u_7 + 6;
else __gen_e_acsl_if_3 = 3;
- if (__gen_e_acsl_v_3 <= __gen_e_acsl_if_3) ; else break;
+ if (__gen_e_acsl_v_5 <= __gen_e_acsl_if_3) ; else break;
}
{
int __gen_e_acsl_valid_read_6;
@@ -553,25 +547,25 @@ int main(void)
"__gen_e_acsl_at_6",
(void *)__gen_e_acsl_at_6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_12,
- "__gen_e_acsl_u_3",0,
- __gen_e_acsl_u_3);
+ "__gen_e_acsl_u_7",0,
+ __gen_e_acsl_u_7);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_12,
- "__gen_e_acsl_v_3",0,
- __gen_e_acsl_v_3);
+ "__gen_e_acsl_v_5",0,
+ __gen_e_acsl_v_5);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_12,
- "sizeof(int)",0,sizeof(int));
+ "sizeof(long)",0,sizeof(long));
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(
__gen_e_acsl_at_6 + (int)(
(long)((int)(
(long)((int)(
- __gen_e_acsl_u_3 - 9L)) * 32L)) + (int)(
- __gen_e_acsl_v_3 - -4L))),
- sizeof(int),
+ __gen_e_acsl_u_7 - 9L)) * 32L)) + (int)(
+ __gen_e_acsl_v_5 - -4L))),
+ sizeof(long),
(void *)__gen_e_acsl_at_6,
(void *)(& __gen_e_acsl_at_6));
__gen_e_acsl_assert_data_12.blocking = 1;
__gen_e_acsl_assert_data_12.kind = "RTE";
- __gen_e_acsl_assert_data_12.pred_txt = "\\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)(__gen_e_acsl_v_3 - -4)))";
+ __gen_e_acsl_assert_data_12.pred_txt = "mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +\n (int)(__gen_e_acsl_v_5 - -4)))";
__gen_e_acsl_assert_data_12.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 46;
@@ -582,17 +576,18 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32)
- + (int)(__gen_e_acsl_v_3 - -4)));
+ (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32)
+ + (int)(__gen_e_acsl_v_5 - -4)));
*/
- if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
- __gen_e_acsl_v_3 - -4)))) ;
+ if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_7 - 9) * 32 + (
+ __gen_e_acsl_v_5 - -4))) > 0L)
+ ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop6;
}
}
- __gen_e_acsl_v_3 ++;
+ __gen_e_acsl_v_5 ++;
}
e_acsl_end_loop6: ;
if (! __gen_e_acsl_forall_2) ;
@@ -601,15 +596,15 @@ int main(void)
goto e_acsl_end_loop7;
}
}
- __gen_e_acsl_u_3 ++;
+ __gen_e_acsl_u_7 ++;
}
e_acsl_end_loop7: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,
- "\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
+ "\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v,K) > 0)",
0,__gen_e_acsl_exists_4);
__gen_e_acsl_assert_data_11.blocking = 1;
__gen_e_acsl_assert_data_11.kind = "Assertion";
- __gen_e_acsl_assert_data_11.pred_txt = "\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))";
+ __gen_e_acsl_assert_data_11.pred_txt = "\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v,K) > 0)";
__gen_e_acsl_assert_data_11.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_11.fct = "main";
__gen_e_acsl_assert_data_11.line = 44;
@@ -621,7 +616,7 @@ int main(void)
\exists integer u;
9 <= u < 21 &&
(\forall integer v;
- -5 < v <= (u < 15? u + 6: 3) ==> \at((n + u) + v > 0,K));
+ -5 < v <= (u < 15? u + 6: 3) ==> \at((n + u) + v,K) > 0);
*/
;
int t[5] = {9, 12, 12, 12, -4};
@@ -631,31 +626,31 @@ int main(void)
g();
{
int __gen_e_acsl_exists_5;
- int __gen_e_acsl_u_5;
+ int __gen_e_acsl_u_8;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_13 =
{.values = (void *)0};
__gen_e_acsl_exists_5 = 0;
- __gen_e_acsl_u_5 = 10;
+ __gen_e_acsl_u_8 = 10;
while (1) {
- if (__gen_e_acsl_u_5 < 20) ; else break;
+ if (__gen_e_acsl_u_8 < 20) ; else break;
{
int __gen_e_acsl_exists_6;
- int __gen_e_acsl_v_5;
+ int __gen_e_acsl_v_6;
__gen_e_acsl_exists_6 = 0;
- __gen_e_acsl_v_5 = -10 + 1;
+ __gen_e_acsl_v_6 = -10 + 1;
while (1) {
{
int __gen_e_acsl_u_9;
__gen_e_acsl_u_9 = -2;
- if (__gen_e_acsl_v_5 <= -5 + __gen_e_acsl_u_9) ; else break;
+ if (__gen_e_acsl_v_6 <= -5 + __gen_e_acsl_u_9) ; else break;
}
{
int __gen_e_acsl_exists_7;
- int __gen_e_acsl_w;
+ int __gen_e_acsl_w_2;
__gen_e_acsl_exists_7 = 0;
- __gen_e_acsl_w = 100 + 1;
+ __gen_e_acsl_w_2 = 100 + 1;
while (1) {
- if (__gen_e_acsl_w <= 200) ; else break;
+ if (__gen_e_acsl_w_2 <= 200) ; else break;
{
int __gen_e_acsl_valid_read_7;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_14 =
@@ -664,31 +659,31 @@ int main(void)
"__gen_e_acsl_at_7",
(void *)__gen_e_acsl_at_7);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,
- "__gen_e_acsl_u_5",0,
- __gen_e_acsl_u_5);
+ "__gen_e_acsl_u_8",0,
+ __gen_e_acsl_u_8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,
- "__gen_e_acsl_v_5",0,
- __gen_e_acsl_v_5);
+ "__gen_e_acsl_v_6",0,
+ __gen_e_acsl_v_6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,
- "__gen_e_acsl_w",0,
- __gen_e_acsl_w);
+ "__gen_e_acsl_w_2",0,
+ __gen_e_acsl_w_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_14,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(
__gen_e_acsl_at_7 + (int)(
(long)((int)(
(long)((int)(
- __gen_e_acsl_u_5 - 10L)) * 300L)) + (int)(
+ __gen_e_acsl_u_8 - 10L)) * 300L)) + (int)(
(long)((int)(
(long)((int)(
- __gen_e_acsl_v_5 - -9L)) * 100L)) + (int)(
- __gen_e_acsl_w - 101L)))),
+ __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));
__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_5 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_5 - -9) * 100) +\n (int)(__gen_e_acsl_w - 101))))";
+ __gen_e_acsl_assert_data_14.pred_txt = "mem_access:\n \\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.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_14.fct = "main";
__gen_e_acsl_assert_data_14.line = 59;
@@ -696,16 +691,16 @@ 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_5 - 10) * 300 + (
- (__gen_e_acsl_v_5 - -9) * 100 + (
- __gen_e_acsl_w - 101)))))
+ if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_8 - 10) * 300 + (
+ (__gen_e_acsl_v_6 - -9) * 100 + (
+ __gen_e_acsl_w_2 - 101)))))
;
else {
__gen_e_acsl_exists_7 = 1;
goto e_acsl_end_loop8;
}
}
- __gen_e_acsl_w ++;
+ __gen_e_acsl_w_2 ++;
}
e_acsl_end_loop8: ;
if (! __gen_e_acsl_exists_7) ;
@@ -714,7 +709,7 @@ int main(void)
goto e_acsl_end_loop9;
}
}
- __gen_e_acsl_v_5 ++;
+ __gen_e_acsl_v_6 ++;
}
e_acsl_end_loop9: ;
if (! __gen_e_acsl_exists_6) ;
@@ -723,7 +718,7 @@ int main(void)
goto e_acsl_end_loop10;
}
}
- __gen_e_acsl_u_5 ++;
+ __gen_e_acsl_u_8 ++;
}
e_acsl_end_loop10: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,
@@ -759,10 +754,10 @@ int main(void)
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);
+ free((void *)__gen_e_acsl_at_8);
__e_acsl_memory_clean();
return __retres;
}
@@ -778,101 +773,97 @@ void __gen_e_acsl_f(int *t)
int *__gen_e_acsl_at_3;
int *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
- __gen_e_acsl_at_4 = (int *)malloc((size_t)4);
- __gen_e_acsl_at_3 = (int *)malloc((size_t)4);
- __gen_e_acsl_at_2 = (int *)malloc((size_t)8);
- __gen_e_acsl_at = (int *)malloc((size_t)8);
+ __gen_e_acsl_at_4 = (int *)malloc((size_t)8);
+ __gen_e_acsl_at_3 = (int *)malloc((size_t)8);
+ __gen_e_acsl_at_2 = (int *)malloc((size_t)4);
+ __gen_e_acsl_at = (int *)malloc((size_t)4);
__e_acsl_store_block((void *)(& t),(size_t)8);
{
- int __gen_e_acsl_m_3;
- __gen_e_acsl_m_3 = 4;
+ int __gen_e_acsl_m;
+ __gen_e_acsl_m = 4;
{
- int __gen_e_acsl_valid_read_7;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
+ int __gen_e_acsl_valid_read;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,"t",
- (void *)t);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,
- "__gen_e_acsl_m_3",0,__gen_e_acsl_m_3);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_9,
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"t",(void *)t);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "__gen_e_acsl_m",0,__gen_e_acsl_m);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(t + (int)(
- __gen_e_acsl_m_3 - 4L)),
- sizeof(int),(void *)t,
- (void *)(& t));
- __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(t + (int)(__gen_e_acsl_m_3 - 4))";
- __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;
- __gen_e_acsl_assert_data_9.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_7,& __gen_e_acsl_assert_data_9);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
- *(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m),
+ sizeof(int),(void *)t,
+ (void *)(& t));
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "RTE";
+ __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(t + __gen_e_acsl_m)";
+ __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;
+ __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;
}
}
{
int __gen_e_acsl_m_2;
__gen_e_acsl_m_2 = 4;
{
- int __gen_e_acsl_valid_read_5;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
+ int __gen_e_acsl_valid_read_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"t",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"t",
(void *)t);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
"__gen_e_acsl_m_2",0,__gen_e_acsl_m_2);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m_2),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (int)(
+ __gen_e_acsl_m_2 - 4L)),
sizeof(int),(void *)t,
(void *)(& t));
- __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(t + __gen_e_acsl_m_2)";
- __gen_e_acsl_assert_data_7.file = "at_on-purely-logic-variables.c";
- __gen_e_acsl_assert_data_7.fct = "f";
- __gen_e_acsl_assert_data_7.line = 8;
- __gen_e_acsl_assert_data_7.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_5,& __gen_e_acsl_assert_data_7);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- *(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4;
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "RTE";
+ __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read(t + (int)(__gen_e_acsl_m_2 - 4))";
+ __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;
+ __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));
}
}
{
- int __gen_e_acsl_n_3;
- __gen_e_acsl_n_3 = 1 + 1;
+ int __gen_e_acsl_n;
+ __gen_e_acsl_n = 1 + 1;
while (1) {
- if (__gen_e_acsl_n_3 <= 3) ; else break;
+ if (__gen_e_acsl_n <= 3) ; else break;
{
int __gen_e_acsl_valid_read_3;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"t",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"t",
(void *)t);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
- "__gen_e_acsl_n_3",0,__gen_e_acsl_n_3);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
+ "__gen_e_acsl_n",0,__gen_e_acsl_n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(t + (int)(
- __gen_e_acsl_n_3 - 1L)),
+ __gen_e_acsl_n - 1L)),
sizeof(int),
(void *)t,
(void *)(& t));
- __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(t + (int)(__gen_e_acsl_n_3 - 1))";
- __gen_e_acsl_assert_data_4.file = "at_on-purely-logic-variables.c";
- __gen_e_acsl_assert_data_4.fct = "f";
- __gen_e_acsl_assert_data_4.line = 7;
- __gen_e_acsl_assert_data_4.name = "mem_access";
+ __gen_e_acsl_assert_data_3.blocking = 1;
+ __gen_e_acsl_assert_data_3.kind = "RTE";
+ __gen_e_acsl_assert_data_3.pred_txt = "mem_access: \\valid_read(t + (int)(__gen_e_acsl_n - 1))";
+ __gen_e_acsl_assert_data_3.file = "at_on-purely-logic-variables.c";
+ __gen_e_acsl_assert_data_3.fct = "f";
+ __gen_e_acsl_assert_data_3.line = 7;
__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);
- *(__gen_e_acsl_at_2 + (__gen_e_acsl_n_3 - 2)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
+ & __gen_e_acsl_assert_data_3);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ *(__gen_e_acsl_at_3 + (__gen_e_acsl_n - 2)) = *(t + (__gen_e_acsl_n - 1)) > 5;
}
- __gen_e_acsl_n_3 ++;
+ __gen_e_acsl_n ++;
}
}
{
@@ -881,28 +872,29 @@ void __gen_e_acsl_f(int *t)
while (1) {
if (__gen_e_acsl_n_2 <= 3) ; else break;
{
- int __gen_e_acsl_valid_read;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ int __gen_e_acsl_valid_read_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"t",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"t",
(void *)t);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
"__gen_e_acsl_n_2",0,__gen_e_acsl_n_2);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_n_2),
- sizeof(int),(void *)t,
- (void *)(& t));
- __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 + __gen_e_acsl_n_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 = 7;
- __gen_e_acsl_assert_data_2.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- *(__gen_e_acsl_at + (__gen_e_acsl_n_2 - 2)) = *(t + __gen_e_acsl_n_2) == 12;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(t + __gen_e_acsl_n_2),
+ sizeof(int),
+ (void *)t,
+ (void *)(& t));
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "RTE";
+ __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(t + __gen_e_acsl_n_2)";
+ __gen_e_acsl_assert_data_4.file = "at_on-purely-logic-variables.c";
+ __gen_e_acsl_assert_data_4.fct = "f";
+ __gen_e_acsl_assert_data_4.line = 7;
+ __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_4 + (__gen_e_acsl_n_2 - 2)) = *(t + __gen_e_acsl_n_2) == 12;
}
__gen_e_acsl_n_2 ++;
}
@@ -910,69 +902,68 @@ void __gen_e_acsl_f(int *t)
f(t);
{
int __gen_e_acsl_forall;
- int __gen_e_acsl_n;
- int __gen_e_acsl_m;
- int __gen_e_acsl_valid_read_6;
+ int __gen_e_acsl_n_3;
+ int __gen_e_acsl_m_3;
+ int __gen_e_acsl_valid_read_7;
int __gen_e_acsl_and_2;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
+ {.values = (void *)0};
__gen_e_acsl_forall = 1;
- __gen_e_acsl_n = 1 + 1;
+ __gen_e_acsl_n_3 = 1 + 1;
while (1) {
- if (__gen_e_acsl_n <= 3) ; else break;
+ if (__gen_e_acsl_n_3 <= 3) ; else break;
{
- int __gen_e_acsl_valid_read_2;
+ int __gen_e_acsl_valid_read_5;
int __gen_e_acsl_and;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "__gen_e_acsl_at",
- (void *)__gen_e_acsl_at);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "__gen_e_acsl_n",0,__gen_e_acsl_n);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
+ "__gen_e_acsl_at_4",
+ (void *)__gen_e_acsl_at_4);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
+ "__gen_e_acsl_n_3",0,__gen_e_acsl_n_3);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
- __gen_e_acsl_n - 2L)),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + (int)(
+ __gen_e_acsl_n_3 - 2L)),
sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
- __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 + (int)(__gen_e_acsl_n - 2))";
- __gen_e_acsl_assert_data_3.file = "at_on-purely-logic-variables.c";
- __gen_e_acsl_assert_data_3.fct = "f";
- __gen_e_acsl_assert_data_3.line = 7;
- __gen_e_acsl_assert_data_3.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_2,
- & __gen_e_acsl_assert_data_3);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
- if (*(__gen_e_acsl_at + (__gen_e_acsl_n - 2))) {
- int __gen_e_acsl_valid_read_4;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
+ __gen_e_acsl_assert_data_6.blocking = 1;
+ __gen_e_acsl_assert_data_6.kind = "RTE";
+ __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_4 + (int)(__gen_e_acsl_n_3 - 2))";
+ __gen_e_acsl_assert_data_6.file = "at_on-purely-logic-variables.c";
+ __gen_e_acsl_assert_data_6.fct = "f";
+ __gen_e_acsl_assert_data_6.line = 7;
+ __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);
+ if (*(__gen_e_acsl_at_4 + (__gen_e_acsl_n_3 - 2))) {
+ int __gen_e_acsl_valid_read_6;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
- "__gen_e_acsl_at_2",
- (void *)__gen_e_acsl_at_2);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
- "__gen_e_acsl_n",0,__gen_e_acsl_n);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,
+ "__gen_e_acsl_at_3",
+ (void *)__gen_e_acsl_at_3);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
+ "__gen_e_acsl_n_3",0,__gen_e_acsl_n_3);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
- __gen_e_acsl_n - 2L)),
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_3 + (int)(
+ __gen_e_acsl_n_3 - 2L)),
sizeof(int),
- (void *)__gen_e_acsl_at_2,
- (void *)(& __gen_e_acsl_at_2));
- __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_2 + (int)(__gen_e_acsl_n - 2))";
- __gen_e_acsl_assert_data_5.file = "at_on-purely-logic-variables.c";
- __gen_e_acsl_assert_data_5.fct = "f";
- __gen_e_acsl_assert_data_5.line = 7;
- __gen_e_acsl_assert_data_5.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_4,
- & __gen_e_acsl_assert_data_5);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- __gen_e_acsl_and = *(__gen_e_acsl_at_2 + (__gen_e_acsl_n - 2));
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
+ __gen_e_acsl_assert_data_7.blocking = 1;
+ __gen_e_acsl_assert_data_7.kind = "RTE";
+ __gen_e_acsl_assert_data_7.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_3 + (int)(__gen_e_acsl_n_3 - 2))";
+ __gen_e_acsl_assert_data_7.file = "at_on-purely-logic-variables.c";
+ __gen_e_acsl_assert_data_7.fct = "f";
+ __gen_e_acsl_assert_data_7.line = 7;
+ __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);
+ __gen_e_acsl_and = *(__gen_e_acsl_at_3 + (__gen_e_acsl_n_3 - 2));
}
else __gen_e_acsl_and = 0;
if (__gen_e_acsl_and) ;
@@ -981,65 +972,63 @@ void __gen_e_acsl_f(int *t)
goto e_acsl_end_loop11;
}
}
- __gen_e_acsl_n ++;
+ __gen_e_acsl_n_3 ++;
}
e_acsl_end_loop11: ;
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
"\\forall integer n;\n 1 < n <= 3 ==> \\old(*(t + n) == 12) && \\old(*(t + (n - 1)) > 5)",
0,__gen_e_acsl_forall);
- __gen_e_acsl_assert_data.blocking = 1;
- __gen_e_acsl_assert_data.kind = "Postcondition";
- __gen_e_acsl_assert_data.pred_txt = "\\forall integer n;\n 1 < n <= 3 ==> \\old(*(t + n) == 12) && \\old(*(t + (n - 1)) > 5)";
- __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 = 6;
- __e_acsl_assert(__gen_e_acsl_forall,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
+ __gen_e_acsl_assert_data_5.blocking = 1;
+ __gen_e_acsl_assert_data_5.kind = "Postcondition";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\forall integer n;\n 1 < n <= 3 ==> \\old(*(t + n) == 12) && \\old(*(t + (n - 1)) > 5)";
+ __gen_e_acsl_assert_data_5.file = "at_on-purely-logic-variables.c";
+ __gen_e_acsl_assert_data_5.fct = "f";
+ __gen_e_acsl_assert_data_5.line = 6;
+ __e_acsl_assert(__gen_e_acsl_forall,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
- __gen_e_acsl_m = 4;
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
+ __gen_e_acsl_m_3 = 4;
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
"\\old(*(t + m) == -4)",0,
- *(__gen_e_acsl_at_3 + 0));
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
+ *(__gen_e_acsl_at + 0));
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,
- "__gen_e_acsl_at_3",
- (void *)__gen_e_acsl_at_3);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_8,
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,
+ "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_9,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_3 + 0),
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
sizeof(int),
- (void *)__gen_e_acsl_at_3,
- (void *)(& __gen_e_acsl_at_3));
- __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(__gen_e_acsl_at_3 + 0)";
- __gen_e_acsl_assert_data_8.file = "at_on-purely-logic-variables.c";
- __gen_e_acsl_assert_data_8.fct = "f";
- __gen_e_acsl_assert_data_8.line = 8;
- __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);
- if (*(__gen_e_acsl_at_3 + 0)) {
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __gen_e_acsl_assert_data_9.blocking = 1;
+ __gen_e_acsl_assert_data_9.kind = "RTE";
+ __gen_e_acsl_assert_data_9.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at + 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;
+ __e_acsl_assert(__gen_e_acsl_valid_read_7,& __gen_e_acsl_assert_data_9);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
+ if (*(__gen_e_acsl_at + 0)) {
int __gen_e_acsl_valid_read_8;
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
"\\old(*(t + (m - 4)))",0,
- *(__gen_e_acsl_at_4 + 0));
+ *(__gen_e_acsl_at_2 + 0));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_10,
- "__gen_e_acsl_at_4",
- (void *)__gen_e_acsl_at_4);
+ "__gen_e_acsl_at_2",
+ (void *)__gen_e_acsl_at_2);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_10,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
+ __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + 0),
sizeof(int),
- (void *)__gen_e_acsl_at_4,
- (void *)(& __gen_e_acsl_at_4));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__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_4 + 0)";
+ __gen_e_acsl_assert_data_10.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_2 + 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;
@@ -1047,17 +1036,17 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert(__gen_e_acsl_valid_read_8,
& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
- __gen_e_acsl_and_2 = *(__gen_e_acsl_at_4 + 0) == 9;
+ __gen_e_acsl_and_2 = *(__gen_e_acsl_at_2 + 0) == 9;
}
else __gen_e_acsl_and_2 = 0;
- __gen_e_acsl_assert_data_6.blocking = 1;
- __gen_e_acsl_assert_data_6.kind = "Postcondition";
- __gen_e_acsl_assert_data_6.pred_txt = "\\let m = 4; \\old(*(t + m) == -4) && \\old(*(t + (m - 4))) == 9";
- __gen_e_acsl_assert_data_6.file = "at_on-purely-logic-variables.c";
- __gen_e_acsl_assert_data_6.fct = "f";
- __gen_e_acsl_assert_data_6.line = 8;
- __e_acsl_assert(__gen_e_acsl_and_2,& __gen_e_acsl_assert_data_6);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
+ __gen_e_acsl_assert_data_8.blocking = 1;
+ __gen_e_acsl_assert_data_8.kind = "Postcondition";
+ __gen_e_acsl_assert_data_8.pred_txt = "\\let m = 4; \\old(*(t + m) == -4) && \\old(*(t + (m - 4))) == 9";
+ __gen_e_acsl_assert_data_8.file = "at_on-purely-logic-variables.c";
+ __gen_e_acsl_assert_data_8.fct = "f";
+ __gen_e_acsl_assert_data_8.line = 8;
+ __e_acsl_assert(__gen_e_acsl_and_2,& __gen_e_acsl_assert_data_8);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
__e_acsl_delete_block((void *)(& t));
free((void *)__gen_e_acsl_at);
free((void *)__gen_e_acsl_at_2);
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 189169fa1e0f2750dae762e7b894217bf8d20c39..43188869d2bf8a7e6e5d346fb82881ec4d3da6c7 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
@@ -359,13 +359,13 @@ double __gen_e_acsl_avg(double a, double b)
double __gen_e_acsl_at_2;
__e_acsl_mpq_t __gen_e_acsl_at;
double __retres;
- __gen_e_acsl_at_2 = b;
{
__e_acsl_mpq_t __gen_e_acsl_a;
__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));
+ __gen_e_acsl_at_2 = b;
__gmpq_clear(__gen_e_acsl_a);
}
__retres = avg(a,b);
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 4683310c7c5aa6cb601f118d1a34e10cecb0c3e4..91b3577515f914de25c8b42d016d2b5bbdeeca51 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -95,13 +95,10 @@ int main(void)
*/
void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
- float *__gen_e_acsl_at_6;
- float *__gen_e_acsl_at_5;
- float *__gen_e_acsl_at_4;
+ __e_acsl_contract_t *__gen_e_acsl_contract;
float *__gen_e_acsl_at_3;
float *__gen_e_acsl_at_2;
float *__gen_e_acsl_at;
- __e_acsl_contract_t *__gen_e_acsl_contract;
{
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
@@ -109,6 +106,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
__e_acsl_store_block((void *)(& Mwmin),(size_t)8);
__e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
+ __gen_e_acsl_at = Mtmin_in;
+ __gen_e_acsl_at_2 = Mwmin;
+ __gen_e_acsl_at_3 = Mtmin_out;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"Mtmin_in",
@@ -167,12 +167,6 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1);
}
- __gen_e_acsl_at_6 = Mwmin;
- __gen_e_acsl_at_5 = Mtmin_in;
- __gen_e_acsl_at_4 = Mwmin;
- __gen_e_acsl_at_3 = Mtmin_in;
- __gen_e_acsl_at_2 = Mtmin_in;
- __gen_e_acsl_at = Mtmin_out;
bar(Mtmin_in,Mwmin,Mtmin_out);
{
int __gen_e_acsl_assumes_value;
@@ -186,23 +180,22 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_out)",*__gen_e_acsl_at);
+ "*\\old(Mtmin_out)",*__gen_e_acsl_at_3);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at_2);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
- "__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_5,
"sizeof(float)",0,sizeof(float));
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at,
sizeof(float),
- (void *)__gen_e_acsl_at_2,
- (void *)(& __gen_e_acsl_at_2));
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__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_2)";
+ __gen_e_acsl_assert_data_5.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at)";
__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;
@@ -212,42 +205,43 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_at",(void *)__gen_e_acsl_at);
+ "__gen_e_acsl_at_3",
+ (void *)__gen_e_acsl_at_3);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"sizeof(float)",0,sizeof(float));
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
sizeof(float),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__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)";
+ __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_3)";
__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 == *__gen_e_acsl_at_2) {
+ if (*__gen_e_acsl_at_3 == *__gen_e_acsl_at) {
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl_mul;
__e_acsl_mpq_t __gen_e_acsl__3;
int __gen_e_acsl_lt;
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at_3);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at);
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"085/100",10);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmin)",*__gen_e_acsl_at_4);
+ "*\\old(Mwmin)",*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_4);
+ __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3);
+ __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at);
__gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__gen_e_acsl_and = __gen_e_acsl_lt < 0;
@@ -260,21 +254,21 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
if (__gen_e_acsl_and) {
int __gen_e_acsl_valid_read_3;
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmin_in)",*__gen_e_acsl_at_5);
+ "*\\old(Mtmin_in)",*__gen_e_acsl_at);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,
- "__gen_e_acsl_at_5",
- (void *)__gen_e_acsl_at_5);
+ "__gen_e_acsl_at",
+ (void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,
"sizeof(float)",0,sizeof(float));
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5,
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
sizeof(float),
- (void *)__gen_e_acsl_at_5,
- (void *)(& __gen_e_acsl_at_5));
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__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_5)";
+ __gen_e_acsl_assert_data_7.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at)";
__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;
@@ -282,7 +276,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_valid_read_3,
& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- __gen_e_acsl_if = (double)*__gen_e_acsl_at_5 != 0.;
+ __gen_e_acsl_if = (double)*__gen_e_acsl_at != 0.;
}
else {
__e_acsl_mpq_t __gen_e_acsl__4;
@@ -293,9 +287,9 @@ 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);
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmin)",*__gen_e_acsl_at_6);
+ "*\\old(Mwmin)",*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl__5);
- __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_6);
+ __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl_mul_2);
__gmpq_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
@@ -340,10 +334,10 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
*/
void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
+ __e_acsl_contract_t *__gen_e_acsl_contract;
float *__gen_e_acsl_at_3;
float *__gen_e_acsl_at_2;
float *__gen_e_acsl_at;
- __e_acsl_contract_t *__gen_e_acsl_contract;
{
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
@@ -351,6 +345,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
__e_acsl_store_block((void *)(& Mwmax),(size_t)8);
__e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
+ __gen_e_acsl_at = Mtmax_in;
+ __gen_e_acsl_at_2 = Mwmax;
+ __gen_e_acsl_at_3 = Mtmax_out;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"Mtmax_in",
@@ -409,9 +406,6 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1);
}
- __gen_e_acsl_at_3 = Mwmax;
- __gen_e_acsl_at_2 = Mtmax_in;
- __gen_e_acsl_at = Mtmax_out;
foo(Mtmax_in,Mwmax,Mtmax_out);
{
int __gen_e_acsl_assumes_value;
@@ -434,9 +428,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mtmax_out)",*__gen_e_acsl_at);
+ "*\\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_2);
+ "*\\old(Mtmax_in)",*__gen_e_acsl_at);
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"5",10);
__gmpq_init(__gen_e_acsl__2);
@@ -448,9 +442,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
__e_acsl_assert_register_float(& __gen_e_acsl_assert_data_4,
- "*\\old(Mwmax)",*__gen_e_acsl_at_3);
+ "*\\old(Mwmax)",*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl__4);
- __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_3);
+ __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div),
@@ -466,13 +460,13 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2));
__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_add);
__gmpq_add(__gen_e_acsl_add,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__gmpq_init(__gen_e_acsl__7);
- __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at);
+ __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at_3);
__gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
__gen_e_acsl_assert_data_4.blocking = 1;
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 e48c777bf33ec8b67b026477260fdad73930a82d..eb58dccf2f55da9a1211ad762c48191f56b73a15 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -57,20 +57,12 @@ int main(void)
void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int *AverageAccel)
{
- ArrayInt *__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;
- int *__gen_e_acsl_at;
+ int *__gen_e_acsl_at_2;
+ ArrayInt *__gen_e_acsl_at;
__e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
__e_acsl_store_block((void *)(& Accel),(size_t)8);
- __gen_e_acsl_at_6 = Accel;
- __gen_e_acsl_at_5 = Accel;
- __gen_e_acsl_at_4 = Accel;
- __gen_e_acsl_at_3 = Accel;
- __gen_e_acsl_at_2 = Accel;
- __gen_e_acsl_at = AverageAccel;
+ __gen_e_acsl_at = Accel;
+ __gen_e_acsl_at_2 = AverageAccel;
atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
{
int __gen_e_acsl_valid_read;
@@ -81,36 +73,36 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int __gen_e_acsl_valid_read_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "*\\old(AverageAccel)",0,*__gen_e_acsl_at);
+ "*\\old(AverageAccel)",0,*__gen_e_acsl_at_2);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[4]",0,
- (*__gen_e_acsl_at_2)[4]);
+ (*__gen_e_acsl_at)[4]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[3]",0,
- (*__gen_e_acsl_at_3)[3]);
+ (*__gen_e_acsl_at)[3]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[2]",0,
- (*__gen_e_acsl_at_4)[2]);
+ (*__gen_e_acsl_at)[2]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[1]",0,
- (*__gen_e_acsl_at_5)[1]);
+ (*__gen_e_acsl_at)[1]);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"(*\\old(Accel))[0]",0,
- (*__gen_e_acsl_at_6)[0]);
+ (*__gen_e_acsl_at)[0]);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
- "(int *)*__gen_e_acsl_at_6",
- (void *)(*__gen_e_acsl_at_6));
+ "(int *)*__gen_e_acsl_at",
+ (void *)(*__gen_e_acsl_at));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*__gen_e_acsl_at_6),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*__gen_e_acsl_at),
sizeof(int),
- (void *)(*__gen_e_acsl_at_6),
+ (void *)(*__gen_e_acsl_at),
(void *)0);
__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((int *)*__gen_e_acsl_at_6)";
+ __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read((int *)*__gen_e_acsl_at)";
__gen_e_acsl_assert_data_2.file = "bts1326.i";
__gen_e_acsl_assert_data_2.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_2.line = 8;
@@ -120,17 +112,17 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "&(*__gen_e_acsl_at_5)[1]",
- (void *)(& (*__gen_e_acsl_at_5)[1]));
+ "&(*__gen_e_acsl_at)[1]",
+ (void *)(& (*__gen_e_acsl_at)[1]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1]),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[1]),
sizeof(int),
- (void *)(*__gen_e_acsl_at_5),
+ (void *)(*__gen_e_acsl_at),
(void *)0);
__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_5)[1])";
+ __gen_e_acsl_assert_data_3.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[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;
@@ -140,17 +132,17 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
- "&(*__gen_e_acsl_at_4)[2]",
- (void *)(& (*__gen_e_acsl_at_4)[2]));
+ "&(*__gen_e_acsl_at)[2]",
+ (void *)(& (*__gen_e_acsl_at)[2]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2]),
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[2]),
sizeof(int),
- (void *)(*__gen_e_acsl_at_4),
+ (void *)(*__gen_e_acsl_at),
(void *)0);
__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_4)[2])";
+ __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[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;
@@ -160,17 +152,17 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,
- "&(*__gen_e_acsl_at_3)[3]",
- (void *)(& (*__gen_e_acsl_at_3)[3]));
+ "&(*__gen_e_acsl_at)[3]",
+ (void *)(& (*__gen_e_acsl_at)[3]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3]),
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[3]),
sizeof(int),
- (void *)(*__gen_e_acsl_at_3),
+ (void *)(*__gen_e_acsl_at),
(void *)0);
__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)[3])";
+ __gen_e_acsl_assert_data_5.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[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;
@@ -180,17 +172,17 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
- "&(*__gen_e_acsl_at_2)[4]",
- (void *)(& (*__gen_e_acsl_at_2)[4]));
+ "&(*__gen_e_acsl_at)[4]",
+ (void *)(& (*__gen_e_acsl_at)[4]));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4]),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at)[4]),
sizeof(int),
- (void *)(*__gen_e_acsl_at_2),
+ (void *)(*__gen_e_acsl_at),
(void *)0);
__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_2)[4])";
+ __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[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;
@@ -200,16 +192,17 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__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(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__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 = "mem_access: \\valid_read(__gen_e_acsl_at_2)";
__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;
@@ -222,7 +215,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 == (int)((((((*__gen_e_acsl_at_2)[4] + (long)(*__gen_e_acsl_at_3)[3]) + (*__gen_e_acsl_at_4)[2]) + (*__gen_e_acsl_at_5)[1]) + (*__gen_e_acsl_at_6)[0]) / 5L),
+ __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),
& __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 18254b245ea74905f0a1daf93f8bc1869b91ae03..1626dbd4ea419ee09b6a1d48eedcacd2f584b7df 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -70,9 +70,9 @@ 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;
- __e_acsl_contract_t *__gen_e_acsl_contract;
void *__retres;
__e_acsl_store_block((void *)(& __retres),(size_t)8);
{
@@ -81,6 +81,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall;
unsigned int __gen_e_acsl_k;
__e_acsl_store_block((void *)(& buf),(size_t)8);
+ __gen_e_acsl_at = buf;
+ __gen_e_acsl_at_2 = c;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__gen_e_acsl_exists = 0;
__gen_e_acsl_i = 0U;
@@ -162,8 +164,6 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
__gen_e_acsl_forall);
}
- __gen_e_acsl_at_2 = c;
- __gen_e_acsl_at = buf;
__retres = memchr(buf,c,n);
{
int __gen_e_acsl_assumes_value;
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 3b16a3b2a4bfd4764b7766b41ff34b7858988009..fbedbcc8e9c436959dea0e2e4eb241ed4452f867 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -53,14 +53,14 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
- __e_acsl_mpz_t __gen_e_acsl_at_3;
- char *__gen_e_acsl_at_2;
- char *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ __e_acsl_mpz_t __gen_e_acsl_at_2;
+ char *__gen_e_acsl_at;
char *__retres;
{
- unsigned long __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_n;
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
__e_acsl_mpz_t __gen_e_acsl__2;
@@ -86,6 +86,10 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_at = dest;
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -96,11 +100,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"sizeof(char)",
0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"n",0,n);
- __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
__gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gmpz_init(__gen_e_acsl_sub_2);
@@ -253,21 +257,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert(__gen_e_acsl_separated,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_n_2);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_sub_2);
__gmpz_clear(__gen_e_acsl_add);
}
- {
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
- __gmpz_clear(__gen_e_acsl_n_2);
- }
- __gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at = dest;
__retres = strncpy(dest,src,n);
__e_acsl_initialize((void *)dest,n);
{
@@ -298,17 +294,17 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"\\old(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
__gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__gen_e_acsl_sub_4);
@@ -329,7 +325,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_size_6);
__gen_e_acsl_if_6 = __gen_e_acsl_size_6;
}
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at +
1 * 0),
__gen_e_acsl_if_6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
@@ -352,7 +348,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_clear(__gen_e_acsl__9);
__gmpz_clear(__gen_e_acsl_sub_4);
__gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_at_3);
+ __gmpz_clear(__gen_e_acsl_at_2);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
index a6466bb5a4cd839f0ff014b89c0080609e9786e8..213b4d9f74eac564bebdd0059d7b93532bd5c786 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
@@ -40,31 +40,29 @@ void __gen_e_acsl_f(struct X *item)
{
struct X __gen_e_acsl_at_2;
struct X *__gen_e_acsl_at;
- __e_acsl_store_block((void *)(& item),(size_t)8);
{
int __gen_e_acsl_valid_read;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
- {.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"item",
+ __e_acsl_store_block((void *)(& item),(size_t)8);
+ __gen_e_acsl_at = item;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"item",
(void *)item);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,
"sizeof(struct X)",0,sizeof(struct X));
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)item,
sizeof(struct X),
(void *)item,
(void *)(& item));
- __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(item)";
- __gen_e_acsl_assert_data_2.file = "issue-eacsl-139.c";
- __gen_e_acsl_assert_data_2.fct = "f";
- __gen_e_acsl_assert_data_2.line = 9;
- __gen_e_acsl_assert_data_2.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "RTE";
+ __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(item)";
+ __gen_e_acsl_assert_data.file = "issue-eacsl-139.c";
+ __gen_e_acsl_assert_data.fct = "f";
+ __gen_e_acsl_assert_data.line = 9;
+ __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;
f(item);
__e_acsl_delete_block((void *)(& item));
return;
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 3e8074f9776e02e075d00ab8e2519445cb3f1f3b..0c097d165c898e577807b108df86ae1b9f1af4cd 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
@@ -55,15 +55,16 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
FILE * restrict stream)
{
- __e_acsl_mpz_t __gen_e_acsl_at_3;
- void *__gen_e_acsl_at_2;
- size_t __gen_e_acsl_at;
+ size_t __gen_e_acsl_at_3;
+ __e_acsl_mpz_t __gen_e_acsl_at_2;
+ void *__gen_e_acsl_at;
size_t __retres;
{
__e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
__e_acsl_mpz_t __gen_e_acsl_sizeof;
__e_acsl_mpz_t __gen_e_acsl_nmemb;
- __e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl_size_3;
__e_acsl_mpz_t __gen_e_acsl_mul;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
@@ -75,11 +76,16 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_mpz_t __gen_e_acsl_if;
__e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le_2;
- unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl_size_4;
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& stream),(size_t)8);
__e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __gen_e_acsl_at = ptr;
+ __gmpz_init_set_ui(__gen_e_acsl_size,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_3 = nmemb;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"ptr",ptr);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"sizeof(char)",0,
@@ -91,11 +97,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
nmemb);
__gmpz_init_set_ui(__gen_e_acsl_nmemb,nmemb);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"size",0,size);
- __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init_set_ui(__gen_e_acsl_size_3,size);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_nmemb),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_3));
__gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
@@ -114,11 +120,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_init_set(__gen_e_acsl_size,
+ __gmpz_init_set(__gen_e_acsl_size_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
if (__gen_e_acsl_le <= 0) {
__e_acsl_mpz_t __gen_e_acsl__3;
@@ -129,9 +135,9 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
}
else {
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
__gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
}
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -153,9 +159,9 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_2.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_size_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 1 * 0),
- __gen_e_acsl_size_3,ptr,
+ __gen_e_acsl_size_4,ptr,
(void *)(& ptr));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"valid_ptr_block: \\valid((char *)ptr + (0 .. nmemb * size - 1))",
@@ -189,9 +195,10 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl_size_2);
__gmpz_clear(__gen_e_acsl_sizeof);
__gmpz_clear(__gen_e_acsl_nmemb);
- __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl_size_3);
__gmpz_clear(__gen_e_acsl_mul);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
@@ -202,23 +209,14 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_clear(__gen_e_acsl_if);
__gmpz_clear(__gen_e_acsl__4);
}
- {
- __e_acsl_mpz_t __gen_e_acsl_size_7;
- __gmpz_init_set_ui(__gen_e_acsl_size_7,size);
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
- __gmpz_clear(__gen_e_acsl_size_7);
- }
- __gen_e_acsl_at_2 = ptr;
- __gen_e_acsl_at = nmemb;
__retres = fread(ptr,size,nmemb,stream);
{
__e_acsl_mpz_t __gen_e_acsl___retres;
- __e_acsl_mpz_t __gen_e_acsl_size_4;
+ __e_acsl_mpz_t __gen_e_acsl_size_5;
__e_acsl_mpz_t __gen_e_acsl_mul_3;
__e_acsl_mpz_t __gen_e_acsl__5;
int __gen_e_acsl_le_3;
- unsigned long __gen_e_acsl_size_5;
+ unsigned long __gen_e_acsl_size_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"__retres",0,
@@ -226,11 +224,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init_set_ui(__gen_e_acsl___retres,__retres);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
size);
- __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
+ __gmpz_init_set_ui(__gen_e_acsl_size_5,size);
__gmpz_init(__gen_e_acsl_mul_3);
__gmpz_mul(__gen_e_acsl_mul_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl___retres),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
__gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL);
__gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
@@ -243,15 +241,15 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_4.name = "size_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
- __gen_e_acsl_size_5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
- __e_acsl_initialize(ptr,__gen_e_acsl_size_5);
+ __gen_e_acsl_size_6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ __e_acsl_initialize(ptr,__gen_e_acsl_size_6);
__gmpz_clear(__gen_e_acsl___retres);
- __gmpz_clear(__gen_e_acsl_size_4);
+ __gmpz_clear(__gen_e_acsl_size_5);
__gmpz_clear(__gen_e_acsl_mul_3);
__gmpz_clear(__gen_e_acsl__5);
}
{
- __e_acsl_mpz_t __gen_e_acsl_size_6;
+ __e_acsl_mpz_t __gen_e_acsl_size_7;
__e_acsl_mpz_t __gen_e_acsl_sizeof_2;
__e_acsl_mpz_t __gen_e_acsl_result;
__e_acsl_mpz_t __gen_e_acsl_mul_4;
@@ -272,20 +270,20 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"\\result",0,
__retres);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
- "\\old(nmemb)",0,__gen_e_acsl_at);
+ "\\old(nmemb)",0,__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "Postcondition";
__gen_e_acsl_assert_data_5.pred_txt = "\\result <= \\old(nmemb)";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_5.fct = "fread";
__gen_e_acsl_assert_data_5.line = 356;
- __gen_e_acsl_assert_data_5.name = "size_read";
- __e_acsl_assert(__retres <= __gen_e_acsl_at,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert(__retres <= __gen_e_acsl_at_3,
+ & __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(ptr)",
- __gen_e_acsl_at_2);
+ __gen_e_acsl_at);
__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)",
@@ -296,11 +294,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init_set_ui(__gen_e_acsl_result,__retres);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
__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_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
__gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
@@ -319,11 +317,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_mul(__gen_e_acsl_mul_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gmpz_init_set(__gen_e_acsl_size_6,
+ __gmpz_init_set(__gen_e_acsl_size_7,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_5));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
- __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
+ __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
if (__gen_e_acsl_le_4 <= 0) {
__e_acsl_mpz_t __gen_e_acsl__8;
@@ -334,9 +332,9 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
}
else {
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
__gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
}
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
@@ -359,7 +357,7 @@ 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_2 +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at +
1 * 0),
__gen_e_acsl_size_8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
@@ -376,7 +374,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_delete_block((void *)(& stream));
__e_acsl_delete_block((void *)(& ptr));
- __gmpz_clear(__gen_e_acsl_size_6);
+ __gmpz_clear(__gen_e_acsl_size_7);
__gmpz_clear(__gen_e_acsl_sizeof_2);
__gmpz_clear(__gen_e_acsl_result);
__gmpz_clear(__gen_e_acsl_mul_4);
@@ -388,7 +386,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_3);
+ __gmpz_clear(__gen_e_acsl_at_2);
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 7423ad772d31fe769874a2b1c3100c41309c3e8a..4949156576b6bc32719122b4133ae404541d27fc 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -700,13 +700,13 @@ pid_t __gen_e_acsl_fork(void)
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
- int *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ __gen_e_acsl_at = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
stat_loc == (int *)0);
@@ -738,8 +738,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
}
- __gen_e_acsl_at_2 = stat_loc;
- __gen_e_acsl_at = stat_loc;
__retres = waitpid(pid,stat_loc,options);
{
int __gen_e_acsl_or;
@@ -778,11 +776,10 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
else {
int __gen_e_acsl_initialized;
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",
- (void *)__gen_e_acsl_at_2);
+ "\\old(stat_loc)",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at,
sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\initialized(\\old(stat_loc))",0,
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 347be95252fe859c04523ce6b8dc37b9b9d57a5d..835b7da03d0d6d67bd22e2c4d15ab1271bf3ace5 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -241,13 +241,13 @@ pid_t __gen_e_acsl_fork(void)
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
- int *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ __gen_e_acsl_at = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
stat_loc == (int *)0);
@@ -279,8 +279,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
}
- __gen_e_acsl_at_2 = stat_loc;
- __gen_e_acsl_at = stat_loc;
__retres = waitpid(pid,stat_loc,options);
{
int __gen_e_acsl_or;
@@ -319,11 +317,10 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
else {
int __gen_e_acsl_initialized;
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",
- (void *)__gen_e_acsl_at_2);
+ "\\old(stat_loc)",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at,
sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\initialized(\\old(stat_loc))",0,
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 893f81a67edabdfab1dd017663cbb56506f5b5db..4328926452d166452f267138baf6d299c327b6d7 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -675,13 +675,13 @@ pid_t __gen_e_acsl_fork(void)
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
- int *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ __gen_e_acsl_at = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
stat_loc == (int *)0);
@@ -713,8 +713,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
}
- __gen_e_acsl_at_2 = stat_loc;
- __gen_e_acsl_at = stat_loc;
__retres = waitpid(pid,stat_loc,options);
{
int __gen_e_acsl_or;
@@ -753,11 +751,10 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
else {
int __gen_e_acsl_initialized;
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",
- (void *)__gen_e_acsl_at_2);
+ "\\old(stat_loc)",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at,
sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\initialized(\\old(stat_loc))",0,
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 4de9c149b4f9efd18cd257d98779f06afcc729d8..824fb3503a591edf467f21b2832705dc5583a931 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -215,13 +215,13 @@ pid_t __gen_e_acsl_fork(void)
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
- int *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ __gen_e_acsl_at = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
stat_loc == (int *)0);
@@ -253,8 +253,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
}
- __gen_e_acsl_at_2 = stat_loc;
- __gen_e_acsl_at = stat_loc;
__retres = waitpid(pid,stat_loc,options);
{
int __gen_e_acsl_or;
@@ -293,11 +291,10 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
else {
int __gen_e_acsl_initialized;
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",
- (void *)__gen_e_acsl_at_2);
+ "\\old(stat_loc)",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at,
sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\initialized(\\old(stat_loc))",0,
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index 76ac158551f5a3b2cc9eb53a5e30b94dbd22ecf4..65e0a1d60438b62081897d070f4285491869a3cf 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -957,6 +957,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& attrs),(size_t)8);
__e_acsl_store_block((void *)(& mutex),(size_t)8);
+ __gen_e_acsl_at = mutex;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"mutex",
(void *)mutex);
@@ -1008,7 +1009,6 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
- __gen_e_acsl_at = mutex;
__retres = pthread_mutex_init(mutex,attrs);
{
int __gen_e_acsl_and;
@@ -1424,6 +1424,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& attr),(size_t)8);
__e_acsl_store_block((void *)(& cond),(size_t)8);
+ __gen_e_acsl_at = cond;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"cond",
(void *)cond);
@@ -1474,7 +1475,6 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
- __gen_e_acsl_at = cond;
__retres = pthread_cond_init(cond,attr);
{
int __gen_e_acsl_initialized;
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 4b07a6a1478adaa2271cee811f1d544ef83202a4..bad13c318e4c95ae8fec4d83fa2ee7c0f10ebb03 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -639,6 +639,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& attrs),(size_t)8);
__e_acsl_store_block((void *)(& mutex),(size_t)8);
+ __gen_e_acsl_at = mutex;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"mutex",
(void *)mutex);
@@ -690,7 +691,6 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
- __gen_e_acsl_at = mutex;
__retres = pthread_mutex_init(mutex,attrs);
{
int __gen_e_acsl_and;
@@ -1106,6 +1106,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& attr),(size_t)8);
__e_acsl_store_block((void *)(& cond),(size_t)8);
+ __gen_e_acsl_at = cond;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"cond",
(void *)cond);
@@ -1156,7 +1157,6 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
- __gen_e_acsl_at = cond;
__retres = pthread_cond_init(cond,attr);
{
int __gen_e_acsl_initialized;
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 1cf003981e3405f102571e9fdc71d96845960180..a969672a927d878c2756178fede4fa29a88554d7 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
@@ -228,15 +228,12 @@ int main(void)
*/
void __gen_e_acsl_o(void)
{
- 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;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ 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_contract = __e_acsl_contract_init((size_t)4);
__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);
@@ -406,11 +403,6 @@ void __gen_e_acsl_o(void)
& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
}
- __gen_e_acsl_at_5 = Y;
- __gen_e_acsl_at_4 = Y;
- __gen_e_acsl_at_3 = Y;
- __gen_e_acsl_at_2 = Y;
- __gen_e_acsl_at = Y;
o();
{
int __gen_e_acsl_assumes_value_2;
@@ -434,15 +426,14 @@ 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_2);
+ 0,__gen_e_acsl_at);
__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)";
__gen_e_acsl_assert_data_13.file = "function_contract.i";
__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_2,& __gen_e_acsl_assert_data_13);
+ __e_acsl_assert(X == __gen_e_acsl_at,& __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
@@ -452,15 +443,14 @@ 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_3);
+ 0,__gen_e_acsl_at);
__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)";
__gen_e_acsl_assert_data_14.file = "function_contract.i";
__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_3,& __gen_e_acsl_assert_data_14);
+ __e_acsl_assert(X == __gen_e_acsl_at,& __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
@@ -470,15 +460,14 @@ 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_4);
+ 0,__gen_e_acsl_at);
__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)";
__gen_e_acsl_assert_data_15.file = "function_contract.i";
__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_4,& __gen_e_acsl_assert_data_15);
+ __e_acsl_assert(X == __gen_e_acsl_at,& __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
@@ -488,15 +477,14 @@ void __gen_e_acsl_o(void)
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"X",0,X);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"\\old(Y)",
- 0,__gen_e_acsl_at_5);
+ 0,__gen_e_acsl_at);
__gen_e_acsl_assert_data_16.blocking = 1;
__gen_e_acsl_assert_data_16.kind = "Postcondition";
__gen_e_acsl_assert_data_16.pred_txt = "X == \\old(Y)";
__gen_e_acsl_assert_data_16.file = "function_contract.i";
__gen_e_acsl_assert_data_16.fct = "o";
__gen_e_acsl_assert_data_16.line = 114;
- __gen_e_acsl_assert_data_16.name = "even";
- __e_acsl_assert(X == __gen_e_acsl_at_5,& __gen_e_acsl_assert_data_16);
+ __e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_16);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
}
__e_acsl_contract_clean(__gen_e_acsl_contract);
@@ -598,10 +586,11 @@ void __gen_e_acsl_n(void)
*/
void __gen_e_acsl_m(void)
{
- long __gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ long __gen_e_acsl_at;
{
int __gen_e_acsl_and;
+ __gen_e_acsl_at = (long)X;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
X == 7);
@@ -609,7 +598,6 @@ void __gen_e_acsl_m(void)
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
__gen_e_acsl_and);
}
- __gen_e_acsl_at = (long)X;
m();
{
int __gen_e_acsl_assumes_value;
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 b90c677cd6740b1f66f7d8d1ae345b67489ca9dc..c99db3bf2f45ab4efa11c47155678b6581fe419a 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
@@ -112,10 +112,8 @@ int __gen_e_acsl_g(int x)
/*@ ensures \result == (int)(\old(x) - \old(x)); */
int __gen_e_acsl_f(int x)
{
- int __gen_e_acsl_at_2;
long __gen_e_acsl_at;
int __retres;
- __gen_e_acsl_at_2 = x;
__gen_e_acsl_at = (long)x;
__retres = f(x);
{
@@ -124,15 +122,15 @@ int __gen_e_acsl_f(int x)
__retres);
__e_acsl_assert_register_long(& __gen_e_acsl_assert_data,"\\old(x)",0,
__gen_e_acsl_at);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"\\old(x)",0,
- __gen_e_acsl_at_2);
+ __e_acsl_assert_register_long(& __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_2),
+ __e_acsl_assert(__retres == (int)(__gen_e_acsl_at - __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 d541359143b02d5e336ac2d54af2faa7864a2451..20f953076433b4058d4249f0cbbe345bd0ddd782 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
@@ -56,11 +56,13 @@ int main(void)
void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
int h, int i, int j, int k, int l)
{
+ __e_acsl_contract_t *__gen_e_acsl_contract;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_contract_t *__gen_e_acsl_contract;
{
int __gen_e_acsl_assumes_value;
+ __gen_e_acsl_at = b;
+ __gen_e_acsl_at_2 = e;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
__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);
@@ -324,8 +326,6 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
}
- __gen_e_acsl_at_2 = e;
- __gen_e_acsl_at = b;
test(a,b,c,d,e,f,g,h,i,j,k,l);
{
int __gen_e_acsl_assumes_value_2;
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 c154bf096dd6e181a09a9350cf0c8e3b0ed7ab83..8b89a531d8c6f7499c7c29b67f3416e881c3809a 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_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
+ function __e_acsl_assert_register_long: 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/constructs/oracle_dev/printed_data.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log
index 6ae207c797812ba73f9eb18cb2d8153d839a3d57..66e7a3231b68451f7e4400fbf1c8cf1be3b91ba4 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log
@@ -2,98 +2,98 @@ EVERY ASSERTION SHOULD PRINT ITS DATA IN EXECUTION LOG
printed_data.c: In function 'main'
printed_data.c:69: Assertion valid:
\let x = int_bool; \true.
- With values:
+ With values at failure point:
- int_bool: 1
printed_data.c: In function 'main'
printed_data.c:71: Assertion valid:
\let x = int_char; \true.
- With values:
+ With values at failure point:
- int_char: 127
printed_data.c: In function 'main'
printed_data.c:73: Assertion valid:
\let x = int_schar; \true.
- With values:
+ With values at failure point:
- int_schar: 127
printed_data.c: In function 'main'
printed_data.c:75: Assertion valid:
\let x = int_uchar; \true.
- With values:
+ With values at failure point:
- int_uchar: 255
printed_data.c: In function 'main'
printed_data.c:77: Assertion valid:
\let x = int_int; \true.
- With values:
+ With values at failure point:
- int_int: 2147483647
printed_data.c: In function 'main'
printed_data.c:79: Assertion valid:
\let x = int_uint; \true.
- With values:
+ With values at failure point:
- int_uint: 4294967295
printed_data.c: In function 'main'
printed_data.c:81: Assertion valid:
\let x = int_short; \true.
- With values:
+ With values at failure point:
- int_short: 32767
printed_data.c: In function 'main'
printed_data.c:83: Assertion valid:
\let x = int_ushort; \true.
- With values:
+ With values at failure point:
- int_ushort: 65535
printed_data.c: In function 'main'
printed_data.c:85: Assertion valid:
\let x = int_long; \true.
- With values:
+ With values at failure point:
- int_long: 9223372036854775807
printed_data.c: In function 'main'
printed_data.c:87: Assertion valid:
\let x = int_ulong; \true.
- With values:
+ With values at failure point:
- int_ulong: 18446744073709551615
printed_data.c: In function 'main'
printed_data.c:89: Assertion valid:
\let x = int_llong; \true.
- With values:
+ With values at failure point:
- int_llong: 9223372036854775807
printed_data.c: In function 'main'
printed_data.c:91: Assertion valid:
\let x = int_ullong; \true.
- With values:
+ With values at failure point:
- int_ullong: 18446744073709551615
printed_data.c: In function 'main'
printed_data.c:93: Assertion valid:
\let int_mpz = (0x7fffffffffffffffLL * 2ULL + 1ULL) + 1;
int_mpz != 0x7fffffffffffffffLL * 2ULL + 1ULL.
- With values:
+ With values at failure point:
- int_mpz: 18446744073709551616
printed_data.c: In function 'main'
printed_data.c:98: Assertion valid:
\let x = real_float; \true.
- With values:
+ With values at failure point:
- real_float: 3.402823e+38
printed_data.c: In function 'main'
printed_data.c:100: Assertion valid:
\let x = real_double; \true.
- With values:
+ With values at failure point:
- real_double: 1.797693e+308
printed_data.c: In function 'main'
printed_data.c:102: Assertion valid:
\let x = real_ldouble; \true.
- With values:
+ With values at failure point:
- real_ldouble: 1.189731e+4932
printed_data.c: In function 'main'
printed_data.c:104: Assertion valid:
\let real_mpq = 0.1; real_mpq != 1.
- With values:
+ With values at failure point:
- real_mpq: 1/10
printed_data.c: In function 'main'
printed_data.c:109: Assertion valid:
ptr != (void *)0.
- With values:
+ With values at failure point:
- ptr: 0x000000
printed_data.c: In function 'main'
printed_data.c:113: Assertion valid:
array1 != array2.
- With values:
+ With values at failure point:
- array2: <array>
- address: 0x000000
- array1: <array>
@@ -101,83 +101,83 @@ printed_data.c:113: Assertion valid:
printed_data.c: In function 'main'
printed_data.c:118: Assertion valid:
&f != &g.
- With values:
+ With values at failure point:
- &g: 0x000000
- &f: 0x000000
printed_data.c: In function 'main'
printed_data.c:123: Assertion valid:
\let x = struct1; \true.
- With values:
+ With values at failure point:
- struct1: <struct>
printed_data.c: In function 'main'
printed_data.c:128: Assertion valid:
\let x = union1; \true.
- With values:
+ With values at failure point:
- union1: <union>
printed_data.c: In function 'main'
printed_data.c:133: Assertion valid:
\let x = enum_bool; \true.
- With values:
+ With values at failure point:
- enum_bool: <enum> 1
printed_data.c: In function 'main'
printed_data.c:135: Assertion valid:
\let x = enum_char; \true.
- With values:
+ With values at failure point:
- enum_char: <enum> 127
printed_data.c: In function 'main'
printed_data.c:137: Assertion valid:
\let x = enum_schar; \true.
- With values:
+ With values at failure point:
- enum_schar: <enum> 127
printed_data.c: In function 'main'
printed_data.c:139: Assertion valid:
\let x = enum_uchar; \true.
- With values:
+ With values at failure point:
- enum_uchar: <enum> 255
printed_data.c: In function 'main'
printed_data.c:141: Assertion valid:
\let x = enum_int; \true.
- With values:
+ With values at failure point:
- enum_int: <enum> 2147483647
printed_data.c: In function 'main'
printed_data.c:143: Assertion valid:
\let x = enum_uint; \true.
- With values:
+ With values at failure point:
- enum_uint: <enum> 4294967295
printed_data.c: In function 'main'
printed_data.c:145: Assertion valid:
\let x = enum_short; \true.
- With values:
+ With values at failure point:
- enum_short: <enum> 32767
printed_data.c: In function 'main'
printed_data.c:147: Assertion valid:
\let x = enum_ushort; \true.
- With values:
+ With values at failure point:
- enum_ushort: <enum> 65535
printed_data.c: In function 'main'
printed_data.c:149: Assertion valid:
\let x = enum_long; \true.
- With values:
+ With values at failure point:
- enum_long: <enum> 9223372036854775807
printed_data.c: In function 'main'
printed_data.c:151: Assertion valid:
\let x = enum_ulong; \true.
- With values:
+ With values at failure point:
- enum_ulong: <enum> 18446744073709551615
printed_data.c: In function 'main'
printed_data.c:153: Assertion valid:
\let x = enum_llong; \true.
- With values:
+ With values at failure point:
- enum_llong: <enum> 9223372036854775807
printed_data.c: In function 'main'
printed_data.c:155: Assertion valid:
\let x = enum_ullong; \true.
- With values:
+ With values at failure point:
- enum_ullong: <enum> 18446744073709551615
printed_data.c: In function 'main'
printed_data.c:161: Assertion valid:
\let c = a + b; a != b && c == a + b.
- With values:
+ With values at failure point:
- c: 5
- b: 3
- a: 2
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 6f72b40c111a225647a22a74e7662b92ffc9e4d5..f9fa434c6110f921a62e4d548ada67b48be2ffb0 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -154,13 +154,13 @@ pid_t __gen_e_acsl_fork(void)
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
- int *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ __gen_e_acsl_at = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
stat_loc == (int *)0);
@@ -192,8 +192,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
}
- __gen_e_acsl_at_2 = stat_loc;
- __gen_e_acsl_at = stat_loc;
__retres = waitpid(pid,stat_loc,options);
{
int __gen_e_acsl_or;
@@ -232,11 +230,10 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
else {
int __gen_e_acsl_initialized;
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",
- (void *)__gen_e_acsl_at_2);
+ "\\old(stat_loc)",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at,
sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\initialized(\\old(stat_loc))",0,
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 ca8765b8f2703ec3458a2925a0d5fed15bbcd41c..4fcfca74865f84b46d21f3289bb4d2857120ad17 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -735,13 +735,13 @@ void test_specifier_application(char const *allowed, char const *fmt,
*/
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
- char *__gen_e_acsl_at;
unsigned long __gen_e_acsl_strcpy_src_size;
+ char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
- __gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__gen_e_acsl_at = dest;
+ __gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
__e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcpy_src_size;
@@ -830,19 +830,16 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
*/
char *__gen_e_acsl_strchr(char const *s, int c)
{
- char const *__gen_e_acsl_at_4;
- char const *__gen_e_acsl_at_2;
- int __gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int __gen_e_acsl_at_2;
+ char const *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& __retres),(size_t)8);
__e_acsl_store_block((void *)(& s),(size_t)8);
+ __gen_e_acsl_at = s;
+ __gen_e_acsl_at_2 = c;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)3);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)2,1);
- __gen_e_acsl_at_4 = s;
- __gen_e_acsl_at_3 = s;
- __gen_e_acsl_at_2 = s;
- __gen_e_acsl_at = c;
__retres = strchr(s,c);
{
int __gen_e_acsl_assumes_value;
@@ -858,7 +855,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_2,"*\\result",
0,*__retres);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"\\old(c)",0,
- __gen_e_acsl_at);
+ __gen_e_acsl_at_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"&__retres",
@@ -895,7 +892,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
"\\base_addr(\\result)",
__gen_e_acsl_base_addr);
- __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at_2);
+ __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
"\\base_addr(\\old(s))",
__gen_e_acsl_base_addr_2);
@@ -915,8 +912,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/string.h";
__gen_e_acsl_assert_data_2.fct = "strchr";
__gen_e_acsl_assert_data_2.line = 177;
- __gen_e_acsl_assert_data_2.name = "found/result_char";
- __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at),
+ __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at_2),
& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
@@ -953,7 +949,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,
"\\base_addr(\\result)",
__gen_e_acsl_base_addr_3);
- __gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)__gen_e_acsl_at_4);
+ __gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)__gen_e_acsl_at);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,
"\\base_addr(\\old(s))",
__gen_e_acsl_base_addr_4);
@@ -1050,13 +1046,13 @@ pid_t __gen_e_acsl_fork(void)
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
{
- int *__gen_e_acsl_at_2;
- int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ int *__gen_e_acsl_at;
pid_t __retres;
{
int __gen_e_acsl_assumes_value;
__e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ __gen_e_acsl_at = stat_loc;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
stat_loc == (int *)0);
@@ -1088,8 +1084,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
}
- __gen_e_acsl_at_2 = stat_loc;
- __gen_e_acsl_at = stat_loc;
__retres = waitpid(pid,stat_loc,options);
{
int __gen_e_acsl_or;
@@ -1128,11 +1122,10 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
else {
int __gen_e_acsl_initialized;
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,
- "\\old(stat_loc)",
- (void *)__gen_e_acsl_at_2);
+ "\\old(stat_loc)",(void *)__gen_e_acsl_at);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at,
sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\initialized(\\old(stat_loc))",0,
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 06f88c63176372a599aefcc0d772d00e1ebd6a57..c6e10b5b0c544ee932324fbc8badc71f04621b8b 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -55,15 +55,16 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
FILE * restrict stream)
{
- __e_acsl_mpz_t __gen_e_acsl_at_3;
- void *__gen_e_acsl_at_2;
- size_t __gen_e_acsl_at;
+ size_t __gen_e_acsl_at_3;
+ __e_acsl_mpz_t __gen_e_acsl_at_2;
+ void *__gen_e_acsl_at;
size_t __retres;
{
__e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
__e_acsl_mpz_t __gen_e_acsl_sizeof;
__e_acsl_mpz_t __gen_e_acsl_nmemb;
- __e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl_size_3;
__e_acsl_mpz_t __gen_e_acsl_mul;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
@@ -75,11 +76,16 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_mpz_t __gen_e_acsl_if;
__e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le_2;
- unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl_size_4;
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& stream),(size_t)8);
__e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __gen_e_acsl_at = ptr;
+ __gmpz_init_set_ui(__gen_e_acsl_size,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gen_e_acsl_at_3 = nmemb;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"ptr",ptr);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"sizeof(char)",0,
@@ -91,11 +97,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
nmemb);
__gmpz_init_set_ui(__gen_e_acsl_nmemb,nmemb);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"size",0,size);
- __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init_set_ui(__gen_e_acsl_size_3,size);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_nmemb),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_3));
__gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
@@ -114,11 +120,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_init_set(__gen_e_acsl_size,
+ __gmpz_init_set(__gen_e_acsl_size_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
if (__gen_e_acsl_le <= 0) {
__e_acsl_mpz_t __gen_e_acsl__3;
@@ -129,9 +135,9 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
}
else {
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
__gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
}
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -153,9 +159,9 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_2.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_size_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 1 * 0),
- __gen_e_acsl_size_3,ptr,
+ __gen_e_acsl_size_4,ptr,
(void *)(& ptr));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"valid_ptr_block: \\valid((char *)ptr + (0 .. nmemb * size - 1))",
@@ -189,9 +195,10 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl_size_2);
__gmpz_clear(__gen_e_acsl_sizeof);
__gmpz_clear(__gen_e_acsl_nmemb);
- __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl_size_3);
__gmpz_clear(__gen_e_acsl_mul);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
@@ -202,23 +209,14 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_clear(__gen_e_acsl_if);
__gmpz_clear(__gen_e_acsl__4);
}
- {
- __e_acsl_mpz_t __gen_e_acsl_size_7;
- __gmpz_init_set_ui(__gen_e_acsl_size_7,size);
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
- __gmpz_clear(__gen_e_acsl_size_7);
- }
- __gen_e_acsl_at_2 = ptr;
- __gen_e_acsl_at = nmemb;
__retres = fread(ptr,size,nmemb,stream);
{
__e_acsl_mpz_t __gen_e_acsl___retres;
- __e_acsl_mpz_t __gen_e_acsl_size_4;
+ __e_acsl_mpz_t __gen_e_acsl_size_5;
__e_acsl_mpz_t __gen_e_acsl_mul_3;
__e_acsl_mpz_t __gen_e_acsl__5;
int __gen_e_acsl_le_3;
- unsigned long __gen_e_acsl_size_5;
+ unsigned long __gen_e_acsl_size_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"__retres",0,
@@ -226,11 +224,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init_set_ui(__gen_e_acsl___retres,__retres);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
size);
- __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
+ __gmpz_init_set_ui(__gen_e_acsl_size_5,size);
__gmpz_init(__gen_e_acsl_mul_3);
__gmpz_mul(__gen_e_acsl_mul_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl___retres),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
__gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL);
__gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
@@ -243,15 +241,15 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_4.name = "size_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
- __gen_e_acsl_size_5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
- __e_acsl_initialize(ptr,__gen_e_acsl_size_5);
+ __gen_e_acsl_size_6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ __e_acsl_initialize(ptr,__gen_e_acsl_size_6);
__gmpz_clear(__gen_e_acsl___retres);
- __gmpz_clear(__gen_e_acsl_size_4);
+ __gmpz_clear(__gen_e_acsl_size_5);
__gmpz_clear(__gen_e_acsl_mul_3);
__gmpz_clear(__gen_e_acsl__5);
}
{
- __e_acsl_mpz_t __gen_e_acsl_size_6;
+ __e_acsl_mpz_t __gen_e_acsl_size_7;
__e_acsl_mpz_t __gen_e_acsl_sizeof_2;
__e_acsl_mpz_t __gen_e_acsl_result;
__e_acsl_mpz_t __gen_e_acsl_mul_4;
@@ -272,20 +270,20 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"\\result",0,
__retres);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
- "\\old(nmemb)",0,__gen_e_acsl_at);
+ "\\old(nmemb)",0,__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "Postcondition";
__gen_e_acsl_assert_data_5.pred_txt = "\\result <= \\old(nmemb)";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_5.fct = "fread";
__gen_e_acsl_assert_data_5.line = 356;
- __gen_e_acsl_assert_data_5.name = "size_read";
- __e_acsl_assert(__retres <= __gen_e_acsl_at,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert(__retres <= __gen_e_acsl_at_3,
+ & __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\old(ptr)",
- __gen_e_acsl_at_2);
+ __gen_e_acsl_at);
__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)",
@@ -296,11 +294,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_init_set_ui(__gen_e_acsl_result,__retres);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"\\old(size)",
0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
__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_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
__gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
@@ -319,11 +317,11 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gmpz_mul(__gen_e_acsl_mul_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gmpz_init_set(__gen_e_acsl_size_6,
+ __gmpz_init_set(__gen_e_acsl_size_7,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_5));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
- __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
+ __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
if (__gen_e_acsl_le_4 <= 0) {
__e_acsl_mpz_t __gen_e_acsl__8;
@@ -334,9 +332,9 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
}
else {
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
__gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
}
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
@@ -359,7 +357,7 @@ 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_2 +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at +
1 * 0),
__gen_e_acsl_size_8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
@@ -376,7 +374,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_delete_block((void *)(& stream));
__e_acsl_delete_block((void *)(& ptr));
- __gmpz_clear(__gen_e_acsl_size_6);
+ __gmpz_clear(__gen_e_acsl_size_7);
__gmpz_clear(__gen_e_acsl_sizeof_2);
__gmpz_clear(__gen_e_acsl_result);
__gmpz_clear(__gen_e_acsl_mul_4);
@@ -388,7 +386,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_3);
+ __gmpz_clear(__gen_e_acsl_at_2);
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 503f06d93716cae46b39b2d05307255839b19039..5d9daf5e2e76e143f2c8324aba63392160a3723c 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -518,6 +518,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_at = dest;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
@@ -656,7 +657,6 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__gmpz_clear(__gen_e_acsl_sub_2);
__gmpz_clear(__gen_e_acsl_add);
}
- __gen_e_acsl_at = dest;
__retres = memcpy(dest,src,n);
__e_acsl_initialize(dest,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 3b7660e1a3ebbb5388edb7a40c3b91b86d786ae9..23add5a82f4db755be7a6a45211e12d7aa452294 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -149,17 +149,17 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
size_t n)
{
- char *__gen_e_acsl_at;
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;
char *__retres;
__e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_at = dest;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__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;
__gen_e_acsl_strcat_dest_size = __e_acsl_builtin_strlen((char const *)dest);
- __gen_e_acsl_at = dest;
__retres = strncat(dest,src,n);
{
__e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcat_src_size;
@@ -256,15 +256,14 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
*/
char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
{
- char *__gen_e_acsl_at_2;
unsigned long __gen_e_acsl_strcat_dest_size;
unsigned long __gen_e_acsl_strcat_src_size;
+ char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_at = 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);
- __gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at = dest;
__retres = strcat(dest,src);
{
__e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcat_src_size;
@@ -323,16 +322,14 @@ char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,"\\result",
(void *)__retres);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,"\\old(dest)",
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at);
__gen_e_acsl_assert_data_8.blocking = 1;
__gen_e_acsl_assert_data_8.kind = "Postcondition";
__gen_e_acsl_assert_data_8.pred_txt = "\\result == \\old(dest)";
__gen_e_acsl_assert_data_8.file = "FRAMAC_SHARE/libc/string.h";
__gen_e_acsl_assert_data_8.fct = "strcat";
__gen_e_acsl_assert_data_8.line = 434;
- __gen_e_acsl_assert_data_8.name = "result_ptr";
- __e_acsl_assert(__retres == __gen_e_acsl_at_2,
- & __gen_e_acsl_assert_data_8);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
__e_acsl_delete_block((void *)(& dest));
return __retres;
@@ -360,14 +357,14 @@ char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
- __e_acsl_mpz_t __gen_e_acsl_at_3;
- char *__gen_e_acsl_at_2;
- char *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ __e_acsl_mpz_t __gen_e_acsl_at_2;
+ char *__gen_e_acsl_at;
char *__retres;
{
- unsigned long __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_n;
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
__e_acsl_mpz_t __gen_e_acsl__2;
@@ -393,6 +390,10 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_at = dest;
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -403,11 +404,11 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"sizeof(char)",
0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"n",0,n);
- __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
__gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gmpz_init(__gen_e_acsl_sub_2);
@@ -560,21 +561,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert(__gen_e_acsl_separated,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_n_2);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_sub_2);
__gmpz_clear(__gen_e_acsl_add);
}
- {
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
- __gmpz_clear(__gen_e_acsl_n_2);
- }
- __gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at = dest;
__retres = strncpy(dest,src,n);
__e_acsl_initialize((void *)dest,n);
{
@@ -605,17 +598,17 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"\\old(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
__gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__gen_e_acsl_sub_4);
@@ -636,7 +629,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_size_6);
__gen_e_acsl_if_6 = __gen_e_acsl_size_6;
}
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at +
1 * 0),
__gen_e_acsl_if_6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
@@ -659,7 +652,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_clear(__gen_e_acsl__9);
__gmpz_clear(__gen_e_acsl_sub_4);
__gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_at_3);
+ __gmpz_clear(__gen_e_acsl_at_2);
return __retres;
}
}
@@ -678,13 +671,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
*/
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
- char *__gen_e_acsl_at;
unsigned long __gen_e_acsl_strcpy_src_size;
+ char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
- __gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__gen_e_acsl_at = dest;
+ __gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
__e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcpy_src_size;
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 e8c4b325fcc879c6d3eded17655065d74bee84e2..51a87c4aa3be194352b758708cc91416a6e7d18a 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
@@ -835,8 +835,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
long *__gen_e_acsl_at;
{
__e_acsl_mpz_t __gen_e_acsl_size;
- __e_acsl_mpz_t __gen_e_acsl_sizeof;
__e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_size_3;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
__e_acsl_mpz_t __gen_e_acsl__2;
@@ -847,9 +848,13 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_mpz_t __gen_e_acsl_if;
__e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le_2;
- unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl_size_4;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __gen_e_acsl_at = ptr;
+ __gmpz_init_set_ui(__gen_e_acsl_size,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"ptr",
(void *)ptr);
@@ -859,11 +864,11 @@ void __gen_e_acsl_g(long *ptr, size_t size)
8);
__gmpz_init_set_si(__gen_e_acsl_sizeof,8L);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"size",0,size);
- __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init_set_ui(__gen_e_acsl_size_3,size);
__gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gmpz_init(__gen_e_acsl_sub_2);
@@ -878,11 +883,11 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_mul(__gen_e_acsl_mul,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_init_set(__gen_e_acsl_size,
+ __gmpz_init_set(__gen_e_acsl_size_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
if (__gen_e_acsl_le <= 0) {
__e_acsl_mpz_t __gen_e_acsl__3;
@@ -893,9 +898,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
}
else {
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
__gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
}
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
@@ -917,9 +922,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gen_e_acsl_assert_data_2.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_size_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 8 * 0),
- __gen_e_acsl_size_3,(void *)ptr,
+ __gen_e_acsl_size_4,(void *)ptr,
(void *)(& ptr));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
"\\valid(ptr + (0 .. size - 1))",0,
@@ -933,8 +938,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__gmpz_clear(__gen_e_acsl_size);
- __gmpz_clear(__gen_e_acsl_sizeof);
__gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_size_3);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
__gmpz_clear(__gen_e_acsl__2);
@@ -944,17 +950,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl_if);
__gmpz_clear(__gen_e_acsl__4);
}
- {
- __e_acsl_mpz_t __gen_e_acsl_size_5;
- __gmpz_init_set_ui(__gen_e_acsl_size_5,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
- __gmpz_clear(__gen_e_acsl_size_5);
- }
- __gen_e_acsl_at = ptr;
g(ptr,size);
{
- __e_acsl_mpz_t __gen_e_acsl_size_4;
+ __e_acsl_mpz_t __gen_e_acsl_size_5;
__e_acsl_mpz_t __gen_e_acsl_sizeof_2;
__e_acsl_mpz_t __gen_e_acsl__5;
__e_acsl_mpz_t __gen_e_acsl_add_2;
@@ -998,11 +996,11 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_init_set(__gen_e_acsl_size_4,
+ __gmpz_init_set(__gen_e_acsl_size_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
- __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
if (__gen_e_acsl_le_3 <= 0) {
__e_acsl_mpz_t __gen_e_acsl__7;
@@ -1013,9 +1011,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
}
else {
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"size",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
__gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
}
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
@@ -1055,7 +1053,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_assert(! __gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_delete_block((void *)(& ptr));
- __gmpz_clear(__gen_e_acsl_size_4);
+ __gmpz_clear(__gen_e_acsl_size_5);
__gmpz_clear(__gen_e_acsl_sizeof_2);
__gmpz_clear(__gen_e_acsl__5);
__gmpz_clear(__gen_e_acsl_add_2);
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 087ef8783af5880fa77f4caf88562952160d686c..e2ed7604f622ceb4eedcefe8c3fb0c6bf8cf9ad0 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
@@ -66,15 +66,15 @@ int main(void)
*/
struct list *__gen_e_acsl_f(struct list *l)
{
- struct list *__gen_e_acsl_at_2;
- struct list *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ struct list *__gen_e_acsl_at;
struct list *__retres;
__e_acsl_store_block((void *)(& __retres),(size_t)8);
{
int __gen_e_acsl_valid;
int __gen_e_acsl_or;
__e_acsl_store_block((void *)(& l),(size_t)8);
+ __gen_e_acsl_at = l;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
l == (struct list *)0);
@@ -121,8 +121,6 @@ struct list *__gen_e_acsl_f(struct list *l)
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
__gen_e_acsl_or);
}
- __gen_e_acsl_at_2 = l;
- __gen_e_acsl_at = l;
__retres = f(l);
{
int __gen_e_acsl_assumes_value;
@@ -154,15 +152,14 @@ struct list *__gen_e_acsl_f(struct list *l)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"\\result",
(void *)__retres);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"\\old(l)",
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at);
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Postcondition";
__gen_e_acsl_assert_data_3.pred_txt = "\\result == \\old(l)";
__gen_e_acsl_assert_data_3.file = "valid_in_contract.c";
__gen_e_acsl_assert_data_3.fct = "f";
__gen_e_acsl_assert_data_3.line = 18;
- __gen_e_acsl_assert_data_3.name = "B2";
- __e_acsl_assert(__retres == __gen_e_acsl_at_2,
+ __e_acsl_assert(__retres == __gen_e_acsl_at,
& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c
index 54be1732403f281be5d49021696b420322544072..a41ca5d9a3cc3340c93dc7197414b8f54315ba35 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c
@@ -52,14 +52,15 @@ time_t __gen_e_acsl_time(time_t *timer);
*/
time_t __gen_e_acsl_time(time_t *timer)
{
- time_t *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
+ time_t *__gen_e_acsl_at;
time_t __retres;
__e_acsl_store_block((void *)(& __retres),(size_t)8);
{
int __gen_e_acsl_assumes_value;
int __gen_e_acsl_active_bhvrs;
__e_acsl_store_block((void *)(& timer),(size_t)8);
+ __gen_e_acsl_at = timer;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
timer == (time_t *)0);
@@ -122,7 +123,6 @@ time_t __gen_e_acsl_time(time_t *timer)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
}
- __gen_e_acsl_at = timer;
__retres = time(timer);
{
int __gen_e_acsl_assumes_value_2;
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
index f4b8d2b5d868a7b3105d7959e16fec999a8a5ad1..80c12c0821d94d39d64514ea2a9074e5a86e779c 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
@@ -1,5 +1,8 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] e-acsl-functions.c:11: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] e-acsl-functions.c:9: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -9,9 +12,6 @@
[eva:alarm] e-acsl-functions.c:10: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] e-acsl-functions.c:11: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
[eva:alarm] e-acsl-functions.c: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/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
index 1eda3264b1fe3bb63c5d9840eb9515541ac963b7..660f9ccf3bb7eea28c2838193af92523cb57823b 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
@@ -104,89 +104,85 @@ int __gen_e_acsl_f(int *p)
int __gen_e_acsl_at;
int __retres;
{
- int __gen_e_acsl_initialized;
int __gen_e_acsl_valid_read;
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_valid_read_2;
__e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"p",(void *)p);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"sizeof(int)",
0,sizeof(int));
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "\\initialized(p)",0,
- __gen_e_acsl_initialized);
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_assert_data.blocking = 1;
- __gen_e_acsl_assert_data.kind = "Precondition";
- __gen_e_acsl_assert_data.pred_txt = "\\initialized(p)";
+ __gen_e_acsl_assert_data.kind = "RTE";
+ __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(p)";
__gen_e_acsl_assert_data.file = "e-acsl-functions.c";
__gen_e_acsl_assert_data.fct = "f";
- __gen_e_acsl_assert_data.line = 9;
- __e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data);
+ __gen_e_acsl_assert_data.line = 11;
+ __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 = *p;
__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,"*p",0,*p);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"p",(void *)p);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+ "sizeof(int)",0,sizeof(int));
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "\\initialized(p)",0,
+ __gen_e_acsl_initialized);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Precondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\initialized(p)";
+ __gen_e_acsl_assert_data_2.file = "e-acsl-functions.c";
+ __gen_e_acsl_assert_data_2.fct = "f";
+ __gen_e_acsl_assert_data_2.line = 9;
+ __e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"p",(void *)p);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"*p",0,*p);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"p",(void *)p);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "RTE";
+ __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(p)";
+ __gen_e_acsl_assert_data_4.file = "e-acsl-functions.c";
+ __gen_e_acsl_assert_data_4.fct = "f";
+ __gen_e_acsl_assert_data_4.line = 10;
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__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(p)";
+ __gen_e_acsl_assert_data_3.kind = "Precondition";
+ __gen_e_acsl_assert_data_3.pred_txt = "*p == 0";
__gen_e_acsl_assert_data_3.file = "e-acsl-functions.c";
__gen_e_acsl_assert_data_3.fct = "f";
__gen_e_acsl_assert_data_3.line = 10;
- __gen_e_acsl_assert_data_3.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert(*p == 0,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
- __gen_e_acsl_assert_data_2.blocking = 1;
- __gen_e_acsl_assert_data_2.kind = "Precondition";
- __gen_e_acsl_assert_data_2.pred_txt = "*p == 0";
- __gen_e_acsl_assert_data_2.file = "e-acsl-functions.c";
- __gen_e_acsl_assert_data_2.fct = "f";
- __gen_e_acsl_assert_data_2.line = 10;
- __e_acsl_assert(*p == 0,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
+ __retres = f(p);
{
- int __gen_e_acsl_valid_read_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"p",(void *)p);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,
- "sizeof(int)",0,sizeof(int));
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"\\result",0,
+ __retres);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"\\old(*p)",0,
+ __gen_e_acsl_at);
__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(p)";
+ __gen_e_acsl_assert_data_5.kind = "Postcondition";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\result == \\old(*p)";
__gen_e_acsl_assert_data_5.file = "e-acsl-functions.c";
__gen_e_acsl_assert_data_5.fct = "f";
__gen_e_acsl_assert_data_5.line = 11;
- __gen_e_acsl_assert_data_5.name = "mem_access";
- __e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- __gen_e_acsl_at = *p;
- }
- __retres = f(p);
- {
- __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,"\\result",0,
- __retres);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"\\old(*p)",0,
- __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 = "\\result == \\old(*p)";
- __gen_e_acsl_assert_data_4.file = "e-acsl-functions.c";
- __gen_e_acsl_assert_data_4.fct = "f";
- __gen_e_acsl_assert_data_4.line = 11;
- __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_4);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__e_acsl_delete_block((void *)(& p));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log
index 3d675389171b08485dc090f06aa577328c2b2cc2..907aef209f7b7ad84611e61258a73f453f69faec 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log
@@ -2,5 +2,5 @@ e-acsl-external-print-value.c: In function 'main'
e-acsl-external-print-value.c:7: Error: Assertion failed:
The failing predicate is:
\let x = value; \false.
- With values:
+ With values at failure point:
- custom print for value
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 9b0a94e0efa8152db7d793b74336d09789904632..9d5021eb070b12afaed8be77738575b0bb47f472 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
@@ -738,11 +738,11 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
void *__retres;
__e_acsl_store_block((void *)(& s),(size_t)8);
__e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
+ __gen_e_acsl_at = s;
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& s),0U);
__e_acsl_temporal_memset(s,c,n);
- __gen_e_acsl_at = s;
__retres = memset(s,c,n);
__e_acsl_initialize(s,n);
{
@@ -812,6 +812,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_store_block((void *)(& dest),(size_t)8);
__e_acsl_temporal_pull_parameter((void *)(& dest),0U,8UL);
__e_acsl_temporal_pull_parameter((void *)(& src),1U,8UL);
+ __gen_e_acsl_at = dest;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
@@ -955,7 +956,6 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__gmpz_clear(__gen_e_acsl_sub_2);
__gmpz_clear(__gen_e_acsl_add);
}
- __gen_e_acsl_at = dest;
__retres = memcpy(dest,src,n);
__e_acsl_initialize(dest,n);
{