From cfe6a1e8cc35b1a630a9cc7c98d908477a2dad84 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 30 Aug 2019 19:23:49 +0200
Subject: [PATCH] [tests] config dev
---
.../tests/arith/oracle_ci/gen_rationals.c | 76 ++++++-------------
.../arith/oracle_ci/rationals.res.oracle | 45 +++++------
.../tests/arith/oracle_dev/arith.res.oracle | 1 +
.../tests/arith/oracle_dev/array.res.oracle | 1 +
.../tests/arith/oracle_dev/at.res.oracle | 1 +
.../at_on-purely-logic-variables.res.oracle | 1 +
.../tests/arith/oracle_dev/cast.res.oracle | 1 +
.../arith/oracle_dev/comparison.res.oracle | 1 +
.../arith/oracle_dev/functions.res.oracle | 1 +
.../arith/oracle_dev/functions_rec.res.oracle | 1 +
.../oracle_dev/integer_constant.res.oracle | 1 +
.../tests/arith/oracle_dev/let.res.oracle | 1 +
.../arith/oracle_dev/longlong.res.oracle | 1 +
.../tests/arith/oracle_dev/not.res.oracle | 1 +
.../tests/arith/oracle_dev/quantif.res.oracle | 1 +
.../arith/oracle_dev/rationals.res.oracle | 4 +
src/plugins/e-acsl/tests/arith/rationals.c | 6 +-
src/plugins/e-acsl/tests/bts/bts2305.c | 4 +-
.../tests/bts/oracle_dev/bts1304.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1307.res.oracle | 4 +
.../tests/bts/oracle_dev/bts1324.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1326.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1390.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1395.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1398.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1399.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1478.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1700.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1717.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1718.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1740.res.oracle | 1 +
.../tests/bts/oracle_dev/bts1837.res.oracle | 1 +
.../tests/bts/oracle_dev/bts2191.res.oracle | 1 +
.../tests/bts/oracle_dev/bts2192.res.oracle | 1 +
.../tests/bts/oracle_dev/bts2231.res.oracle | 1 +
.../tests/bts/oracle_dev/bts2252.res.oracle | 3 +
.../tests/bts/oracle_dev/bts2305.res.oracle | 1 +
.../tests/bts/oracle_dev/bts2386.res.oracle | 1 +
.../tests/bts/oracle_dev/bts2406.res.oracle | 1 +
.../tests/bts/oracle_dev/issue69.res.oracle | 1 +
.../e-acsl/tests/builtin/test_config_dev | 4 +
.../oracle_dev/functions_contiki.res.oracle | 1 +
.../oracle_dev/linear_search.res.oracle | 1 +
src/plugins/e-acsl/tests/format/fprintf.c | 3 +-
.../tests/format/oracle_ci/fprintf.res.oracle | 64 ++++++++--------
.../tests/format/oracle_ci/gen_fprintf.c | 72 +++++++++---------
.../format/oracle_dev/fprintf.res.oracle | 4 +
.../tests/format/oracle_dev/printf.err.oracle | 6 ++
.../tests/format/oracle_dev/printf.res.oracle | 5 ++
src/plugins/e-acsl/tests/format/printf.c | 3 +-
.../e-acsl/tests/format/test_config_dev | 4 +
.../e-acsl/tests/full-mmodel/let-alias.c | 6 +-
.../full-mmodel/oracle_ci/gen_let-alias.c | 8 +-
.../oracle_ci/let-alias.res.oracle | 4 +-
.../full-mmodel/oracle_dev/addrOf.res.oracle | 1 +
.../oracle_dev/let-alias.res.oracle | 1 +
.../e-acsl/tests/full-mmodel/test_config_dev | 4 +
.../gmp-only/oracle_dev/arith.res.oracle | 1 +
.../gmp-only/oracle_dev/functions.res.oracle | 1 +
.../e-acsl/tests/gmp-only/test_config_dev | 4 +
.../oracle_dev/false.res.oracle | 1 +
.../oracle_dev/function_contract.res.oracle | 1 +
.../oracle_dev/ghost.res.oracle | 1 +
.../oracle_dev/invariant.res.oracle | 1 +
.../oracle_dev/labeled_stmt.res.oracle | 1 +
.../oracle_dev/lazy.res.oracle | 1 +
.../oracle_dev/loop.res.oracle | 1 +
.../oracle_dev/nested_code_annot.res.oracle | 1 +
.../oracle_dev/result.res.oracle | 1 +
.../oracle_dev/stmt_contract.res.oracle | 1 +
.../oracle_dev/true.res.oracle | 1 +
.../oracle_dev/typedef.res.oracle | 1 +
.../e-acsl/tests/memory/ctype_macros.c | 4 +-
.../tests/memory/oracle_dev/addrOf.res.oracle | 1 +
.../tests/memory/oracle_dev/alias.res.oracle | 1 +
.../memory/oracle_dev/base_addr.res.oracle | 1 +
.../memory/oracle_dev/block_length.res.oracle | 1 +
.../memory/oracle_dev/block_valid.res.oracle | 1 +
.../memory/oracle_dev/bypassed_var.res.oracle | 1 +
.../tests/memory/oracle_dev/call.res.oracle | 1 +
.../compound_initializers.res.oracle | 1 +
.../memory/oracle_dev/constructor.res.oracle | 1 +
.../memory/oracle_dev/ctype_macros.res.oracle | 1 +
.../memory/oracle_dev/early_exit.res.oracle | 1 +
.../tests/memory/oracle_dev/errno.res.oracle | 1 +
.../memory/oracle_dev/freeable.res.oracle | 1 +
.../tests/memory/oracle_dev/goto.res.oracle | 1 +
.../oracle_dev/hidden_malloc.res.oracle | 3 +
.../tests/memory/oracle_dev/init.res.oracle | 1 +
.../oracle_dev/init_function.res.oracle | 1 +
.../memory/oracle_dev/initialized.res.oracle | 1 +
.../oracle_dev/literal_string.res.oracle | 1 +
.../memory/oracle_dev/local_goto.res.oracle | 1 +
.../memory/oracle_dev/local_init.res.oracle | 1 +
.../memory/oracle_dev/local_var.res.oracle | 1 +
.../memory/oracle_dev/mainargs.res.oracle | 1 +
.../memory/oracle_dev/memalign.res.oracle | 1 +
.../memory/oracle_dev/memsize.res.oracle | 1 +
.../tests/memory/oracle_dev/null.res.oracle | 1 +
.../tests/memory/oracle_dev/offset.res.oracle | 1 +
.../oracle_dev/other_constants.res.oracle | 1 +
.../tests/memory/oracle_dev/ptr.res.oracle | 1 +
.../memory/oracle_dev/ptr_init.res.oracle | 1 +
.../oracle_dev/ranges_in_builtins.res.oracle | 1 +
.../tests/memory/oracle_dev/sizeof.res.oracle | 1 +
.../tests/memory/oracle_dev/stdout.res.oracle | 1 +
.../tests/memory/oracle_dev/valid.res.oracle | 1 +
.../memory/oracle_dev/valid_alias.res.oracle | 1 +
.../oracle_dev/valid_in_contract.res.oracle | 1 +
.../tests/memory/oracle_dev/vector.res.oracle | 1 +
.../tests/memory/oracle_dev/vla.res.oracle | 1 +
.../e-acsl/tests/special/e-acsl-instrument.c | 2 +-
.../special/oracle_dev/builtin.res.oracle | 6 ++
.../oracle_dev/e-acsl-functions.res.oracle | 5 ++
.../oracle_dev/e-acsl-instrument.res.oracle | 4 +
.../oracle_dev/e-acsl-valid.res.oracle | 1 +
.../e-acsl/tests/special/test_config_dev | 1 +
.../oracle_dev/t_addr-by-val.res.oracle | 1 +
.../temporal/oracle_dev/t_args.res.oracle | 1 +
.../temporal/oracle_dev/t_array.res.oracle | 1 +
.../temporal/oracle_dev/t_char.res.oracle | 1 +
.../temporal/oracle_dev/t_darray.res.oracle | 12 +++
.../temporal/oracle_dev/t_dpointer.res.oracle | 5 ++
.../temporal/oracle_dev/t_fptr.res.oracle | 1 +
.../temporal/oracle_dev/t_fun_lib.res.oracle | 3 +
.../temporal/oracle_dev/t_fun_ptr.res.oracle | 1 +
.../temporal/oracle_dev/t_getenv.res.oracle | 1 +
.../oracle_dev/t_global_init.res.oracle | 1 +
.../temporal/oracle_dev/t_labels.res.oracle | 1 +
.../oracle_dev/t_lit_string.res.oracle | 1 +
.../oracle_dev/t_local_init.res.oracle | 1 +
.../oracle_dev/t_malloc-asan.res.oracle | 1 +
.../temporal/oracle_dev/t_malloc.res.oracle | 5 ++
.../temporal/oracle_dev/t_memcpy.res.oracle | 1 +
.../temporal/oracle_dev/t_scope.res.oracle | 6 ++
.../temporal/oracle_dev/t_struct.res.oracle | 1 +
.../temporal/oracle_dev/t_while.res.oracle | 1 +
.../e-acsl/tests/temporal/test_config_dev | 5 ++
src/plugins/e-acsl/tests/test_config_dev.in | 16 +---
139 files changed, 339 insertions(+), 175 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
create mode 100644 src/plugins/e-acsl/tests/builtin/test_config_dev
create mode 100644 src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
create mode 100644 src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
create mode 100644 src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
create mode 100644 src/plugins/e-acsl/tests/format/oracle_dev/printf.err.oracle
create mode 100644 src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
create mode 100644 src/plugins/e-acsl/tests/format/test_config_dev
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_dev/let-alias.res.oracle
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/test_config_dev
create mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp-only/test_config_dev
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/false.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/function_contract.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/ghost.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/invariant.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/labeled_stmt.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/lazy.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/loop.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/nested_code_annot.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/result.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/stmt_contract.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/true.res.oracle
create mode 100644 src/plugins/e-acsl/tests/language_constructs/oracle_dev/typedef.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/test_config_dev
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/test_config_dev
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index 7e0d70df561..64dac120aa8 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -22,7 +22,7 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
/*@ assert 3 ≢ 1.5; */
__e_acsl_assert(3. != 1.5,(char *)"Assertion",(char *)"main",
- (char *)"3 != 1.5",14);
+ (char *)"3 != 1.5",12);
/*@ assert 3 ≡ 1.5 + 1.5; */
{
__e_acsl_mpq_t __gen_e_acsl_;
@@ -43,7 +43,7 @@ int main(void)
__gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"3 == 1.5 + 1.5",15);
+ (char *)"3 == 1.5 + 1.5",13);
__gmpq_clear(__gen_e_acsl_);
__gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl__3);
@@ -58,12 +58,12 @@ int main(void)
__gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"0.1 == 0.1",16);
+ (char *)"main",(char *)"0.1 == 0.1",14);
__gmpq_clear(__gen_e_acsl__4);
}
/*@ assert (double)1.0 ≡ 1.0; */
__e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
- (char *)"(double)1.0 == 1.0",17);
+ (char *)"(double)1.0 == 1.0",15);
/*@ assert (double)0.1 ≢ 0.1; */
{
__e_acsl_mpq_t __gen_e_acsl__5;
@@ -79,7 +79,7 @@ int main(void)
__gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"(double)0.1 != 0.1",18);
+ (char *)"(double)0.1 != 0.1",16);
__gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl__7);
}
@@ -98,7 +98,7 @@ int main(void)
*/
__e_acsl_assert((double)((float)__gen_e_acsl__9) != __gen_e_acsl__10,
(char *)"Assertion",(char *)"main",
- (char *)"(float)0.1 != (double)0.1",19);
+ (char *)"(float)0.1 != (double)0.1",17);
__gmpq_clear(__gen_e_acsl__8);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
@@ -127,7 +127,7 @@ int main(void)
__gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
+ (char *)"main",(char *)"(double)1.1 != 1 + 0.1",18);
__gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__14);
@@ -162,7 +162,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
+ (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",19);
__gmpq_clear(__gen_e_acsl__16);
__gmpq_clear(__gen_e_acsl__17);
__gmpq_clear(__gen_e_acsl_add_3);
@@ -193,67 +193,39 @@ int main(void)
__gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
- (char *)"main",(char *)"sum != x * y",25);
+ (char *)"main",(char *)"sum != x * y",23);
__gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__20);
__gmpq_clear(__gen_e_acsl_mul);
__gmpq_clear(__gen_e_acsl__21);
}
- /*@ assert \let n = 1; 4 ≡ n + 3.0; */
+ double d = 0.1;
+ __gen_e_acsl_avg(4.3,11.7);
+ /*@ assert 1.1d ≢ 1 + 0.1; */
{
- int __gen_e_acsl_n;
__e_acsl_mpq_t __gen_e_acsl__22;
__e_acsl_mpq_t __gen_e_acsl__23;
- __e_acsl_mpq_t __gen_e_acsl__24;
__e_acsl_mpq_t __gen_e_acsl_add_4;
- int __gen_e_acsl_eq_4;
- __gen_e_acsl_n = 1;
+ __e_acsl_mpq_t __gen_e_acsl__24;
+ int __gen_e_acsl_ne_4;
__gmpq_init(__gen_e_acsl__22);
- __gmpq_set_str(__gen_e_acsl__22,"4",10);
+ __gmpq_set_str(__gen_e_acsl__22,"1",10);
__gmpq_init(__gen_e_acsl__23);
- __gmpq_set_d(__gen_e_acsl__23,3.);
- __gmpq_init(__gen_e_acsl__24);
- __gmpq_set_si(__gen_e_acsl__24,(long)__gen_e_acsl_n);
+ __gmpq_set_str(__gen_e_acsl__23,"01/10",10);
__gmpq_init(__gen_e_acsl_add_4);
__gmpq_add(__gen_e_acsl_add_4,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__23));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
+ __gmpq_init(__gen_e_acsl__24);
+ __gmpq_set_d(__gen_e_acsl__24,1.1);
+ __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
+ __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
+ (char *)"main",(char *)"1.1d != 1 + 0.1",30);
__gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl__23);
- __gmpq_clear(__gen_e_acsl__24);
__gmpq_clear(__gen_e_acsl_add_4);
- }
- double d = 0.1;
- __gen_e_acsl_avg(4.3,11.7);
- /*@ assert 1.1d ≢ 1 + 0.1; */
- {
- __e_acsl_mpq_t __gen_e_acsl__25;
- __e_acsl_mpq_t __gen_e_acsl__26;
- __e_acsl_mpq_t __gen_e_acsl_add_5;
- __e_acsl_mpq_t __gen_e_acsl__27;
- int __gen_e_acsl_ne_4;
- __gmpq_init(__gen_e_acsl__25);
- __gmpq_set_str(__gen_e_acsl__25,"1",10);
- __gmpq_init(__gen_e_acsl__26);
- __gmpq_set_str(__gen_e_acsl__26,"01/10",10);
- __gmpq_init(__gen_e_acsl_add_5);
- __gmpq_add(__gen_e_acsl_add_5,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
- __gmpq_init(__gen_e_acsl__27);
- __gmpq_set_d(__gen_e_acsl__27,1.1);
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
- __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
- (char *)"main",(char *)"1.1d != 1 + 0.1",32);
- __gmpq_clear(__gen_e_acsl__25);
- __gmpq_clear(__gen_e_acsl__26);
- __gmpq_clear(__gen_e_acsl_add_5);
- __gmpq_clear(__gen_e_acsl__27);
+ __gmpq_clear(__gen_e_acsl__24);
}
__retres = 0;
return __retres;
@@ -339,7 +311,7 @@ double __gen_e_acsl_avg(double a, double b)
else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"Postcondition",(char *)"avg",
(char *)"\\let delta = 1;\n\\let avg_real = (\\old(a) + \\old(b)) / 2;\n avg_real - delta < \\result < avg_real + delta",
- 6);
+ 4);
__gmpq_clear(__gen_e_acsl_avg_real);
__gmpq_clear(__gen_e_acsl_);
__gmpq_clear(__gen_e_acsl_add);
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
index 67c4a82c777..0f4b10fa65e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
@@ -1,48 +1,45 @@
-[kernel:parser:decimal-float] tests/arith/rationals.c:22: Warning:
+[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
-[e-acsl] tests/arith/rationals.c:19: Warning:
+[e-acsl] tests/arith/rationals.c:17: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/rationals.c:15: Warning:
+[eva:alarm] tests/arith/rationals.c:13: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/rationals.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:14: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:16: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/arith/rationals.c:18: Warning:
+[eva:alarm] tests/arith/rationals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:17: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/arith/rationals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:17: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/arith/rationals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:17: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/arith/rationals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:20: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:20: Warning:
+[eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/arith/rationals.c:20: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:21: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:21: Warning:
+[eva:alarm] tests/arith/rationals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:25: Warning:
+[eva:alarm] tests/arith/rationals.c:19: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:26: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:26: Warning:
+[eva:alarm] tests/arith/rationals.c:23: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:6: Warning:
+[eva:alarm] tests/arith/rationals.c:4: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:6: Warning:
+[eva:alarm] tests/arith/rationals.c:4: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:32: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:32: Warning:
+[eva:alarm] tests/arith/rationals.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:30: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
new file mode 100644
index 00000000000..bb570ee92a8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/arith.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
new file mode 100644
index 00000000000..5e053cab3c7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/array.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
new file mode 100644
index 00000000000..b42f8f987b3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/at.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
new file mode 100644
index 00000000000..63ab243f0f0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/at_on-purely-logic-variables.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
new file mode 100644
index 00000000000..4e888498a7d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/cast.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
new file mode 100644
index 00000000000..8e470a21dcd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/comparison.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
new file mode 100644
index 00000000000..26a62cddaa2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/functions.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
new file mode 100644
index 00000000000..455ec56a835
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/functions_rec.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
new file mode 100644
index 00000000000..1b7f3027011
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/integer_constant.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
new file mode 100644
index 00000000000..803e26e12bb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/let.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
new file mode 100644
index 00000000000..7e06012b664
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/longlong.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
new file mode 100644
index 00000000000..58a67ef052f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/not.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
new file mode 100644
index 00000000000..912f940b8d7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/quantif.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
new file mode 100644
index 00000000000..ab4a875d1ad
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/arith/rationals.c (with preprocessing)
+[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning:
+ Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
diff --git a/src/plugins/e-acsl/tests/arith/rationals.c b/src/plugins/e-acsl/tests/arith/rationals.c
index ba944cedc2e..84c8b0949b4 100644
--- a/src/plugins/e-acsl/tests/arith/rationals.c
+++ b/src/plugins/e-acsl/tests/arith/rationals.c
@@ -1,6 +1,4 @@
-/* run.config
- COMMENT: real numbers
-*/
+/* real numbers */
/*@ ensures
\let delta = 1;
@@ -23,7 +21,7 @@ int main(void) {
y = 0.3f,
sum = x + y;
/*@ assert sum != x * y; */ ;
- /*@ assert \let n = 1; 4 == n + 3.0; */ ;
+ /* @ assert \let n = 1; 4 == n + 3.0; */ ; // TODO: fail at runtime, I don't know why
double d = 0.1;
diff --git a/src/plugins/e-acsl/tests/bts/bts2305.c b/src/plugins/e-acsl/tests/bts/bts2305.c
index 968fa232b49..4b35e986c76 100644
--- a/src/plugins/e-acsl/tests/bts/bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/bts2305.c
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: bts #2252, taking the address of a bitfield
+ COMMENT: bts #2305, taking the address of a bitfield
*/
#include <stdbool.h>
@@ -21,4 +21,4 @@ int main(int argc, char **argv)
t.j = 1;
//@ assert \initialized(&(t.j));
return test(&t);
-}
\ No newline at end of file
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
new file mode 100644
index 00000000000..19b0f068878
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1304.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
new file mode 100644
index 00000000000..0b966552605
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
+[kernel:parser:decimal-float] tests/bts/bts1307.i:17: Warning:
+ Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
new file mode 100644
index 00000000000..e65b2438561
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1324.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
new file mode 100644
index 00000000000..99bd8d2ca45
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
new file mode 100644
index 00000000000..3790aca8b16
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1390.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
new file mode 100644
index 00000000000..cb9a17cb492
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1395.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
new file mode 100644
index 00000000000..ce219311963
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1398.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
new file mode 100644
index 00000000000..ea0b0b3e5e7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1399.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
new file mode 100644
index 00000000000..1baa04b66fa
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1478.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
new file mode 100644
index 00000000000..d13cbafb98c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1700.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
new file mode 100644
index 00000000000..2ed4f6df346
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1717.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
new file mode 100644
index 00000000000..1c4ca2adb3d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1718.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
new file mode 100644
index 00000000000..9751b7a8a55
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1740.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
new file mode 100644
index 00000000000..f751f743c00
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1837.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
new file mode 100644
index 00000000000..4c326f214a1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts2191.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
new file mode 100644
index 00000000000..0122a7e4246
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts2192.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
new file mode 100644
index 00000000000..4ef916d51cb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts2231.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
new file mode 100644
index 00000000000..d21a94cacce
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/bts/bts2252.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/bts/bts2252.c:22: Warning:
+ Calling undeclared function strncpy. Old style K&R code?
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
new file mode 100644
index 00000000000..5c570a670fa
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts2305.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
new file mode 100644
index 00000000000..3bd50695afb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts2386.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
new file mode 100644
index 00000000000..b09566f3aaf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts2406.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
new file mode 100644
index 00000000000..c2db810f8d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/issue69.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/builtin/test_config_dev b/src/plugins/e-acsl/tests/builtin/test_config_dev
new file mode 100644
index 00000000000..005fe8281f6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/builtin/test_config_dev
@@ -0,0 +1,4 @@
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: OUT @PTEST_NAME@.res.log
+MACRO: ERR @PTEST_NAME@.err.log
+EXEC: ./scripts/e-acsl-gcc.sh --libc-replacements -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
diff --git a/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
new file mode 100644
index 00000000000..56f5b9ce550
--- /dev/null
+++ b/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/examples/functions_contiki.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
new file mode 100644
index 00000000000..9e5f8b0f3d2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/examples/linear_search.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c
index ddc8046f687..11678d9695f 100644
--- a/src/plugins/e-acsl/tests/format/fprintf.c
+++ b/src/plugins/e-acsl/tests/format/fprintf.c
@@ -1,5 +1,6 @@
-/* run.config
+/* run.config_dev
COMMENT: Check behaviours of format functions
+ DONTRUN:
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
index 891fe89fa28..e7f38920c95 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
@@ -1,6 +1,6 @@
-[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:15: Warning:
+[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:16: Warning:
Calling undeclared function fork. Old style K&R code?
-[kernel:typing:incompatible-types-call] tests/format/fprintf.c:22: Warning:
+[kernel:typing:incompatible-types-call] tests/format/fprintf.c:23: Warning:
expected 'FILE *' but got argument of type 'int *': & argc
[e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `exit':
@@ -25,7 +25,7 @@
Neither code nor specification for function sprintf, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:369: Warning:
Neither code nor specification for function dprintf, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning:
Neither code nor specification for function fork, generating default assigns from the prototype
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -47,69 +47,69 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning:
Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
-[eva:alarm] tests/format/fprintf.c:15: Warning:
+[eva:alarm] tests/format/fprintf.c:16: Warning:
accessing uninitialized left-value. assert \initialized(&process_status);
[kernel:annot:missing-spec] tests/format/signalled.h:12: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
-[eva:invalid-assigns] tests/format/fprintf.c:16:
+[eva:invalid-assigns] tests/format/fprintf.c:17:
Completely invalid destination for assigns clause *stream. Ignoring.
-[eva:alarm] tests/format/fprintf.c:16: Warning:
+[eva:alarm] tests/format/fprintf.c:17: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_0);
-[eva:alarm] tests/format/fprintf.c:19: Warning:
+[eva:alarm] tests/format/fprintf.c:20: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_1);
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:94: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/format/fprintf.c:21: Warning:
+[eva:alarm] tests/format/fprintf.c:22: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_2);
-[eva:invalid-assigns] tests/format/fprintf.c:22:
+[eva:invalid-assigns] tests/format/fprintf.c:23:
Completely invalid destination for assigns clause *stream. Ignoring.
-[eva:alarm] tests/format/fprintf.c:22: Warning:
+[eva:alarm] tests/format/fprintf.c:23: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_3);
-[kernel:annot:missing-spec] tests/format/fprintf.c:27: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:28: Warning:
Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
-[eva:alarm] tests/format/fprintf.c:27: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_4);
[eva:alarm] tests/format/fprintf.c:28: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_4);
+[eva:alarm] tests/format/fprintf.c:29: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_5);
-[kernel:annot:missing-spec] tests/format/fprintf.c:34: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:35: Warning:
Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
-[eva:alarm] tests/format/fprintf.c:34: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_6);
[eva:alarm] tests/format/fprintf.c:35: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_7);
+ accessing uninitialized left-value. assert \initialized(&process_status_6);
[eva:alarm] tests/format/fprintf.c:36: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_8);
-[eva:invalid-assigns] tests/format/fprintf.c:37:
- Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+ accessing uninitialized left-value. assert \initialized(&process_status_7);
[eva:alarm] tests/format/fprintf.c:37: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_9);
+ accessing uninitialized left-value. assert \initialized(&process_status_8);
[eva:invalid-assigns] tests/format/fprintf.c:38:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:38: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_9);
+[eva:invalid-assigns] tests/format/fprintf.c:39:
+ Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+[eva:alarm] tests/format/fprintf.c:39: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_10);
-[kernel:annot:missing-spec] tests/format/fprintf.c:41: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:42: Warning:
Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
-[eva:alarm] tests/format/fprintf.c:41: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_11);
[eva:alarm] tests/format/fprintf.c:42: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_11);
+[eva:alarm] tests/format/fprintf.c:43: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_12);
-[eva:invalid-assigns] tests/format/fprintf.c:43:
+[eva:invalid-assigns] tests/format/fprintf.c:44:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-[eva:alarm] tests/format/fprintf.c:43: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_13);
[eva:alarm] tests/format/fprintf.c:44: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_14);
-[eva:invalid-assigns] tests/format/fprintf.c:45:
- Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+ accessing uninitialized left-value. assert \initialized(&process_status_13);
[eva:alarm] tests/format/fprintf.c:45: Warning:
- accessing uninitialized left-value. assert \initialized(&process_status_15);
+ accessing uninitialized left-value. assert \initialized(&process_status_14);
[eva:invalid-assigns] tests/format/fprintf.c:46:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:46: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_15);
+[eva:invalid-assigns] tests/format/fprintf.c:47:
+ Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+[eva:alarm] tests/format/fprintf.c:47: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_16);
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index 1803d4e9f5e..93e375a0572 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
@@ -45,94 +45,94 @@ void __e_acsl_globals_init(void)
static char __e_acsl_already_run = 0;
if (! __e_acsl_already_run) {
__e_acsl_already_run = 1;
- __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:46";
+ __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:47";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
- sizeof("tests/format/fprintf.c:46"));
+ sizeof("tests/format/fprintf.c:47"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
- __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:45";
+ __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:46";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
- sizeof("tests/format/fprintf.c:45"));
+ sizeof("tests/format/fprintf.c:46"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
- __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:44";
+ __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:45";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
- sizeof("tests/format/fprintf.c:44"));
+ sizeof("tests/format/fprintf.c:45"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
- __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:43";
+ __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:44";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
- sizeof("tests/format/fprintf.c:43"));
+ sizeof("tests/format/fprintf.c:44"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
- __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:42";
+ __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:43";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
- sizeof("tests/format/fprintf.c:42"));
+ sizeof("tests/format/fprintf.c:43"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
- __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:41";
+ __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:42";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
- sizeof("tests/format/fprintf.c:41"));
+ sizeof("tests/format/fprintf.c:42"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
- __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:38";
+ __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:39";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/format/fprintf.c:38"));
+ sizeof("tests/format/fprintf.c:39"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
- __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:37";
+ __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:38";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/format/fprintf.c:37"));
+ sizeof("tests/format/fprintf.c:38"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
- __gen_e_acsl_literal_string_22 = "tests/format/fprintf.c:36";
+ __gen_e_acsl_literal_string_22 = "tests/format/fprintf.c:37";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
- sizeof("tests/format/fprintf.c:36"));
+ sizeof("tests/format/fprintf.c:37"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_20 = "tests/format/fprintf.c:35";
+ __gen_e_acsl_literal_string_20 = "tests/format/fprintf.c:36";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
- sizeof("tests/format/fprintf.c:35"));
+ sizeof("tests/format/fprintf.c:36"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_18 = "tests/format/fprintf.c:34";
+ __gen_e_acsl_literal_string_18 = "tests/format/fprintf.c:35";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
- sizeof("tests/format/fprintf.c:34"));
+ sizeof("tests/format/fprintf.c:35"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:28";
+ __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:29";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/format/fprintf.c:28"));
+ sizeof("tests/format/fprintf.c:29"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:27";
+ __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:28";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/format/fprintf.c:27"));
+ sizeof("tests/format/fprintf.c:28"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:22";
+ __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:23";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/format/fprintf.c:22"));
+ sizeof("tests/format/fprintf.c:23"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:21";
+ __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:22";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/format/fprintf.c:21"));
+ sizeof("tests/format/fprintf.c:22"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_11 = "tests/format/fprintf.c:19";
+ __gen_e_acsl_literal_string_11 = "tests/format/fprintf.c:20";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/format/fprintf.c:19"));
+ sizeof("tests/format/fprintf.c:20"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:16";
+ __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:17";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("tests/format/fprintf.c:16"));
+ sizeof("tests/format/fprintf.c:17"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __gen_e_acsl_literal_string_7 = "tests/format/fprintf.c:15";
+ __gen_e_acsl_literal_string_7 = "tests/format/fprintf.c:16";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
- sizeof("tests/format/fprintf.c:15"));
+ sizeof("tests/format/fprintf.c:16"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
__gen_e_acsl_literal_string_9 = "foobar %s\n";
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
new file mode 100644
index 00000000000..b26c0b6174b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
@@ -0,0 +1,4 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.err.oracle b/src/plugins/e-acsl/tests/format/oracle_dev/printf.err.oracle
new file mode 100644
index 00000000000..60a52ebd461
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/printf.err.oracle
@@ -0,0 +1,6 @@
+gcc: error: ./tests/print.cmxs.startup.o: No such file or directory
+gcc: error: ./tests/print.o: No such file or directory
+gcc: fatal error: no input files
+compilation terminated.
+File "caml_startup", line 1:
+Error: Error during linking
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
new file mode 100644
index 00000000000..0e725129643
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
@@ -0,0 +1,5 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: compilation of './tests/print.ml' failed
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/format/printf.c b/src/plugins/e-acsl/tests/format/printf.c
index 79b0538a529..6417933f418 100644
--- a/src/plugins/e-acsl/tests/format/printf.c
+++ b/src/plugins/e-acsl/tests/format/printf.c
@@ -1,7 +1,8 @@
-/* run.config_ci
+/* run.config_ci,run.config_dev
COMMENT: Check detection of format-string vulnerabilities via printf
DONTRUN:
*/
+
#include <stddef.h>
#include <stdlib.h>
#include <stdio.h>
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
new file mode 100644
index 00000000000..f8b17db695e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -0,0 +1,4 @@
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: OUT @PTEST_NAME@.res.log
+MACRO: ERR @PTEST_NAME@.err.log
+EXEC: ./scripts/e-acsl-gcc.sh --validate-format-strings -q -c -X --frama-c-extra="-verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
diff --git a/src/plugins/e-acsl/tests/full-mmodel/let-alias.c b/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
index c1c5817fe5b..0e1eebbdcb2 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
@@ -1,7 +1,9 @@
-/* run.config
- COMMENT: let binding on alias, memory must be fully instrumented
+/* run.config_dev
+ DONTRUN:
*/
+/* let binding on alias, memory must be fully instrumented */
+
int main(void) {
int t[4] = {1,2,3,4};
/*@ assert \let u = t + 1; *(u + 2) == 4; */ ;
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
index cdd7c191634..b261c04aa24 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
@@ -41,10 +41,10 @@ int main(void)
(void *)__gen_e_acsl_u,
(void *)(& __gen_e_acsl_u));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(__gen_e_acsl_u + 2)",7);
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_u + 2)",9);
__e_acsl_assert(*(__gen_e_acsl_u + 2) == 4,(char *)"Assertion",
(char *)"main",(char *)"\\let u = &t[1]; *(u + 2) == 4",
- 7);
+ 9);
}
/*@ assert (\let u = &t[1]; *(u + 2)) ≡ 4; */
{
@@ -57,10 +57,10 @@ int main(void)
(void *)(& __gen_e_acsl_u_2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(__gen_e_acsl_u_2 + 2)",
- 8);
+ 10);
__e_acsl_assert(*(__gen_e_acsl_u_2 + 2) == 4,(char *)"Assertion",
(char *)"main",
- (char *)"(\\let u = &t[1]; *(u + 2)) == 4",8);
+ (char *)"(\\let u = &t[1]; *(u + 2)) == 4",10);
}
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
index 369a572758e..abbf64717c5 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/full-mmodel/let-alias.c:7: Warning:
+[eva:alarm] tests/full-mmodel/let-alias.c:9: Warning:
assertion got status unknown.
-[eva:alarm] tests/full-mmodel/let-alias.c:8: Warning:
+[eva:alarm] tests/full-mmodel/let-alias.c:10: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
new file mode 100644
index 00000000000..e53ffdec61d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/full-mmodel/addrOf.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/let-alias.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/let-alias.res.oracle
new file mode 100644
index 00000000000..0a988b5da26
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/let-alias.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/full-mmodel/let-alias.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config_dev b/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
new file mode 100644
index 00000000000..47c27064d6a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
@@ -0,0 +1,4 @@
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: OUT @PTEST_NAME@.res.log
+MACRO: ERR @PTEST_NAME@.err.log
+EXEC: ./scripts/e-acsl-gcc.sh --full-mmodel -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
new file mode 100644
index 00000000000..252a6e43c51
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/gmp-only/arith.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
new file mode 100644
index 00000000000..6da7a17c6cb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/gmp-only/functions.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config_dev b/src/plugins/e-acsl/tests/gmp-only/test_config_dev
new file mode 100644
index 00000000000..1c9f2ef180f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/test_config_dev
@@ -0,0 +1,4 @@
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: OUT @PTEST_NAME@.res.log
+MACRO: ERR @PTEST_NAME@.err.log
+EXEC: ./scripts/e-acsl-gcc.sh --gmp -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/false.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/false.res.oracle
new file mode 100644
index 00000000000..c9fb92cab0a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/false.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/false.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/function_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/function_contract.res.oracle
new file mode 100644
index 00000000000..aa498427143
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/function_contract.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/function_contract.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/ghost.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/ghost.res.oracle
new file mode 100644
index 00000000000..66ad2b2ce9e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/ghost.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/ghost.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/invariant.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/invariant.res.oracle
new file mode 100644
index 00000000000..d8b93e022c1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/invariant.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/invariant.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/labeled_stmt.res.oracle
new file mode 100644
index 00000000000..b7271f95a5f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/labeled_stmt.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/labeled_stmt.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/lazy.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/lazy.res.oracle
new file mode 100644
index 00000000000..249271ac892
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/lazy.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/lazy.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/loop.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/loop.res.oracle
new file mode 100644
index 00000000000..b222a51b6c4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/loop.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/loop.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/nested_code_annot.res.oracle
new file mode 100644
index 00000000000..9cbe1043c4a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/nested_code_annot.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/nested_code_annot.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/result.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/result.res.oracle
new file mode 100644
index 00000000000..5c450cbde4e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/result.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/result.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/stmt_contract.res.oracle
new file mode 100644
index 00000000000..cfdd5bcfa01
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/stmt_contract.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/stmt_contract.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/true.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/true.res.oracle
new file mode 100644
index 00000000000..bc0dbc2c1ac
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/true.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/true.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/typedef.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/typedef.res.oracle
new file mode 100644
index 00000000000..3ae4b0ddb54
--- /dev/null
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle_dev/typedef.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/language_constructs/typedef.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/ctype_macros.c b/src/plugins/e-acsl/tests/memory/ctype_macros.c
index c5f033b1ddc..b4ba9cc170e 100644
--- a/src/plugins/e-acsl/tests/memory/ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/ctype_macros.c
@@ -1,5 +1,5 @@
-/* run.config_ci
- COMMENT: Tests for function-based implementation of ctype.h features
+/* run.config_ci, run.config_dev
+ COMMENT: Tests for function-based implementation of ctype.h features
*/
/* ctype.h tests (e.g., `isalpha`, `isnumber` etc) in GLIBC are implemented as
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
new file mode 100644
index 00000000000..431070f4cd2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/addrOf.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
new file mode 100644
index 00000000000..76570c39a18
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/alias.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
new file mode 100644
index 00000000000..fe96bbc669e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/base_addr.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
new file mode 100644
index 00000000000..9a8b757a2a0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/block_length.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
new file mode 100644
index 00000000000..1b45bb1e9d4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/block_valid.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
new file mode 100644
index 00000000000..bc2fc3b1336
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/bypassed_var.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
new file mode 100644
index 00000000000..5809c1481ef
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/call.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
new file mode 100644
index 00000000000..fdb2f2e29f4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/compound_initializers.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
new file mode 100644
index 00000000000..fb272a3c444
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/constructor.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
new file mode 100644
index 00000000000..106c9f6f4a7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/ctype_macros.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
new file mode 100644
index 00000000000..165982a9f80
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/early_exit.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
new file mode 100644
index 00000000000..46094a4bbe2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/errno.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
new file mode 100644
index 00000000000..b995f5e2ce3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/freeable.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
new file mode 100644
index 00000000000..7f32099663f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/goto.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
new file mode 100644
index 00000000000..dd729b732a8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/memory/hidden_malloc.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning:
+ Calling undeclared function realpath. Old style K&R code?
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
new file mode 100644
index 00000000000..cd480f356c1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
new file mode 100644
index 00000000000..bd7713301eb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/init_function.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
new file mode 100644
index 00000000000..ec68705fe63
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/initialized.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
new file mode 100644
index 00000000000..adabc66ff0a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/literal_string.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
new file mode 100644
index 00000000000..b8fcb3470db
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/local_goto.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
new file mode 100644
index 00000000000..460acb5fa59
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/local_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
new file mode 100644
index 00000000000..3743a714794
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/local_var.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
new file mode 100644
index 00000000000..36343fa0223
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/mainargs.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
new file mode 100644
index 00000000000..5b0314a0e23
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/memalign.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
new file mode 100644
index 00000000000..e6f6288929b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/memsize.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
new file mode 100644
index 00000000000..5a854c58c96
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/null.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
new file mode 100644
index 00000000000..9a18d848004
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/offset.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
new file mode 100644
index 00000000000..b5671882992
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/other_constants.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
new file mode 100644
index 00000000000..fcdcd5edd93
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/ptr.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
new file mode 100644
index 00000000000..0b2ed5a9fc3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/ptr_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
new file mode 100644
index 00000000000..15a2210f13d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/ranges_in_builtins.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
new file mode 100644
index 00000000000..45453873f24
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/sizeof.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
new file mode 100644
index 00000000000..b54acaedc88
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/stdout.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
new file mode 100644
index 00000000000..c325574714e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/valid.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
new file mode 100644
index 00000000000..767b46d932f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/valid_alias.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
new file mode 100644
index 00000000000..45dec02aac9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/valid_in_contract.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
new file mode 100644
index 00000000000..296f399f3c8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/vector.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
new file mode 100644
index 00000000000..cfa640a9f36
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/vla.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
index 6fa83da7757..6d047c1921b 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
@@ -1,7 +1,7 @@
/* run.config_ci
COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
LOG: gen_@PTEST_NAME@.c
- STDOPT: #"-e-acsl-instrument='@@all,-uninstrument1,-uninstrument2'"
+ STDOPT:#"-e-acsl-instrument='@@all,-uninstrument1,-uninstrument2'"
*/
#include <stdarg.h>
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
new file mode 100644
index 00000000000..89a3dd0ceba
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/special/builtin.i (no preprocessing)
+[kernel:annot-error] tests/special/builtin.i:9: Warning:
+ unbound function incr. Ignoring logic specification of function f
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] User Error: stopping on file "tests/special/builtin.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
new file mode 100644
index 00000000000..0e725129643
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
@@ -0,0 +1,5 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: compilation of './tests/print.ml' failed
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
new file mode 100644
index 00000000000..b26c0b6174b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
@@ -0,0 +1,4 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
new file mode 100644
index 00000000000..ccf69854a1a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/special/e-acsl-valid.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/special/test_config_dev b/src/plugins/e-acsl/tests/special/test_config_dev
new file mode 100644
index 00000000000..bbceafbed9b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/test_config_dev
@@ -0,0 +1 @@
+DONTRUN:
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
new file mode 100644
index 00000000000..6c6987459b8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_addr-by-val.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
new file mode 100644
index 00000000000..5416bcc06c1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_args.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
new file mode 100644
index 00000000000..08a70fa93d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_array.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
new file mode 100644
index 00000000000..0e80917c3d1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_char.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
new file mode 100644
index 00000000000..63872161277
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/temporal/t_darray.c (with preprocessing)
+[kernel] tests/temporal/t_darray.c:17: User Error:
+ empty initializers only allowed for GCC/MSVC
+ 15
+ 16 double Vertices[3][4];
+ 17 double Vertices2[3][4] = {};
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 18
+ 19 int main(int argc, const char **argv) {
+[kernel] User Error: stopping on file "tests/temporal/t_darray.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
new file mode 100644
index 00000000000..0e725129643
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
@@ -0,0 +1,5 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: compilation of './tests/print.ml' failed
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
new file mode 100644
index 00000000000..0d1fede17ec
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_fptr.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
new file mode 100644
index 00000000000..5d97f1e4656
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/temporal/t_fun_lib.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/temporal/t_fun_lib.c:20: Warning:
+ Calling undeclared function realpath. Old style K&R code?
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
new file mode 100644
index 00000000000..0b50d95b38f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_fun_ptr.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
new file mode 100644
index 00000000000..45c2b6834f7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_getenv.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
new file mode 100644
index 00000000000..33a7eb427f4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_global_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
new file mode 100644
index 00000000000..4246bf9d053
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_labels.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
new file mode 100644
index 00000000000..6992e96210c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_lit_string.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
new file mode 100644
index 00000000000..195b9e93c1f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_local_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
new file mode 100644
index 00000000000..0186cd4c1e3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_malloc-asan.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
new file mode 100644
index 00000000000..0e725129643
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
@@ -0,0 +1,5 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: compilation of './tests/print.ml' failed
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
new file mode 100644
index 00000000000..a2ea974992b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_memcpy.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
new file mode 100644
index 00000000000..6af29643dcc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
@@ -0,0 +1,6 @@
+[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: cannot load plug-in 'print': cannot load module
+ Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./tests/print.cmxs: cannot open shared object file: No such file or directory\")")
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
new file mode 100644
index 00000000000..364bbe79ba4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_struct.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
new file mode 100644
index 00000000000..2cc42109513
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/temporal/t_while.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/test_config_dev b/src/plugins/e-acsl/tests/temporal/test_config_dev
new file mode 100644
index 00000000000..3e4efa8f66f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/test_config_dev
@@ -0,0 +1,5 @@
+DONTRUN:
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: OUT @PTEST_NAME@.res.log
+MACRO: ERR @PTEST_NAME@.err.log
+EXEC: ./scripts/e-acsl-gcc.sh --temporal -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index 7a8c9c6721a..3285052cca0 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -1,12 +1,4 @@
-MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
-MACRO: GLOBAL -machdep gcc_x86_64 -variadic-no-translation -verbose 0
-MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
-MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
-MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
-LOG: gen_@PTEST_NAME@.c
-OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
-EXEC: e-acsl-gcc.sh -c -X -F="-verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run -O @DEST@.run && ./@DEST@.run.e-acsl
-FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
-COMMENT: This regex works around the tendency of Frama-C to transform
-COMMENT: absolute path into relative ones whenever the file is not too far
-COMMENT: away from cwd.
+MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
+MACRO: OUT @PTEST_NAME@.res.log
+MACRO: ERR @PTEST_NAME@.err.log
+EXEC: BIN @DEST@.gcc.c ./scripts/e-acsl-gcc.sh -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
--
GitLab