From b6d2d29742492101bf66396c7032424453950407 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 20 Jul 2020 14:17:31 +0200
Subject: [PATCH] [eacsl:tests] Remove obsolete oracles
---
.../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/bitwise.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 -
.../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 -
.../bts1386_complex_flowgraph.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 -
.../bts/oracle_dev/issue-eacsl-105.res.oracle | 1 -
.../bts/oracle_dev/issue-eacsl-91.res.oracle | 1 -
.../tests/bts/oracle_dev/issue69.res.oracle | 1 -
.../constructs/oracle_dev/false.res.oracle | 1 -
.../oracle_dev/function_contract.res.oracle | 1 -
.../constructs/oracle_dev/ghost.res.oracle | 1 -
.../oracle_dev/invariant.res.oracle | 1 -
.../oracle_dev/labeled_stmt.res.oracle | 1 -
.../constructs/oracle_dev/lazy.res.oracle | 1 -
.../constructs/oracle_dev/loop.res.oracle | 1 -
.../oracle_dev/nested_code_annot.res.oracle | 1 -
.../constructs/oracle_dev/result.res.oracle | 1 -
.../oracle_dev/stmt_contract.res.oracle | 1 -
.../constructs/oracle_dev/true.res.oracle | 1 -
.../constructs/oracle_dev/typedef.res.oracle | 1 -
.../oracle_dev/functions_contiki.res.oracle | 1 -
.../oracle_dev/linear_search.res.oracle | 1 -
.../tests/format/oracle_ci/gen_printf2.c | 362 ------------------
.../format/oracle_ci/printf.0.err.oracle | 0
.../format/oracle_ci/printf.0.res.oracle | 83 ----
.../format/oracle_ci/printf.1.err.oracle | 0
.../format/oracle_ci/printf.1.res.oracle | 84 ----
.../format/oracle_dev/fprintf.res.oracle | 1 -
.../tests/format/oracle_dev/printf.res.oracle | 242 ------------
.../full-mmodel/oracle_ci/addrOf.0.res.oracle | 19 -
.../full-mmodel/oracle_ci/addrOf.1.res.oracle | 19 -
.../tests/full-mmodel/oracle_ci/gen_addrOf2.c | 82 ----
.../full-mmodel/oracle_dev/addrOf.res.oracle | 1 -
.../gmp-only/oracle_dev/arith.res.oracle | 1 -
.../gmp-only/oracle_dev/functions.res.oracle | 1 -
.../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 -
.../oracle_dev/decl_in_switch.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 -
.../oracle_dev/ghost_parameters.res.oracle | 1 -
.../tests/memory/oracle_dev/goto.res.oracle | 1 -
.../oracle_dev/hidden_malloc.res.oracle | 1 -
.../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 -
.../special/oracle_dev/builtin.res.oracle | 1 -
.../oracle_dev/e-acsl-functions.res.oracle | 1 -
.../oracle_dev/e-acsl-instrument.res.oracle | 1 -
.../oracle_dev/e-acsl-valid.res.oracle | 5 -
.../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 | 1 -
.../temporal/oracle_dev/t_fptr.res.oracle | 1 -
.../temporal/oracle_dev/t_fun_lib.res.oracle | 1 -
.../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 | 1 -
.../temporal/oracle_dev/t_memcpy.res.oracle | 1 -
.../temporal/oracle_dev/t_scope.res.oracle | 1 -
.../temporal/oracle_dev/t_struct.res.oracle | 1 -
.../temporal/oracle_dev/t_while.res.oracle | 1 -
131 files changed, 1036 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
delete mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
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
deleted file mode 100644
index bb570ee92a8..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 5e053cab3c7..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index b42f8f987b3..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 63ab243f0f0..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/at_on-purely-logic-variables.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
deleted file mode 100644
index 7a5cede891e..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/bitwise.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
deleted file mode 100644
index 4e888498a7d..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 8e470a21dcd..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 26a62cddaa2..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 455ec56a835..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 1b7f3027011..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 803e26e12bb..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 7e06012b664..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 58a67ef052f..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 912f940b8d7..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 590199db8f0..00000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing tests/arith/rationals.c (with preprocessing)
-[kernel:parser:decimal-float] tests/arith/rationals.c:19: 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/bts/oracle_dev/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
deleted file mode 100644
index 19b0f068878..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 0b966552605..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[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
deleted file mode 100644
index e65b2438561..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 99bd8d2ca45..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
deleted file mode 100644
index 93a1829d941..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1386_complex_flowgraph.c (with 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
deleted file mode 100644
index 3790aca8b16..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index cb9a17cb492..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index ce219311963..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index ea0b0b3e5e7..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 1baa04b66fa..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index d13cbafb98c..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 2ed4f6df346..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 1c4ca2adb3d..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 9751b7a8a55..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index f751f743c00..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 4c326f214a1..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 0122a7e4246..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 4ef916d51cb..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index d21a94cacce..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
+++ /dev/null
@@ -1,3 +0,0 @@
-[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
deleted file mode 100644
index 5c570a670fa..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 3bd50695afb..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index b09566f3aaf..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2406.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
deleted file mode 100644
index 382eac9f065..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/issue-eacsl-105.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
deleted file mode 100644
index 2bd68e9f6dc..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/issue-eacsl-91.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
deleted file mode 100644
index c2db810f8d3..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/issue69.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle
deleted file mode 100644
index 7b03a368b78..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/false.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle
deleted file mode 100644
index a26972504fc..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/function_contract.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle
deleted file mode 100644
index c88d3077a73..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/ghost.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle
deleted file mode 100644
index bf1ef00efd5..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/invariant.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle
deleted file mode 100644
index f970d17171e..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/labeled_stmt.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle
deleted file mode 100644
index ade1e36d99e..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/lazy.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle
deleted file mode 100644
index 84d2f0dd941..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/loop.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle
deleted file mode 100644
index 79c41e376ff..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/nested_code_annot.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle
deleted file mode 100644
index b7000fff6c1..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/result.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle
deleted file mode 100644
index 908fd31137c..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/stmt_contract.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle
deleted file mode 100644
index 3b950952f85..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/true.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle
deleted file mode 100644
index bc4b2fca824..00000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/typedef.i (no preprocessing)
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
deleted file mode 100644
index 56f5b9ce550..00000000000
--- a/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 9e5f8b0f3d2..00000000000
--- a/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/examples/linear_search.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
deleted file mode 100644
index 6209d961c8a..00000000000
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
+++ /dev/null
@@ -1,362 +0,0 @@
-/* Generated by Frama-C */
-#include "signal.h"
-#include "stdio.h"
-#include "stdlib.h"
-#include "string.h"
-#include "sys/time.h"
-#include "sys/wait.h"
-#include "time.h"
-#include "unistd.h"
-#include "wchar.h"
-char *__gen_e_acsl_literal_string_6;
-char *__gen_e_acsl_literal_string_8;
-char *__gen_e_acsl_literal_string_5;
-char *__gen_e_acsl_literal_string_9;
-char *__gen_e_acsl_literal_string_7;
-char *__gen_e_acsl_literal_string;
-char *__gen_e_acsl_literal_string_2;
-char *__gen_e_acsl_literal_string_4;
-char *__gen_e_acsl_literal_string_3;
-void signal_eval(int status, int expect_signal, char const *at)
-{
- __e_acsl_store_block((void *)(& at),(size_t)8);
- __e_acsl_store_block((void *)(& expect_signal),(size_t)4);
- __e_acsl_store_block((void *)(& status),(size_t)4);
- int signalled = (int)((signed char)((status & 0x7f) + 1)) >> 1 > 0;
- __e_acsl_store_block((void *)(& signalled),(size_t)4);
- __e_acsl_full_init((void *)(& signalled));
- if (signalled) {
- if (expect_signal) __e_acsl_builtin_printf("s",
- __gen_e_acsl_literal_string,
- at);
- else goto _LAND_1;
- }
- else
- _LAND_1:
- if (! signalled) {
- if (! expect_signal) __e_acsl_builtin_printf("s",
- __gen_e_acsl_literal_string_2,
- at);
- else goto _LAND_0;
- }
- else
- _LAND_0:
- if (! signalled) {
- if (expect_signal) {
- __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_3,at);
- __gen_e_acsl_exit(1);
- }
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (signalled)
- if (! expect_signal) {
- __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_4,at);
- __gen_e_acsl_exit(2);
- }
- }
- __e_acsl_delete_block((void *)(& at));
- __e_acsl_delete_block((void *)(& expect_signal));
- __e_acsl_delete_block((void *)(& status));
- __e_acsl_delete_block((void *)(& signalled));
- return;
-}
-
-char const *valid_specifiers = "diouxfFeEgGaAcspn";
-void apply_specifier(char *format, int spec)
-{
- int n;
- char *tmp_1;
- __e_acsl_store_block((void *)(& tmp_1),(size_t)8);
- __e_acsl_store_block((void *)(& n),(size_t)4);
- __e_acsl_store_block((void *)(& spec),(size_t)4);
- __e_acsl_store_block((void *)(& format),(size_t)8);
- void *p = (void *)0;
- __e_acsl_store_block((void *)(& p),(size_t)8);
- __e_acsl_full_init((void *)(& p));
- __e_acsl_full_init((void *)(& tmp_1));
- tmp_1 = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_5,spec);
- if (tmp_1 != (char *)0) __e_acsl_builtin_printf("e",(char const *)format,
- 1.0);
- else {
- char *tmp_0;
- __e_acsl_store_block((void *)(& tmp_0),(size_t)8);
- __e_acsl_full_init((void *)(& tmp_0));
- tmp_0 = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_6,spec);
- if (tmp_0 != (char *)0) __e_acsl_builtin_printf("D",(char const *)format,
- 1U);
- else {
- char *tmp;
- __e_acsl_store_block((void *)(& tmp),(size_t)8);
- __e_acsl_full_init((void *)(& tmp));
- tmp = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_7,spec);
- if (tmp != (char *)0) __e_acsl_builtin_printf("d",(char const *)format,
- 97);
- else
- if (spec == 's') __e_acsl_builtin_printf("s",(char const *)format,
- __gen_e_acsl_literal_string_8);
- else
- if (spec == 'n') __e_acsl_builtin_printf("i",(char const *)format,
- & n);
- else
- if (spec == 'p') __e_acsl_builtin_printf("p",
- (char const *)format,p);
- else __gen_e_acsl_abort();
- __e_acsl_delete_block((void *)(& tmp));
- }
- __e_acsl_delete_block((void *)(& tmp_0));
- }
- __e_acsl_delete_block((void *)(& spec));
- __e_acsl_delete_block((void *)(& format));
- __e_acsl_delete_block((void *)(& tmp_1));
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& n));
- return;
-}
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *);
-
-/* compiler builtin:
- void *__builtin_alloca(unsigned long); */
-void test_specifier_application(char const *allowed, char const *fmt,
- int only_negative, char *at)
-{
- size_t tmp;
- unsigned long __lengthof_format;
- __e_acsl_store_block((void *)(& __lengthof_format),(size_t)8);
- __e_acsl_store_block((void *)(& tmp),(size_t)8);
- __e_acsl_store_block((void *)(& at),(size_t)8);
- __e_acsl_store_block((void *)(& only_negative),(size_t)4);
- __e_acsl_store_block((void *)(& fmt),(size_t)8);
- __e_acsl_store_block((void *)(& allowed),(size_t)8);
- __e_acsl_full_init((void *)(& tmp));
- tmp = __gen_e_acsl_strlen(fmt);
- int len = (int)tmp;
- __e_acsl_store_block((void *)(& len),(size_t)4);
- __e_acsl_full_init((void *)(& len));
- /*@ assert
- alloca_bounds: 0 < sizeof(char) * (len + 1) ≤ 18446744073709551615;
- */
- {
- int __gen_e_acsl_and;
- if (0L < 1L * (len + 1L)) {
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_le;
- __gmpz_init_set_si(__gen_e_acsl_,1L * (len + 1L));
- __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gen_e_acsl_and = __gen_e_acsl_le <= 0;
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl__2);
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
- (char *)"test_specifier_application",
- (char *)"alloca_bounds: 0 < sizeof(char) * (len + 1) <= 18446744073709551615",
- 82);
- }
- __e_acsl_full_init((void *)(& __lengthof_format));
- __lengthof_format = (unsigned long)(len + 1);
- char *format = __builtin_alloca(sizeof(char) * __lengthof_format);
- __e_acsl_store_block((void *)format,sizeof(char) * __lengthof_format);
- __e_acsl_store_block((void *)(& format),(size_t)8);
- __e_acsl_full_init((void *)(& format));
- __gen_e_acsl_strcpy(format,fmt);
- {
- int i_0 = 0;
- __e_acsl_store_block((void *)(& i_0),(size_t)4);
- __e_acsl_full_init((void *)(& i_0));
- while (1) {
- size_t tmp_3;
- __e_acsl_store_block((void *)(& tmp_3),(size_t)8);
- __e_acsl_full_init((void *)(& tmp_3));
- tmp_3 = __gen_e_acsl_strlen(valid_specifiers);
- ;
- if (! ((size_t)i_0 < tmp_3)) {
- __e_acsl_delete_block((void *)(& tmp_3));
- break;
- }
- {
- char *tmp_2;
- __e_acsl_store_block((void *)(& tmp_2),(size_t)8);
- int c = (int)*(valid_specifiers + i_0);
- __e_acsl_store_block((void *)(& c),(size_t)4);
- __e_acsl_full_init((void *)(& c));
- __e_acsl_initialize((void *)(format + (len - 1)),sizeof(char));
- *(format + (len - 1)) = (char)c;
- __e_acsl_full_init((void *)(& tmp_2));
- tmp_2 = __gen_e_acsl_strchr(allowed,c);
- if (tmp_2) {
- if (! only_negative) {
- {
- pid_t pid = fork();
- __e_acsl_store_block((void *)(& pid),(size_t)4);
- __e_acsl_full_init((void *)(& pid));
- if (! pid) {
- apply_specifier(format,c);
- __gen_e_acsl_exit(0);
- }
- else {
- int process_status;
- __e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
- signal_eval(process_status,0,(char const *)at);
- __e_acsl_delete_block((void *)(& process_status));
- }
- __e_acsl_delete_block((void *)(& pid));
- }
- }
- }
- else {
- {
- pid_t pid_0 = fork();
- __e_acsl_store_block((void *)(& pid_0),(size_t)4);
- __e_acsl_full_init((void *)(& pid_0));
- if (! pid_0) {
- apply_specifier(format,c);
- __gen_e_acsl_exit(0);
- }
- else {
- int process_status_0;
- __e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
- signal_eval(process_status_0,1,(char const *)at);
- __e_acsl_delete_block((void *)(& process_status_0));
- }
- __e_acsl_delete_block((void *)(& pid_0));
- }
- }
- __e_acsl_delete_block((void *)(& tmp_2));
- __e_acsl_delete_block((void *)(& c));
- }
- __e_acsl_full_init((void *)(& i_0));
- i_0 ++;
- __e_acsl_delete_block((void *)(& tmp_3));
- }
- __e_acsl_delete_block((void *)(& i_0));
- }
- __e_acsl_delete_block((void *)format);
- __e_acsl_delete_block((void *)(& at));
- __e_acsl_delete_block((void *)(& only_negative));
- __e_acsl_delete_block((void *)(& fmt));
- __e_acsl_delete_block((void *)(& allowed));
- __e_acsl_delete_block((void *)(& __lengthof_format));
- __e_acsl_delete_block((void *)(& format));
- __e_acsl_delete_block((void *)(& tmp));
- __e_acsl_delete_block((void *)(& len));
- return;
-}
-
-void __e_acsl_globals_init(void)
-{
- __gen_e_acsl_literal_string_6 = "uoxX";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("uoxX"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
- __gen_e_acsl_literal_string_8 = "foo";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,sizeof("foo"));
- __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_5 = "fFeEgGaA";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
- sizeof("fFeEgGaA"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
- __gen_e_acsl_literal_string_9 = "diouxfFeEgGaAcspn";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("diouxfFeEgGaAcspn"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_7 = "dic";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,sizeof("dic"));
- __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 = "OK: expected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("OK: expected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
- __gen_e_acsl_literal_string_2 = "OK: Expected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("OK: Expected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string_4 = "FAIL: Unexpected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
- sizeof("FAIL: Unexpected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_3 = "FAIL: Unexpected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
- sizeof("FAIL: Unexpected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_store_block((void *)(& __gen_e_acsl_strcpy),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strcpy));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strchr),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strchr));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strlen),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strlen));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
- __e_acsl_store_block((void *)(& test_specifier_application),(size_t)1);
- __e_acsl_full_init((void *)(& test_specifier_application));
- __e_acsl_store_block((void *)(& apply_specifier),(size_t)1);
- __e_acsl_full_init((void *)(& apply_specifier));
- __e_acsl_store_block((void *)(& valid_specifiers),(size_t)8);
- __e_acsl_full_init((void *)(& valid_specifiers));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& __fc_p_time_tm),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_time_tm));
- __e_acsl_store_block((void *)(& __fc_time_tm),(size_t)36);
- __e_acsl_full_init((void *)(& __fc_time_tm));
- __e_acsl_store_block((void *)(__fc_fds),(size_t)4096);
- __e_acsl_full_init((void *)(& __fc_fds));
- __e_acsl_store_block((void *)(& __fc_fds_state),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_fds_state));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)4096);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
- return;
-}
-
-int main(int argc, char const **argv)
-{
- int __retres;
- __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
- __e_acsl_globals_init();
- __e_acsl_store_block((void *)(& __retres),(size_t)4);
- __e_acsl_full_init((void *)(& __retres));
- __retres = 0;
- __e_acsl_delete_block((void *)(& argv));
- __e_acsl_delete_block((void *)(& argc));
- __e_acsl_delete_block((void *)(& test_specifier_application));
- __e_acsl_delete_block((void *)(& apply_specifier));
- __e_acsl_delete_block((void *)(& valid_specifiers));
- __e_acsl_delete_block((void *)(& signal_eval));
- __e_acsl_delete_block((void *)(& __fc_p_time_tm));
- __e_acsl_delete_block((void *)(& __fc_time_tm));
- __e_acsl_delete_block((void *)(__fc_fds));
- __e_acsl_delete_block((void *)(& __fc_fds_state));
- __e_acsl_delete_block((void *)(& __fc_time));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
- __e_acsl_delete_block((void *)(& __retres));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
deleted file mode 100644
index ebab565158d..00000000000
--- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
+++ /dev/null
@@ -1,83 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strchr':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:57:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:221:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:222:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:134:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __fc_fopen[0..511] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __e_acsl_internal_heap ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
- __fc_fds_state ∈ [--..--]
- __fc_fds[0..1023] ∈ {0}
- __fc_time_tm ∈ {0}
- __fc_p_time_tm ∈ {{ &__fc_time_tm }}
- valid_specifiers ∈ {{ "diouxfFeEgGaAcspn" }}
- __gen_e_acsl_literal_string ∈ {0}
- __gen_e_acsl_literal_string_2 ∈ {0}
- __gen_e_acsl_literal_string_3 ∈ {0}
- __gen_e_acsl_literal_string_4 ∈ {0}
- __gen_e_acsl_literal_string_5 ∈ {0}
- __gen_e_acsl_literal_string_6 ∈ {0}
- __gen_e_acsl_literal_string_7 ∈ {0}
- __gen_e_acsl_literal_string_8 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function __e_acsl_delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
deleted file mode 100644
index c3ff63dd0ce..00000000000
--- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
+++ /dev/null
@@ -1,84 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strchr':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:57:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:221:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:222:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:134:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __fc_fopen[0..511] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __e_acsl_internal_heap ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
- __fc_fds_state ∈ [--..--]
- __fc_fds[0..1023] ∈ {0}
- __fc_time_tm ∈ {0}
- __fc_p_time_tm ∈ {{ &__fc_time_tm }}
- valid_specifiers ∈ {{ "diouxfFeEgGaAcspn" }}
- __gen_e_acsl_literal_string ∈ {0}
- __gen_e_acsl_literal_string_2 ∈ {0}
- __gen_e_acsl_literal_string_3 ∈ {0}
- __gen_e_acsl_literal_string_4 ∈ {0}
- __gen_e_acsl_literal_string_5 ∈ {0}
- __gen_e_acsl_literal_string_6 ∈ {0}
- __gen_e_acsl_literal_string_7 ∈ {0}
- __gen_e_acsl_literal_string_8 ∈ {0}
- __gen_e_acsl_literal_string_9 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function __e_acsl_delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
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
deleted file mode 100644
index 78e0d254f7c..00000000000
--- a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/format/fprintf.c (with preprocessing)
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
deleted file mode 100644
index 0de6311c2b2..00000000000
--- a/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
+++ /dev/null
@@ -1,242 +0,0 @@
-[kernel] Parsing tests/format/printf.c (with preprocessing)
-[kernel:parser:decimal-float] tests/format/printf.c:89: Warning:
- Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[variadic] tests/format/printf.c:29: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:31: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:33: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:35: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:37: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:39: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:186: Warning:
- Not enough arguments: expected 5, given 4.
-[variadic] tests/format/printf.c:189: Warning:
- Too many arguments: expected 5, given 6. Superfluous arguments will be removed.
-[variadic] tests/format/printf.c:194: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:197: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:199: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:201: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:204: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:206: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:226: Warning: Unknown conversion specifier l.
-[variadic] tests/format/printf.c:257: Warning:
- Incorrect type for argument 2. The argument will be cast from wint_t to intmax_t.
-[variadic] tests/format/printf.c:279: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:279: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:292: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:292: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:293: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:293: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:307: Warning: Unknown conversion specifier C.
-[variadic] tests/format/printf.c:308: Warning: Unknown conversion specifier S.
-[variadic] tests/format/printf.c:309: Warning: Unknown conversion specifier m.
-[variadic] tests/format/printf.c:315: Warning:
- Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/format/printf.c:315: Warning:
- Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/format/printf.c:316: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/format/printf.c:316: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/format/printf.c:317: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to int.
-[variadic] tests/format/printf.c:317: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to int.
-[variadic] tests/format/printf.c:318: Warning:
- Incorrect type for argument 2. The argument will be cast from double to int.
-[variadic] tests/format/printf.c:318: Warning:
- Incorrect type for argument 2. The argument will be cast from double to int.
-[variadic] tests/format/printf.c:328: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:328: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:355: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:355: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:356: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:356: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:357: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:357: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:359: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:359: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:360: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:360: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:361: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:361: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:363: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:363: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:364: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:364: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:365: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:365: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:367: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:367: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:368: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:368: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:369: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:369: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:372: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:372: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:374: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:374: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:375: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:375: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:376: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:376: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:378: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:378: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:379: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:379: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:380: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:380: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:382: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:382: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:383: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:383: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:384: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:384: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:386: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:386: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:387: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:387: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:393: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/format/printf.c:394: Warning:
- Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/format/printf.c:395: Warning:
- Incorrect type for argument 2. The argument will be cast from double to int.
-[variadic] tests/format/printf.c:396: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to int.
-[variadic] tests/format/printf.c:399: Warning:
- Incorrect type for argument 2. The argument will be cast from wint_t to intmax_t.
-[variadic] tests/format/printf.c:400: Warning:
- Incorrect type for argument 2. The argument will be cast from long to intmax_t.
-[variadic] tests/format/printf.c:409: Warning:
- Incorrect type for argument 2. The argument will be cast from int to char *.
-[variadic] tests/format/printf.c:464: Warning: Unknown conversion specifier '.
-[variadic] tests/format/printf.c:465: Warning:
- Flag 0 and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:466: Warning:
- Flag # and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:467: Warning:
- Flag ' ' and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:468: Warning:
- Flag + and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:469: Warning:
- Flag - and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:470: Warning:
- Conversion specifier n does not expect a field width.
-[variadic] tests/format/printf.c:471: Warning:
- Conversion specifier n does not expect a field width.
-[variadic] tests/format/printf.c:472: Warning:
- Conversion specifier n does not expect a field width.
-[variadic] tests/format/printf.c:473: Warning:
- Conversion specifier n does not expect a precision.
-[variadic] tests/format/printf.c:476: Warning: Unknown conversion specifier '.
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
deleted file mode 100644
index 25dfbfef069..00000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- __e_acsl_init ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[eva] using specification for function __e_acsl_initialized
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
deleted file mode 100644
index 25dfbfef069..00000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- __e_acsl_init ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[eva] using specification for function __e_acsl_initialized
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
deleted file mode 100644
index 3c2bad6f858..00000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
+++ /dev/null
@@ -1,82 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-void f(void)
-{
- int m;
- int *u;
- int *p;
- __e_acsl_store_block((void *)(& p),(size_t)8);
- __e_acsl_store_block((void *)(& u),(size_t)8);
- __e_acsl_store_block((void *)(& m),(size_t)4);
- __e_acsl_full_init((void *)(& u));
- u = & m;
- __e_acsl_full_init((void *)(& p));
- p = u;
- __e_acsl_full_init((void *)(& m));
- m = 123;
- /*@ assert \initialized(p); */
- {
- int __gen_e_acsl_initialized;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
- __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f",
- (char *)"\\initialized(p)",10);
- }
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& u));
- __e_acsl_delete_block((void *)(& m));
- return;
-}
-
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __e_acsl_store_block((void *)(& f),(size_t)1);
- __e_acsl_full_init((void *)(& f));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
- }
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_globals_init();
- __e_acsl_store_block((void *)(& __retres),(size_t)4);
- int x = 0;
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __e_acsl_full_init((void *)(& x));
- f();
- /*@ assert &x ≡ &x; */
- __e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
- (char *)"&x == &x",16);
- __e_acsl_full_init((void *)(& __retres));
- __retres = 0;
- __e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
- __e_acsl_delete_block((void *)(& x));
- __e_acsl_delete_block((void *)(& __retres));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
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
deleted file mode 100644
index e53ffdec61d..00000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/full-mmodel/addrOf.i (no preprocessing)
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
deleted file mode 100644
index 252a6e43c51..00000000000
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 6da7a17c6cb..00000000000
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/gmp-only/functions.c (with preprocessing)
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
deleted file mode 100644
index 431070f4cd2..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 76570c39a18..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index fe96bbc669e..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 9a8b757a2a0..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 1b45bb1e9d4..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index bc2fc3b1336..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 5809c1481ef..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index fdb2f2e29f4..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index fb272a3c444..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 106c9f6f4a7..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ctype_macros.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
deleted file mode 100644
index 453f7b598d1..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/decl_in_switch.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
deleted file mode 100644
index 165982a9f80..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 46094a4bbe2..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index b995f5e2ce3..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/freeable.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
deleted file mode 100644
index a076fcedfdb..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ghost_parameters.i (no 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
deleted file mode 100644
index 7f32099663f..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index c1d15293253..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/hidden_malloc.c (with preprocessing)
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
deleted file mode 100644
index cd480f356c1..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index bd7713301eb..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index ec68705fe63..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index adabc66ff0a..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index b8fcb3470db..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 460acb5fa59..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 3743a714794..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 36343fa0223..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 5b0314a0e23..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index e6f6288929b..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 5a854c58c96..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 9a18d848004..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index b5671882992..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index fcdcd5edd93..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 0b2ed5a9fc3..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 15a2210f13d..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 45453873f24..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index b54acaedc88..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index c325574714e..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 767b46d932f..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 45dec02aac9..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 296f399f3c8..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index cfa640a9f36..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/vla.c (with preprocessing)
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
deleted file mode 100644
index cfdeb9b03b5..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/special/builtin.i (no preprocessing)
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
deleted file mode 100644
index 455c37d94db..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/special/e-acsl-functions.c (with preprocessing)
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
deleted file mode 100644
index 1ac7a10c191..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/special/e-acsl-instrument.c (with preprocessing)
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
deleted file mode 100644
index 3d6c2691913..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing share/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing share/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/special/e-acsl-valid.c (with preprocessing)
-[eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
- function f: precondition \valid(y) got status unknown.
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
deleted file mode 100644
index 6c6987459b8..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 5416bcc06c1..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 08a70fa93d3..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 0e80917c3d1..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 63872161277..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-[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
deleted file mode 100644
index e636757d80c..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_dpointer.c (with preprocessing)
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
deleted file mode 100644
index 0d1fede17ec..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 1928ecb96d0..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_fun_lib.c (with preprocessing)
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
deleted file mode 100644
index 0b50d95b38f..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 45c2b6834f7..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 33a7eb427f4..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 4246bf9d053..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 6992e96210c..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 195b9e93c1f..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 0186cd4c1e3..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 95c70361d68..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_malloc.c (with preprocessing)
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
deleted file mode 100644
index a2ea974992b..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 3d748d198fa..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_scope.c (with preprocessing)
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
deleted file mode 100644
index 364bbe79ba4..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[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
deleted file mode 100644
index 2cc42109513..00000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_while.c (with preprocessing)
--
GitLab