From 0b25e04fd954c0ecbacf3459c6a0095fafd052d6 Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Fri, 10 Apr 2020 14:34:03 +0200 Subject: [PATCH] [eacsl:dev] Log stderr from e-acsl test execution (dev config) --- .../e-acsl/tests/arith/oracle_dev/arith.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/array.e-acsl.err.log | 0 src/plugins/e-acsl/tests/arith/oracle_dev/at.e-acsl.err.log | 0 .../oracle_dev/at_on-purely-logic-variables.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/cast.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/comparison.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/functions.e-acsl.err.log | 0 .../tests/arith/oracle_dev/functions_rec.e-acsl.err.log | 0 .../tests/arith/oracle_dev/integer_constant.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/let.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/longlong.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/not.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/quantif.e-acsl.err.log | 0 .../e-acsl/tests/arith/oracle_dev/rationals.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1304.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1307.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1324.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1326.e-acsl.err.log | 0 .../bts/oracle_dev/bts1386_complex_flowgraph.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1390.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1395.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1398.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1399.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1478.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1700.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1717.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1718.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1740.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts1837.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2191.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2192.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2231.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2252.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2305.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2386.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/bts2406.e-acsl.err.log | 0 .../tests/bts/oracle_dev/issue-eacsl-105.e-acsl.err.log | 0 .../tests/bts/oracle_dev/issue-eacsl-91.e-acsl.err.log | 0 .../e-acsl/tests/bts/oracle_dev/issue69.e-acsl.err.log | 0 .../e-acsl/tests/constructs/oracle_dev/false.e-acsl.err.log | 0 .../constructs/oracle_dev/function_contract.e-acsl.err.log | 0 .../e-acsl/tests/constructs/oracle_dev/ghost.e-acsl.err.log | 0 .../tests/constructs/oracle_dev/invariant.e-acsl.err.log | 0 .../tests/constructs/oracle_dev/labeled_stmt.e-acsl.err.log | 0 .../e-acsl/tests/constructs/oracle_dev/lazy.e-acsl.err.log | 0 .../e-acsl/tests/constructs/oracle_dev/loop.e-acsl.err.log | 0 .../constructs/oracle_dev/nested_code_annot.e-acsl.err.log | 0 .../tests/constructs/oracle_dev/result.e-acsl.err.log | 0 .../constructs/oracle_dev/stmt_contract.e-acsl.err.log | 0 .../e-acsl/tests/constructs/oracle_dev/true.e-acsl.err.log | 0 .../tests/constructs/oracle_dev/typedef.e-acsl.err.log | 0 .../examples/oracle_dev/functions_contiki.e-acsl.err.log | 0 .../tests/examples/oracle_dev/linear_search.e-acsl.err.log | 0 .../tests/full-mmodel/oracle_dev/addrOf.e-acsl.err.log | 0 .../e-acsl/tests/gmp-only/oracle_dev/arith.e-acsl.err.log | 0 .../tests/gmp-only/oracle_dev/functions.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/addrOf.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/alias.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/base_addr.e-acsl.err.log | 0 .../tests/memory/oracle_dev/block_length.e-acsl.err.log | 0 .../tests/memory/oracle_dev/block_valid.e-acsl.err.log | 0 .../tests/memory/oracle_dev/bypassed_var.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/call.e-acsl.err.log | 0 .../memory/oracle_dev/compound_initializers.e-acsl.err.log | 0 .../tests/memory/oracle_dev/constructor.e-acsl.err.log | 0 .../tests/memory/oracle_dev/ctype_macros.e-acsl.err.log | 0 .../tests/memory/oracle_dev/decl_in_switch.e-acsl.err.log | 0 .../tests/memory/oracle_dev/early_exit.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/errno.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/freeable.e-acsl.err.log | 0 .../tests/memory/oracle_dev/ghost_parameters.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/goto.e-acsl.err.log | 0 .../tests/memory/oracle_dev/hidden_malloc.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/init.e-acsl.err.log | 0 .../tests/memory/oracle_dev/init_function.e-acsl.err.log | 0 .../tests/memory/oracle_dev/initialized.e-acsl.err.log | 0 .../tests/memory/oracle_dev/literal_string.e-acsl.err.log | 0 .../tests/memory/oracle_dev/local_goto.e-acsl.err.log | 0 .../tests/memory/oracle_dev/local_init.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/local_var.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/mainargs.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/memalign.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/memsize.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/null.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/offset.e-acsl.err.log | 0 .../tests/memory/oracle_dev/other_constants.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/ptr.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/ptr_init.e-acsl.err.log | 0 .../memory/oracle_dev/ranges_in_builtins.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/sizeof.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/stdout.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/valid.e-acsl.err.log | 0 .../tests/memory/oracle_dev/valid_alias.e-acsl.err.log | 0 .../memory/oracle_dev/valid_in_contract.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/vector.e-acsl.err.log | 0 .../e-acsl/tests/memory/oracle_dev/vla.e-acsl.err.log | 0 src/plugins/e-acsl/tests/test_config_dev.in | 6 +++++- 97 files changed, 5 insertions(+), 1 deletion(-) create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/arith.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/array.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/at.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/cast.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/comparison.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/functions.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/let.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/longlong.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/not.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/quantif.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/arith/oracle_dev/rationals.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue69.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/false.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/loop.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/result.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/true.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/alias.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/block_length.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/call.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/constructor.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/errno.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/freeable.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/goto.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/init.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/init_function.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/initialized.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_init.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/local_var.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/memalign.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/memsize.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/null.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/offset.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ptr.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/stdout.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/vector.e-acsl.err.log create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/vla.e-acsl.err.log 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in index 078ff35d56f..8a01dabc2ff 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 -- GitLab