diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/arith.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/arith.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/array.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/array.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/at.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/at.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/cast.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/cast.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/functions.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/functions.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/let.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/let.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/not.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/not.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/false.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/false.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/result.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/result.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/true.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/true.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.e-acsl.err.log b/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.e-acsl.err.log b/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.e-acsl.err.log b/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.e-acsl.err.log b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.e-acsl.err.log b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/alias.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/alias.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/call.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/call.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/errno.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/errno.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/goto.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/goto.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/init.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/init.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/null.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/null.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/offset.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/offset.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/valid.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/vector.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/vector.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/vla.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/vla.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in index 078ff35d56f94053034f9c87584fa6c5969e876e..8a01dabc2fff701b297a64e5ca32911b5fc81414 100644 --- a/src/plugins/e-acsl/tests/test_config_dev.in +++ b/src/plugins/e-acsl/tests/test_config_dev.in @@ -1,6 +1,8 @@ +MACRO: SEDCMD @SEDCMD@ MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@ MACRO: OUT @PTEST_NAME@.res.log MACRO: ERR @PTEST_NAME@.err.log +MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.err.log COMMENT: Define the following macro to "no" in a test to stop the execution of `e-acsl-gcc.sh` MACRO: ROOT_EACSL_GCC_ENABLE yes COMMENT: Default options for `e-acsl-gcc.sh` @@ -11,4 +13,6 @@ COMMENT: Define the following macro in a test to pass extra options to the frama MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh` MACRO: ROOT_EACSL_GCC_OPTS_EXT -EXEC: if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null; fi +COMMENT: Define the following macro in a test to filter the output of the test execution +MACRO: ROOT_EACSL_EXEC_FILTER cat +EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi