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 bb570ee92a885dcd365840665e9b00de514a5dab..0000000000000000000000000000000000000000
--- 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 5e053cab3c744e96f02ea58ddbfac726d008ca3f..0000000000000000000000000000000000000000
--- 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 b42f8f987b3811fcd47315b45c397fc50c18ae68..0000000000000000000000000000000000000000
--- 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 63ab243f0f0ac90b52eb92796f458031b2f23bc9..0000000000000000000000000000000000000000
--- 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 7a5cede891e1d7fc3175c8f0839ee423771fa84a..0000000000000000000000000000000000000000
--- 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 4e888498a7d29bd018398fa488d5cd0bcd5d6caf..0000000000000000000000000000000000000000
--- 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 8e470a21dcd8bc3a4fb7cbd653e6337840efddb5..0000000000000000000000000000000000000000
--- 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 26a62cddaa2b4afdf33d1692dae5a3a79c99e62c..0000000000000000000000000000000000000000
--- 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 455ec56a835fd3d1536d3d10137cf67286160091..0000000000000000000000000000000000000000
--- 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 1b7f30270118bd782618efb4910af0ce98954bd0..0000000000000000000000000000000000000000
--- 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 803e26e12bb488545504f8066fe36c9f59a6de14..0000000000000000000000000000000000000000
--- 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 7e06012b6641a71b7d86732ac93f9801f42f1f5a..0000000000000000000000000000000000000000
--- 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 58a67ef052fb929bfd6e270717f18174ad1403fe..0000000000000000000000000000000000000000
--- 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 912f940b8d7f93255e66171733e59b74f0fb30ce..0000000000000000000000000000000000000000
--- 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 590199db8f04040ab84e966d5307b0dfc39f2ec5..0000000000000000000000000000000000000000
--- 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 19b0f068878a54abe6eb70c9b11771166b5fb060..0000000000000000000000000000000000000000
--- 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 0b966552605c312df3df587c9091b5dc19f54d58..0000000000000000000000000000000000000000
--- 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 e65b24385610fbf0e9291a09879dba416d9cfe8e..0000000000000000000000000000000000000000
--- 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 99bd8d2ca4576581e7e3419c51e1178a1542723a..0000000000000000000000000000000000000000
--- 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 93a1829d941669150d1f398004cdc422a7041bc6..0000000000000000000000000000000000000000
--- 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 3790aca8b1648cf45e6ab0e2e7266144f44af3ae..0000000000000000000000000000000000000000
--- 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 cb9a17cb49257c74abf0d92dee4c7b8549ecd8b1..0000000000000000000000000000000000000000
--- 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 ce219311963cd7c5a48aa4b07869a6c3d3c3389c..0000000000000000000000000000000000000000
--- 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 ea0b0b3e5e737e8e972eab0de467729f1b55189b..0000000000000000000000000000000000000000
--- 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 1baa04b66fa314c4f33180491d831eea829a54fe..0000000000000000000000000000000000000000
--- 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 d13cbafb98cd23d76f9ee695bc5c1e0e9158f7a4..0000000000000000000000000000000000000000
--- 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 2ed4f6df3461b85181897a66820a8073efcbefdf..0000000000000000000000000000000000000000
--- 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 1c4ca2adb3d7fa12bc94ab4b2420f2c3a44603a7..0000000000000000000000000000000000000000
--- 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 9751b7a8a5562c012c8a3a6bf06e091659203991..0000000000000000000000000000000000000000
--- 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 f751f743c00132de9c3f257ce73c01deb8859b22..0000000000000000000000000000000000000000
--- 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 4c326f214a130cf42d1e795388b0c88f34f6caa7..0000000000000000000000000000000000000000
--- 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 0122a7e4246394af3459e31969e6a0375ed0c61c..0000000000000000000000000000000000000000
--- 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 4ef916d51cbfbbc01e1fb200ecaded57aa452471..0000000000000000000000000000000000000000
--- 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 d21a94caccea54821812cfe937ca2446a230fb1c..0000000000000000000000000000000000000000
--- 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 5c570a670fa5408249a025b31ade7311a391fdd2..0000000000000000000000000000000000000000
--- 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 3bd50695afb1343ab68cf179bf22c6364bacf2f7..0000000000000000000000000000000000000000
--- 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 b09566f3aaf5b42219646778e6125c8a6b38df98..0000000000000000000000000000000000000000
--- 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 382eac9f065213428beb5ef5a6abbfb49a9b6194..0000000000000000000000000000000000000000
--- 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 2bd68e9f6dcd4681dfd4f5261d57da8bade8f5bc..0000000000000000000000000000000000000000
--- 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 c2db810f8d36e24400c596766b288e2e333c8a3d..0000000000000000000000000000000000000000
--- 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 7b03a368b78507b4138ef777b52cfbb963f7a0a8..0000000000000000000000000000000000000000
--- 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 a26972504fc11c11cb0b4cef5dc3098de33f50f9..0000000000000000000000000000000000000000
--- 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 c88d3077a73d1a0859eb8b27a861254b12c7b37e..0000000000000000000000000000000000000000
--- 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 bf1ef00efd5c9ce675530be79c853f6c7f5dc661..0000000000000000000000000000000000000000
--- 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 f970d17171ee2581d7d7f6be3d0fae73707be8d2..0000000000000000000000000000000000000000
--- 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 ade1e36d99e66024de2eda4d09cfd72bc0377643..0000000000000000000000000000000000000000
--- 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 84d2f0dd9410127e39335170feab7597534b1c14..0000000000000000000000000000000000000000
--- 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 79c41e376ff4d3e3a59dca0bf24993370504d131..0000000000000000000000000000000000000000
--- 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 b7000fff6c16bad99f08ac1e17b2f329a6292ead..0000000000000000000000000000000000000000
--- 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 908fd31137c0504497dbb0b32676afc8e843b780..0000000000000000000000000000000000000000
--- 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 3b950952f857555f940f059c2ba5ff05d023283a..0000000000000000000000000000000000000000
--- 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 bc4b2fca8240d19b78ea23ba7f785c8c25e90178..0000000000000000000000000000000000000000
--- 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 56f5b9ce5503a767bb5f388ef9430ee5c135e7a2..0000000000000000000000000000000000000000
--- 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 9e5f8b0f3d2f462c08830f4fbec1f7cb555bde52..0000000000000000000000000000000000000000
--- 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 6209d961c8a49396a36a19193d6ba7a3fa8e4367..0000000000000000000000000000000000000000
--- 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
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 ebab565158d2b71aeb27fdb9077718b4788f1a36..0000000000000000000000000000000000000000
--- 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
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 c3ff63dd0ce700cb2c8f81b5d3966c411b35d835..0000000000000000000000000000000000000000
--- 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 78e0d254f7ce67cf02ea35288b8c99260bfd5144..0000000000000000000000000000000000000000
--- 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 0de6311c2b2b21dbcb077c89367f32525dad330e..0000000000000000000000000000000000000000
--- 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 25dfbfef069fb1a71fc6f837a41f73a9eaa741c6..0000000000000000000000000000000000000000
--- 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 25dfbfef069fb1a71fc6f837a41f73a9eaa741c6..0000000000000000000000000000000000000000
--- 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 3c2bad6f858c1f3248748229c2c4d76d1e06bc24..0000000000000000000000000000000000000000
--- 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 e53ffdec61d97f8b6372416756249550b782b0c3..0000000000000000000000000000000000000000
--- 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 252a6e43c513855c224c72e0dde01bdb64de093c..0000000000000000000000000000000000000000
--- 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 6da7a17c6cbd609d91afb9420a61b43173acc0d6..0000000000000000000000000000000000000000
--- 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 431070f4cd2c23a54e002e700cf5e3b38de5ee9b..0000000000000000000000000000000000000000
--- 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 76570c39a1839f0a05c5bb260d0478f294dfc87d..0000000000000000000000000000000000000000
--- 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 fe96bbc669e4065fbba7c900a12576e99798f01f..0000000000000000000000000000000000000000
--- 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 9a8b757a2a064fbd610f0f38dcc832bf08a72d7e..0000000000000000000000000000000000000000
--- 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 1b45bb1e9d4e0c412975f7f584a3f5f41190bf4f..0000000000000000000000000000000000000000
--- 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 bc2fc3b1336d2d4591be415e6e62bd22371b58ef..0000000000000000000000000000000000000000
--- 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 5809c1481efc478b1ae9179ce5afbc4336029d2b..0000000000000000000000000000000000000000
--- 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 fdb2f2e29f43957563faa4c8433c28ca551a71cd..0000000000000000000000000000000000000000
--- 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 fb272a3c444be10982f0bbcd669f61999550fd56..0000000000000000000000000000000000000000
--- 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 106c9f6f4a7d36a2dced986139176c3d82abc26a..0000000000000000000000000000000000000000
--- 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 453f7b598d1082df921d710e460f9ef10443dc4c..0000000000000000000000000000000000000000
--- 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 165982a9f80f193617a7400635a8ac6442cbe4d7..0000000000000000000000000000000000000000
--- 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 46094a4bbe226c576a8f95aee14ba27b5dfe70bf..0000000000000000000000000000000000000000
--- 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 b995f5e2ce349ed69711ca6030bd3cec2977eefd..0000000000000000000000000000000000000000
--- 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 a076fcedfdb07a6e5dbd7554e48c110d6e0b1c0e..0000000000000000000000000000000000000000
--- 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 7f32099663f3add488d205bbd2f791e3e39a9b34..0000000000000000000000000000000000000000
--- 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 c1d1529325342788673c66157df18cac73916533..0000000000000000000000000000000000000000
--- 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 cd480f356c1cfca1517bff6ce0d69645e293b149..0000000000000000000000000000000000000000
--- 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 bd7713301eb0c15cb7f54248e38c2a8cff586b8f..0000000000000000000000000000000000000000
--- 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 ec68705fe630ce62dd5a9b90bf9c2e039d45e2cb..0000000000000000000000000000000000000000
--- 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 adabc66ff0a7eea47c5f7efafdcfb92cfa00f744..0000000000000000000000000000000000000000
--- 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 b8fcb3470dbfcb8da050df6fa58387387fe69b0d..0000000000000000000000000000000000000000
--- 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 460acb5fa597139c788b65a53882d3224f769e9d..0000000000000000000000000000000000000000
--- 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 3743a714794545c5ef62287213e81fef3ffa0e4b..0000000000000000000000000000000000000000
--- 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 36343fa0223fdbb51d13cac0fdb58f44c333a609..0000000000000000000000000000000000000000
--- 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 5b0314a0e239de01f82fde92d898059b25fa62f5..0000000000000000000000000000000000000000
--- 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 e6f6288929b8f85163da1241f838185526930c70..0000000000000000000000000000000000000000
--- 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 5a854c58c96a09f37219080a6c6cb8129f640230..0000000000000000000000000000000000000000
--- 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 9a18d848004451c94fd0b42a86ac95ecc99ddf61..0000000000000000000000000000000000000000
--- 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 b56718829921013ea3f8f5fc73a2f19c8496796b..0000000000000000000000000000000000000000
--- 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 fcdcd5edd933540db9cfee10d831693420f086bf..0000000000000000000000000000000000000000
--- 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 0b2ed5a9fc3516dbce7cc694cfdcaf45e0a8ed9a..0000000000000000000000000000000000000000
--- 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 15a2210f13df3c32991408613e0b5ebb2091b79f..0000000000000000000000000000000000000000
--- 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 45453873f24881a5367652c3ec53912d1685ea36..0000000000000000000000000000000000000000
--- 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 b54acaedc8843427148c51bb6a1c7a8aebee30b7..0000000000000000000000000000000000000000
--- 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 c325574714e3a2da8ca342144e3088da774e8e2b..0000000000000000000000000000000000000000
--- 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 767b46d932fa96248caba8ceeedf72cd7bd2356c..0000000000000000000000000000000000000000
--- 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 45dec02aac951fda0a503a2edf6a9011ef36bc1a..0000000000000000000000000000000000000000
--- 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 296f399f3c8f267c128d2a151780ed432257574f..0000000000000000000000000000000000000000
--- 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 cfa640a9f3642c03e9400b7012a5e580ef2f39e3..0000000000000000000000000000000000000000
--- 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 cfdeb9b03b56b0a1aa61b11bb839839e8951d589..0000000000000000000000000000000000000000
--- 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 455c37d94db4f36ab2df34f71c0d191461914e5c..0000000000000000000000000000000000000000
--- 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 1ac7a10c191fa0fe8b4f4cb3890b06b28fb79ffa..0000000000000000000000000000000000000000
--- 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 3d6c26919131756db591eb531cb53f86d6071745..0000000000000000000000000000000000000000
--- 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 6c6987459b8f35382cf162b4814d67a73001e3e5..0000000000000000000000000000000000000000
--- 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 5416bcc06c1764cde8f9851606aef790b17ba138..0000000000000000000000000000000000000000
--- 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 08a70fa93d302403de8b8e4dc4bf959cbc698a19..0000000000000000000000000000000000000000
--- 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 0e80917c3d153c8b123d3b1802a11b12735d2a94..0000000000000000000000000000000000000000
--- 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 63872161277dfbf0ebb5b2ac19593e308ce6f94e..0000000000000000000000000000000000000000
--- 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 e636757d80cf08bc6ce76558588b6d19d49165e6..0000000000000000000000000000000000000000
--- 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 0d1fede17ec74668949362f9d42a73335964b48c..0000000000000000000000000000000000000000
--- 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 1928ecb96d0085d762db87a850e00544a8bda1b2..0000000000000000000000000000000000000000
--- 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 0b50d95b38f263d8b94551a2bed66f9101f29029..0000000000000000000000000000000000000000
--- 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 45c2b6834f7254653cfc96bd1f7cb4f8a53ea163..0000000000000000000000000000000000000000
--- 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 33a7eb427f45fb397dce6f04cdee3d8e4de325fe..0000000000000000000000000000000000000000
--- 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 4246bf9d0533032254f2253d85e4129696e99379..0000000000000000000000000000000000000000
--- 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 6992e96210c075574977992126484a978ab93aa2..0000000000000000000000000000000000000000
--- 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 195b9e93c1fee84731bf7f97cb54e18760ccd095..0000000000000000000000000000000000000000
--- 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 0186cd4c1e3d0e5ac636ade4077be6f342ebe920..0000000000000000000000000000000000000000
--- 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 95c70361d689b4b4e6930818e275b4b729e56723..0000000000000000000000000000000000000000
--- 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 a2ea974992bd8ead8978265b8bc93ada317e795d..0000000000000000000000000000000000000000
--- 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 3d748d198fa047070be6e22c80b86c6689f40055..0000000000000000000000000000000000000000
--- 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 364bbe79ba49ad4e18fd601d0a6ae50a7f616985..0000000000000000000000000000000000000000
--- 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 2cc42109513b2955f1424545ef0d5d38224f8409..0000000000000000000000000000000000000000
--- 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)