From 231a5e872f15c8f8679506c9962fb1bafe4c1626 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 5 Jul 2018 16:35:27 +0200
Subject: [PATCH] update oracles
---
.../tests/bts/oracle/bts1304.err.oracle | 0
.../tests/bts/oracle/bts1307.err.oracle | 0
.../tests/bts/oracle/bts1324.err.oracle | 0
.../tests/bts/oracle/bts1326.err.oracle | 0
.../tests/bts/oracle/bts1390.err.oracle | 0
.../tests/bts/oracle/bts1395.err.oracle | 0
.../tests/bts/oracle/bts1398.err.oracle | 0
.../tests/bts/oracle/bts1399.err.oracle | 0
.../tests/bts/oracle/bts1478.err.oracle | 0
.../tests/bts/oracle/bts1700.err.oracle | 0
.../tests/bts/oracle/bts1717.err.oracle | 0
.../tests/bts/oracle/bts1718.err.oracle | 0
.../tests/bts/oracle/bts1740.err.oracle | 0
.../tests/bts/oracle/bts1837.err.oracle | 0
.../tests/bts/oracle/bts2191.err.oracle | 0
.../tests/bts/oracle/bts2192.err.oracle | 0
.../tests/bts/oracle/bts2231.err.oracle | 0
.../tests/bts/oracle/bts2252.err.oracle | 0
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 18 ++--
.../e-acsl/tests/bts/oracle/gen_bts1324.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 2 +-
.../tests/format/oracle/fprintf.err.oracle | 0
.../full-mmodel/oracle/addrOf.0.err.oracle | 0
.../full-mmodel/oracle/addrOf.1.err.oracle | 0
.../tests/gmp/oracle/arith.0.err.oracle | 0
.../tests/gmp/oracle/arith.1.err.oracle | 0
.../tests/gmp/oracle/array.0.err.oracle | 0
.../tests/gmp/oracle/array.1.err.oracle | 0
.../e-acsl/tests/gmp/oracle/at.0.err.oracle | 0
.../e-acsl/tests/gmp/oracle/at.1.err.oracle | 0
.../e-acsl/tests/gmp/oracle/cast.0.err.oracle | 0
.../e-acsl/tests/gmp/oracle/cast.1.err.oracle | 0
.../tests/gmp/oracle/comparison.0.err.oracle | 0
.../tests/gmp/oracle/comparison.1.err.oracle | 0
src/plugins/e-acsl/tests/gmp/oracle/gen_at.c | 14 +--
src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c | 86 ++++++++++---------
.../gmp/oracle/integer_constant.0.err.oracle | 0
.../gmp/oracle/integer_constant.1.err.oracle | 0
.../e-acsl/tests/gmp/oracle/let.0.err.oracle | 0
.../e-acsl/tests/gmp/oracle/let.1.err.oracle | 0
.../tests/gmp/oracle/longlong.0.err.oracle | 0
.../tests/gmp/oracle/longlong.1.err.oracle | 0
.../e-acsl/tests/gmp/oracle/not.0.err.oracle | 0
.../e-acsl/tests/gmp/oracle/not.1.err.oracle | 0
.../tests/gmp/oracle/quantif.0.err.oracle | 0
.../tests/gmp/oracle/quantif.1.err.oracle | 0
.../tests/no-main/oracle/empty.err.oracle | 0
.../tests/reject/oracle/quantif.err.oracle | 0
.../tests/runtime/oracle/addrOf.err.oracle | 0
.../tests/runtime/oracle/alias.err.oracle | 0
.../tests/runtime/oracle/base_addr.err.oracle | 0
.../runtime/oracle/block_length.err.oracle | 0
.../runtime/oracle/block_valid.err.oracle | 0
.../runtime/oracle/bypassed_var.err.oracle | 0
.../tests/runtime/oracle/call.err.oracle | 0
.../oracle/compound_initializers.err.oracle | 0
.../runtime/oracle/ctype_macros.err.oracle | 0
.../runtime/oracle/early_exit.err.oracle | 0
.../tests/runtime/oracle/errno.err.oracle | 0
.../tests/runtime/oracle/false.err.oracle | 0
.../tests/runtime/oracle/freeable.err.oracle | 0
.../oracle/function_contract.err.oracle | 0
.../runtime/oracle/gen_function_contract.c | 4 +-
.../e-acsl/tests/runtime/oracle/gen_goto.c | 2 +-
.../tests/runtime/oracle/gen_linear_search.c | 64 +++++++-------
.../tests/runtime/oracle/ghost.err.oracle | 0
.../tests/runtime/oracle/goto.err.oracle | 0
.../runtime/oracle/hidden_malloc.err.oracle | 0
.../tests/runtime/oracle/init.err.oracle | 0
.../runtime/oracle/init_function.err.oracle | 0
.../runtime/oracle/initialized.err.oracle | 0
.../tests/runtime/oracle/invariant.err.oracle | 0
.../runtime/oracle/labeled_stmt.err.oracle | 0
.../tests/runtime/oracle/lazy.err.oracle | 0
.../runtime/oracle/linear_search.err.oracle | 0
.../runtime/oracle/literal_string.err.oracle | 0
.../runtime/oracle/local_goto.err.oracle | 0
.../runtime/oracle/local_init.err.oracle | 0
.../tests/runtime/oracle/localvar.err.oracle | 0
.../tests/runtime/oracle/loop.err.oracle | 0
.../tests/runtime/oracle/mainargs.err.oracle | 0
.../tests/runtime/oracle/memalign.err.oracle | 0
.../tests/runtime/oracle/memsize.err.oracle | 0
.../oracle/nested_code_annot.err.oracle | 0
.../tests/runtime/oracle/null.err.oracle | 0
.../tests/runtime/oracle/offset.err.oracle | 0
.../runtime/oracle/other_constants.err.oracle | 0
.../tests/runtime/oracle/ptr.err.oracle | 0
.../tests/runtime/oracle/ptr_init.err.oracle | 0
.../tests/runtime/oracle/result.err.oracle | 0
.../tests/runtime/oracle/sizeof.err.oracle | 0
.../tests/runtime/oracle/stdout.err.oracle | 0
.../runtime/oracle/stmt_contract.err.oracle | 0
.../tests/runtime/oracle/true.err.oracle | 0
.../tests/runtime/oracle/typedef.err.oracle | 0
.../tests/runtime/oracle/valid.err.oracle | 0
.../runtime/oracle/valid_alias.err.oracle | 0
.../oracle/valid_in_contract.err.oracle | 0
.../tests/runtime/oracle/vector.err.oracle | 0
.../tests/runtime/oracle/vla.err.oracle | 0
.../temporal/oracle/t_addr-by-val.err.oracle | 0
.../tests/temporal/oracle/t_args.err.oracle | 0
.../tests/temporal/oracle/t_array.err.oracle | 0
.../tests/temporal/oracle/t_char.err.oracle | 0
.../tests/temporal/oracle/t_darray.err.oracle | 0
.../temporal/oracle/t_dpointer.err.oracle | 0
.../tests/temporal/oracle/t_fptr.err.oracle | 0
.../temporal/oracle/t_fun_lib.err.oracle | 0
.../temporal/oracle/t_fun_ptr.err.oracle | 0
.../tests/temporal/oracle/t_getenv.err.oracle | 0
.../temporal/oracle/t_global_init.err.oracle | 0
.../tests/temporal/oracle/t_labels.err.oracle | 0
.../temporal/oracle/t_lit_string.err.oracle | 0
.../temporal/oracle/t_local_init.err.oracle | 0
.../temporal/oracle/t_malloc-asan.err.oracle | 0
.../tests/temporal/oracle/t_malloc.err.oracle | 0
.../tests/temporal/oracle/t_memcpy.err.oracle | 0
.../tests/temporal/oracle/t_scope.err.oracle | 0
.../tests/temporal/oracle/t_struct.err.oracle | 0
.../tests/temporal/oracle/t_while.err.oracle | 0
122 files changed, 101 insertions(+), 97 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1324.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1326.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1395.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1398.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1399.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1478.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1717.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1718.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1740.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2191.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2252.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle/fprintf.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/arith.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/arith.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/array.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/array.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/at.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/at.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/cast.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/cast.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/comparison.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/comparison.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/let.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/let.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/longlong.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/longlong.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/not.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/not.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/quantif.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/quantif.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/no-main/oracle/empty.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/reject/oracle/quantif.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/addrOf.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/alias.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/base_addr.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/block_length.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/block_valid.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/call.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/early_exit.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/errno.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/false.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/freeable.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/function_contract.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/ghost.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/goto.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/init.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/init_function.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/initialized.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/invariant.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/lazy.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/linear_search.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/literal_string.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/local_goto.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/local_init.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/localvar.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/loop.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/mainargs.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/memalign.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/memsize.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/null.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/offset.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/other_constants.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/ptr.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/ptr_init.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/result.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/sizeof.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/stdout.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/true.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/typedef.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/valid.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/valid_alias.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/vector.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/vla.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_args.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_array.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_char.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_darray.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_fptr.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_getenv.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_global_init.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_labels.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_local_init.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_malloc.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_scope.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_struct.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_while.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
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 5cc5c43ca9c..61b2754b678 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -94,6 +94,12 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
float *__gen_e_acsl_at_3;
float *__gen_e_acsl_at_2;
float *__gen_e_acsl_at;
+ __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;
{
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
@@ -116,12 +122,6 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mtmin_out)",19);
}
- __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_valid_read;
@@ -207,6 +207,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
float *__gen_e_acsl_at_3;
float *__gen_e_acsl_at_2;
float *__gen_e_acsl_at;
+ __gen_e_acsl_at_3 = Mwmax;
+ __gen_e_acsl_at_2 = Mtmax_in;
+ __gen_e_acsl_at = Mtmax_out;
{
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
@@ -229,9 +232,6 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mtmax_out)",7);
}
- __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_valid_read;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 2e7190ee172..87651cb3b0b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -52,7 +52,6 @@ int __gen_e_acsl_sorted(int *t, int n)
{
int __gen_e_acsl_at;
int __retres;
- __e_acsl_store_block((void *)(& t),(size_t)8);
{
int __gen_e_acsl_forall;
int __gen_e_acsl_i;
@@ -90,6 +89,7 @@ int __gen_e_acsl_sorted(int *t, int n)
e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_forall;
}
+ __e_acsl_store_block((void *)(& t),(size_t)8);
__retres = sorted(t,n);
{
int __gen_e_acsl_implies;
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 5913ad8605b..eb485b81c3d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -56,14 +56,14 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
ArrayInt *__gen_e_acsl_at_3;
ArrayInt *__gen_e_acsl_at_2;
int *__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;
+ __e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
{
int __gen_e_acsl_valid_read;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 9836ce0227b..f64d25acbeb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -31,7 +31,7 @@ int main(void)
__retres = 0;
goto return_label;
lbl_1: __e_acsl_full_init((void *)(& p));
- p = & a;
+ p = & a;
goto lbl_2;
return_label:
__e_acsl_delete_block((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index 69dde9e9d50..a209e7ff761 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -31,7 +31,7 @@ int main(void)
__retres = 0;
goto return_label;
lbl_1: __e_acsl_full_init((void *)(& p));
- p = & a;
+ p = & a;
goto lbl_2;
return_label:
__e_acsl_delete_block((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.err.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.err.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.err.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index 381bd425ddd..e7eb39cd366 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -127,12 +127,14 @@ int main(void)
__e_acsl_full_init((void *)(& x));
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;
/*@ assert x ≡ 0; */
- __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
- 43);
+ {
+ __gen_e_acsl_at_3 = (long)x;
+ __gen_e_acsl_at_2 = x + 1L;
+ __gen_e_acsl_at = x;
+ __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",
+ (char *)"x == 0",43);
+ }
__e_acsl_full_init((void *)(& x));
x = 1;
__e_acsl_full_init((void *)(& x));
@@ -161,8 +163,8 @@ int __gen_e_acsl_h(int x)
int __gen_e_acsl_at;
int __retres;
__e_acsl_store_block((void *)(& __retres),(size_t)4);
- __e_acsl_store_block((void *)(& x),(size_t)4);
__gen_e_acsl_at = x;
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__retres = h(x);
__e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
(char *)"h",(char *)"\\result == \\old(x)",35);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 6a5a2734e0f..1883d05a943 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -197,49 +197,51 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- {
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_add);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
- __gmpz_clear(__gen_e_acsl_x_2);
- }
/*@ assert x ≡ 0; */
{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"x == 0",43);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set(__gen_e_acsl_at,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+ __gmpz_init_set(__gen_e_acsl_at,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
+ __gmpz_clear(__gen_e_acsl_x_2);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
+ (char *)"main",(char *)"x == 0",43);
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_);
+ }
}
__e_acsl_full_init((void *)(& x));
x = 1;
@@ -301,7 +303,6 @@ int __gen_e_acsl_h(int x)
__e_acsl_mpz_t __gen_e_acsl_at;
int __retres;
__e_acsl_store_block((void *)(& __retres),(size_t)4);
- __e_acsl_store_block((void *)(& x),(size_t)4);
{
__e_acsl_mpz_t __gen_e_acsl_x;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
@@ -309,6 +310,7 @@ int __gen_e_acsl_h(int x)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
__gmpz_clear(__gen_e_acsl_x);
}
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__retres = h(x);
{
__e_acsl_mpz_t __gen_e_acsl_result;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/no-main/oracle/empty.err.oracle b/src/plugins/e-acsl/tests/no-main/oracle/empty.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/reject/oracle/quantif.err.oracle b/src/plugins/e-acsl/tests/reject/oracle/quantif.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/alias.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/alias.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_length.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/call.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/call.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/errno.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/false.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/false.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/freeable.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/freeable.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/function_contract.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/function_contract.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index 729e010573f..089ede314fd 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -155,12 +155,12 @@ void __gen_e_acsl_n(void)
{
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
+ __gen_e_acsl_at_2 = X == 5;
+ __gen_e_acsl_at = X == 7;
__e_acsl_assert(X > 0,(char *)"Precondition",(char *)"n",(char *)"X > 0",
65);
__e_acsl_assert(X < 10,(char *)"Precondition",(char *)"n",(char *)"X < 10",
66);
- __gen_e_acsl_at_2 = X == 5;
- __gen_e_acsl_at = X == 7;
n();
{
int __gen_e_acsl_implies;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
index b3efb49daf0..55fddf6c648 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
@@ -18,7 +18,7 @@ int main(void)
__e_acsl_store_block((void *)(& b),(size_t)8);
goto _LOR;
_LOR: __e_acsl_full_init((void *)(& b));
- b = & a;
+ b = & a;
if (a) goto _LOR;
/*@ assert \initialized(b); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 671194ec177..4a0739f91f2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -138,38 +138,6 @@ int __gen_e_acsl_search(int elt)
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
int __retres;
- {
- int __gen_e_acsl_forall;
- int __gen_e_acsl_i;
- __gen_e_acsl_forall = 1;
- __gen_e_acsl_i = 0;
- while (1) {
- if (__gen_e_acsl_i < 9) ; else break;
- __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,(char *)"RTE",
- (char *)"search",
- (char *)"index_bound: (int)(__gen_e_acsl_i + 1) < 10",
- 7);
- __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),(char *)"RTE",
- (char *)"search",
- (char *)"index_bound: 0 <= (int)(__gen_e_acsl_i + 1)",
- 7);
- __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_i < 10",7);
- __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_i",7);
- if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ;
- else {
- __gen_e_acsl_forall = 0;
- goto e_acsl_end_loop3;
- }
- __gen_e_acsl_i ++;
- }
- e_acsl_end_loop3: ;
- __e_acsl_assert(__gen_e_acsl_forall,(char *)"Precondition",
- (char *)"search",
- (char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]",
- 7);
- }
{
int __gen_e_acsl_forall_2;
int __gen_e_acsl_j_2;
@@ -212,6 +180,38 @@ int __gen_e_acsl_search(int elt)
e_acsl_end_loop4: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
}
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_i;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_i = 0;
+ while (1) {
+ if (__gen_e_acsl_i < 9) ; else break;
+ __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,(char *)"RTE",
+ (char *)"search",
+ (char *)"index_bound: (int)(__gen_e_acsl_i + 1) < 10",
+ 7);
+ __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),(char *)"RTE",
+ (char *)"search",
+ (char *)"index_bound: 0 <= (int)(__gen_e_acsl_i + 1)",
+ 7);
+ __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_i < 10",7);
+ __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_i",7);
+ if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop3;
+ }
+ __gen_e_acsl_i ++;
+ }
+ e_acsl_end_loop3: ;
+ __e_acsl_assert(__gen_e_acsl_forall,(char *)"Precondition",
+ (char *)"search",
+ (char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]",
+ 7);
+ }
__retres = search(elt);
{
int __gen_e_acsl_implies;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ghost.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ghost.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/goto.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/goto.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init_function.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init_function.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/invariant.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/invariant.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/lazy.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/lazy.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_init.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_init.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/localvar.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/localvar.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/loop.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/loop.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memsize.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/null.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/null.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/offset.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/offset.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/other_constants.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/other_constants.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/result.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/result.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/sizeof.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/sizeof.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stdout.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stdout.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/true.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/true.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/typedef.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/typedef.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vla.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vla.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_args.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_args.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_array.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_array.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_char.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_char.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_darray.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_darray.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fptr.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fptr.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_global_init.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_global_init.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_labels.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_labels.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_local_init.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_local_init.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_struct.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_struct.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_while.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_while.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
--
GitLab