From 75d20451ceba6240b10fa35c7a587e51c4ee5282 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 30 Aug 2019 16:11:01 +0200
Subject: [PATCH] [tests] config ci
---
src/plugins/e-acsl/.gitignore | 4 +-
src/plugins/e-acsl/Makefile.in | 34 ++--
.../memory => known_bugs}/decl_in_switch.c | 2 +-
src/plugins/e-acsl/tests/arith/array.i | 2 +-
.../e-acsl/tests/arith/functions_rec.c | 2 +-
src/plugins/e-acsl/tests/arith/longlong.i | 2 +-
.../{oracle => oracle_ci}/arith.res.oracle | 0
.../{oracle => oracle_ci}/array.res.oracle | 0
.../arith/{oracle => oracle_ci}/at.res.oracle | 0
.../at_on-purely-logic-variables.res.oracle | 0
.../{oracle => oracle_ci}/cast.res.oracle | 0
.../comparison.res.oracle | 0
.../functions.res.oracle | 0
.../functions_rec.res.oracle | 0
.../arith/{oracle => oracle_ci}/gen_arith.c | 0
.../arith/{oracle => oracle_ci}/gen_array.c | 0
.../arith/{oracle => oracle_ci}/gen_at.c | 0
.../gen_at_on-purely-logic-variables.c | 0
.../arith/{oracle => oracle_ci}/gen_cast.c | 0
.../{oracle => oracle_ci}/gen_comparison.c | 0
.../{oracle => oracle_ci}/gen_functions.c | 0
.../{oracle => oracle_ci}/gen_functions_rec.c | 0
.../gen_integer_constant.c | 0
.../arith/{oracle => oracle_ci}/gen_let.c | 0
.../{oracle => oracle_ci}/gen_longlong.c | 0
.../arith/{oracle => oracle_ci}/gen_not.c | 0
.../arith/{oracle => oracle_ci}/gen_quantif.c | 0
.../{oracle => oracle_ci}/gen_rationals.c | 0
.../integer_constant.res.oracle | 0
.../{oracle => oracle_ci}/let.res.oracle | 0
.../{oracle => oracle_ci}/longlong.res.oracle | 0
.../{oracle => oracle_ci}/not.res.oracle | 0
.../{oracle => oracle_ci}/quantif.res.oracle | 0
.../rationals.res.oracle | 0
.../arith/{result => result_ci}/.gitkeep | 0
src/plugins/e-acsl/tests/bts/bts1395.i | 2 +-
.../{oracle => oracle_ci}/bts1304.res.oracle | 0
.../{oracle => oracle_ci}/bts1307.res.oracle | 0
.../{oracle => oracle_ci}/bts1324.res.oracle | 0
.../{oracle => oracle_ci}/bts1326.res.oracle | 0
.../{oracle => oracle_ci}/bts1390.res.oracle | 0
.../{oracle => oracle_ci}/bts1395.res.oracle | 0
.../{oracle => oracle_ci}/bts1398.res.oracle | 0
.../{oracle => oracle_ci}/bts1399.res.oracle | 0
.../{oracle => oracle_ci}/bts1478.res.oracle | 0
.../{oracle => oracle_ci}/bts1700.res.oracle | 0
.../{oracle => oracle_ci}/bts1717.res.oracle | 0
.../{oracle => oracle_ci}/bts1718.res.oracle | 0
.../{oracle => oracle_ci}/bts1740.res.oracle | 0
.../{oracle => oracle_ci}/bts1837.res.oracle | 0
.../{oracle => oracle_ci}/bts2191.res.oracle | 0
.../{oracle => oracle_ci}/bts2192.res.oracle | 0
.../{oracle => oracle_ci}/bts2231.res.oracle | 0
.../{oracle => oracle_ci}/bts2252.res.oracle | 0
.../{oracle => oracle_ci}/bts2305.res.oracle | 0
.../{oracle => oracle_ci}/bts2386.res.oracle | 0
.../{oracle => oracle_ci}/bts2406.res.oracle | 0
.../bts/{oracle => oracle_ci}/gen_bts1304.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1307.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1324.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1326.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1390.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1395.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1398.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1399.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1478.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1700.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1717.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1718.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1740.c | 0
.../bts/{oracle => oracle_ci}/gen_bts1837.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2191.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2192.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2231.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2252.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2305.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2386.c | 0
.../bts/{oracle => oracle_ci}/gen_bts2406.c | 0
.../bts/{oracle => oracle_ci}/gen_issue69.c | 0
.../{oracle => oracle_ci}/issue69.res.oracle | 0
.../{oracle => oracle_ci}/gen_strcat.c | 0
.../{oracle => oracle_ci}/gen_strcmp.c | 0
.../{oracle => oracle_ci}/gen_strcpy.c | 0
.../{oracle => oracle_ci}/gen_strlen.c | 0
.../{oracle => oracle_ci}/strcat.res.oracle | 0
.../{oracle => oracle_ci}/strcmp.res.oracle | 0
.../{oracle => oracle_ci}/strcpy.res.oracle | 0
.../{oracle => oracle_ci}/strlen.res.oracle | 0
.../builtin/{test_config => test_config_ci} | 0
.../functions_contiki.res.oracle | 0
.../gen_functions_contiki.c | 0
.../{oracle => oracle_ci}/gen_linear_search.c | 0
.../linear_search.res.oracle | 0
.../{oracle => oracle_ci}/fprintf.res.oracle | 0
.../{oracle => oracle_ci}/gen_fprintf.c | 0
.../format/{oracle => oracle_ci}/gen_printf.c | 0
.../{oracle => oracle_ci}/gen_printf2.c | 0
.../{oracle => oracle_ci}/printf.0.err.oracle | 0
.../{oracle => oracle_ci}/printf.0.res.oracle | 0
.../{oracle => oracle_ci}/printf.1.err.oracle | 0
.../{oracle => oracle_ci}/printf.1.res.oracle | 0
.../{oracle => oracle_ci}/printf.err.oracle | 0
.../{oracle => oracle_ci}/printf.res.oracle | 0
src/plugins/e-acsl/tests/format/printf.c | 2 +-
.../format/{test_config => test_config_ci} | 0
.../e-acsl/tests/full-mmodel/let-alias.c | 1 -
.../{oracle => oracle_ci}/addrOf.0.res.oracle | 0
.../{oracle => oracle_ci}/addrOf.1.res.oracle | 0
.../{oracle => oracle_ci}/addrOf.res.oracle | 0
.../{oracle => oracle_ci}/gen_addrOf.c | 0
.../{oracle => oracle_ci}/gen_addrOf2.c | 0
.../{oracle => oracle_ci}/gen_let-alias.c | 0
.../let-alias.res.oracle | 0
.../{test_config => test_config_ci} | 0
.../{oracle => oracle_ci}/arith.res.oracle | 0
.../functions.res.oracle | 0
.../{oracle => oracle_ci}/gen_arith.c | 0
.../{oracle => oracle_ci}/gen_functions.c | 0
.../gmp-only/{test_config => test_config_ci} | 0
.../tests/language_constructs/invariant.i | 2 +-
.../e-acsl/tests/language_constructs/loop.i | 2 +-
.../{oracle => oracle_ci}/false.res.oracle | 0
.../function_contract.res.oracle | 0
.../{oracle => oracle_ci}/gen_false.c | 0
.../gen_function_contract.c | 0
.../{oracle => oracle_ci}/gen_ghost.c | 0
.../{oracle => oracle_ci}/gen_invariant.c | 0
.../{oracle => oracle_ci}/gen_labeled_stmt.c | 0
.../{oracle => oracle_ci}/gen_lazy.c | 0
.../{oracle => oracle_ci}/gen_loop.c | 0
.../gen_nested_code_annot.c | 0
.../{oracle => oracle_ci}/gen_result.c | 0
.../{oracle => oracle_ci}/gen_stmt_contract.c | 0
.../{oracle => oracle_ci}/gen_true.c | 0
.../{oracle => oracle_ci}/gen_typedef.c | 0
.../{oracle => oracle_ci}/ghost.res.oracle | 0
.../invariant.res.oracle | 0
.../labeled_stmt.res.oracle | 0
.../{oracle => oracle_ci}/lazy.res.oracle | 0
.../{oracle => oracle_ci}/loop.res.oracle | 0
.../nested_code_annot.res.oracle | 0
.../{oracle => oracle_ci}/result.res.oracle | 0
.../stmt_contract.res.oracle | 0
.../{oracle => oracle_ci}/true.res.oracle | 0
.../{oracle => oracle_ci}/typedef.res.oracle | 0
.../e-acsl/tests/memory/ctype_macros.c | 2 +-
src/plugins/e-acsl/tests/memory/local_init.c | 2 +-
.../tests/memory/oracle/gen_decl_in_switch.c | 24 ---
.../{oracle => oracle_ci}/addrOf.res.oracle | 0
.../{oracle => oracle_ci}/alias.res.oracle | 0
.../base_addr.res.oracle | 0
.../block_length.res.oracle | 0
.../block_valid.res.oracle | 0
.../bypassed_var.res.oracle | 0
.../{oracle => oracle_ci}/call.res.oracle | 0
.../compound_initializers.res.oracle | 0
.../constructor.res.oracle | 0
.../ctype_macros.res.oracle | 0
.../decl_in_switch.err.oracle | 0
.../decl_in_switch.res.oracle | 0
.../early_exit.res.oracle | 0
.../{oracle => oracle_ci}/errno.res.oracle | 0
.../{oracle => oracle_ci}/freeable.res.oracle | 0
.../memory/{oracle => oracle_ci}/gen_addrOf.c | 0
.../memory/{oracle => oracle_ci}/gen_alias.c | 0
.../{oracle => oracle_ci}/gen_base_addr.c | 0
.../{oracle => oracle_ci}/gen_block_length.c | 0
.../{oracle => oracle_ci}/gen_block_valid.c | 0
.../{oracle => oracle_ci}/gen_bypassed_var.c | 0
.../memory/{oracle => oracle_ci}/gen_call.c | 0
.../gen_compound_initializers.c | 0
.../{oracle => oracle_ci}/gen_constructor.c | 0
.../{oracle => oracle_ci}/gen_ctype_macros.c | 0
.../memory/oracle_ci/gen_decl_in_switch.c | 146 ++++++++++++++++++
.../{oracle => oracle_ci}/gen_early_exit.c | 0
.../memory/{oracle => oracle_ci}/gen_errno.c | 0
.../{oracle => oracle_ci}/gen_freeable.c | 0
.../memory/{oracle => oracle_ci}/gen_goto.c | 0
.../{oracle => oracle_ci}/gen_hidden_malloc.c | 0
.../memory/{oracle => oracle_ci}/gen_init.c | 0
.../{oracle => oracle_ci}/gen_init_function.c | 0
.../{oracle => oracle_ci}/gen_initialized.c | 0
.../gen_literal_string.c | 0
.../{oracle => oracle_ci}/gen_local_goto.c | 0
.../{oracle => oracle_ci}/gen_local_init.c | 0
.../{oracle => oracle_ci}/gen_local_var.c | 0
.../{oracle => oracle_ci}/gen_mainargs.c | 0
.../{oracle => oracle_ci}/gen_memalign.c | 0
.../{oracle => oracle_ci}/gen_memsize.c | 0
.../memory/{oracle => oracle_ci}/gen_null.c | 0
.../memory/{oracle => oracle_ci}/gen_offset.c | 0
.../gen_other_constants.c | 0
.../memory/{oracle => oracle_ci}/gen_ptr.c | 0
.../{oracle => oracle_ci}/gen_ptr_init.c | 0
.../gen_ranges_in_builtins.c | 0
.../memory/{oracle => oracle_ci}/gen_sizeof.c | 0
.../memory/{oracle => oracle_ci}/gen_stdout.c | 0
.../memory/{oracle => oracle_ci}/gen_valid.c | 0
.../{oracle => oracle_ci}/gen_valid_alias.c | 0
.../gen_valid_in_contract.c | 0
.../memory/{oracle => oracle_ci}/gen_vector.c | 0
.../memory/{oracle => oracle_ci}/gen_vla.c | 0
.../{oracle => oracle_ci}/goto.res.oracle | 0
.../hidden_malloc.res.oracle | 0
.../{oracle => oracle_ci}/init.res.oracle | 0
.../init_function.res.oracle | 0
.../initialized.res.oracle | 0
.../literal_string.res.oracle | 0
.../local_goto.res.oracle | 0
.../local_init.res.oracle | 0
.../local_var.res.oracle | 0
.../{oracle => oracle_ci}/mainargs.res.oracle | 0
.../{oracle => oracle_ci}/memalign.res.oracle | 0
.../{oracle => oracle_ci}/memsize.res.oracle | 0
.../{oracle => oracle_ci}/null.res.oracle | 0
.../{oracle => oracle_ci}/offset.res.oracle | 0
.../other_constants.res.oracle | 0
.../{oracle => oracle_ci}/ptr.res.oracle | 0
.../{oracle => oracle_ci}/ptr_init.res.oracle | 0
.../ranges_in_builtins.res.oracle | 0
.../{oracle => oracle_ci}/sizeof.res.oracle | 0
.../{oracle => oracle_ci}/stdout.res.oracle | 0
.../{oracle => oracle_ci}/valid.res.oracle | 0
.../valid_alias.res.oracle | 0
.../valid_in_contract.res.oracle | 0
.../{oracle => oracle_ci}/vector.res.oracle | 0
.../{oracle => oracle_ci}/vla.res.oracle | 0
.../e-acsl/tests/memory/result/.gitkeep | 0
src/plugins/e-acsl/tests/special/builtin.i | 9 +-
.../e-acsl/tests/special/e-acsl-functions.c | 4 +-
.../e-acsl/tests/special/e-acsl-instrument.c | 4 +-
.../e-acsl/tests/special/e-acsl-valid.c | 8 +-
.../tests/special/oracle/builtin.0.res.oracle | 5 -
.../tests/special/oracle/builtin.1.res.oracle | 5 -
.../special/oracle/e-acsl-valid.0.res.oracle | 21 ---
.../special/oracle/e-acsl-valid.1.res.oracle | 18 ---
.../tests/special/oracle/gen_builtin2.c | 58 -------
.../tests/special/oracle/gen_e-acsl-valid2.c | 116 --------------
.../special/oracle_ci/builtin.res.oracle | 4 +
.../e-acsl-functions.res.oracle | 0
.../e-acsl-instrument.res.oracle | 4 +
.../special/oracle_ci/e-acsl-valid.res.oracle | 40 +++++
.../{oracle => oracle_ci}/gen_builtin.c | 2 +-
.../gen_e-acsl-functions.c | 0
.../gen_e-acsl-instrument.c | 1 +
.../{oracle => oracle_ci}/gen_e-acsl-valid.c | 0
.../{oracle => oracle_ci}/gen_t_addr-by-val.c | 0
.../{oracle => oracle_ci}/gen_t_args.c | 0
.../{oracle => oracle_ci}/gen_t_array.c | 0
.../{oracle => oracle_ci}/gen_t_char.c | 0
.../{oracle => oracle_ci}/gen_t_darray.c | 0
.../{oracle => oracle_ci}/gen_t_dpointer.c | 0
.../{oracle => oracle_ci}/gen_t_fptr.c | 0
.../{oracle => oracle_ci}/gen_t_fun_lib.c | 0
.../{oracle => oracle_ci}/gen_t_fun_ptr.c | 0
.../{oracle => oracle_ci}/gen_t_getenv.c | 0
.../{oracle => oracle_ci}/gen_t_global_init.c | 0
.../{oracle => oracle_ci}/gen_t_labels.c | 0
.../{oracle => oracle_ci}/gen_t_lit_string.c | 0
.../{oracle => oracle_ci}/gen_t_local_init.c | 0
.../{oracle => oracle_ci}/gen_t_malloc-asan.c | 0
.../{oracle => oracle_ci}/gen_t_malloc.c | 0
.../{oracle => oracle_ci}/gen_t_memcpy.c | 0
.../{oracle => oracle_ci}/gen_t_scope.c | 0
.../{oracle => oracle_ci}/gen_t_struct.c | 0
.../{oracle => oracle_ci}/gen_t_while.c | 0
.../t_addr-by-val.res.oracle | 0
.../{oracle => oracle_ci}/t_args.res.oracle | 0
.../{oracle => oracle_ci}/t_array.res.oracle | 0
.../{oracle => oracle_ci}/t_char.res.oracle | 0
.../{oracle => oracle_ci}/t_darray.res.oracle | 0
.../t_dpointer.res.oracle | 0
.../{oracle => oracle_ci}/t_fptr.res.oracle | 0
.../t_fun_lib.res.oracle | 0
.../t_fun_ptr.res.oracle | 0
.../{oracle => oracle_ci}/t_getenv.res.oracle | 0
.../t_global_init.res.oracle | 0
.../{oracle => oracle_ci}/t_labels.res.oracle | 0
.../t_lit_string.res.oracle | 0
.../t_local_init.res.oracle | 0
.../t_malloc-asan.res.oracle | 0
.../{oracle => oracle_ci}/t_malloc.res.oracle | 0
.../{oracle => oracle_ci}/t_memcpy.res.oracle | 0
.../{oracle => oracle_ci}/t_scope.res.oracle | 0
.../{oracle => oracle_ci}/t_struct.res.oracle | 0
.../{oracle => oracle_ci}/t_while.res.oracle | 0
.../temporal/{test_config => test_config_ci} | 0
.../{test_config.in => test_config_ci.in} | 0
src/plugins/e-acsl/tests/test_config_dev.in | 12 ++
289 files changed, 253 insertions(+), 287 deletions(-)
rename src/plugins/e-acsl/{tests/memory => known_bugs}/decl_in_switch.c (94%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/arith.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/array.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/at.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/at_on-purely-logic-variables.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/cast.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/comparison.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/functions.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/functions_rec.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_arith.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_array.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_at.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_at_on-purely-logic-variables.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_cast.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_comparison.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_functions.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_functions_rec.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_integer_constant.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_let.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_longlong.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_not.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_quantif.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/gen_rationals.c (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/integer_constant.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/let.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/longlong.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/not.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/quantif.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{oracle => oracle_ci}/rationals.res.oracle (100%)
rename src/plugins/e-acsl/tests/arith/{result => result_ci}/.gitkeep (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1304.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1307.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1324.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1326.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1390.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1395.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1398.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1399.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1478.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1700.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1717.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1718.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1740.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts1837.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2191.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2192.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2231.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2252.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2305.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2386.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/bts2406.res.oracle (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1304.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1307.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1324.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1326.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1390.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1395.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1398.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1399.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1478.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1700.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1717.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1718.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1740.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts1837.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2191.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2192.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2231.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2252.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2305.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2386.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_bts2406.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/gen_issue69.c (100%)
rename src/plugins/e-acsl/tests/bts/{oracle => oracle_ci}/issue69.res.oracle (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/gen_strcat.c (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/gen_strcmp.c (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/gen_strcpy.c (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/gen_strlen.c (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/strcat.res.oracle (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/strcmp.res.oracle (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/strcpy.res.oracle (100%)
rename src/plugins/e-acsl/tests/builtin/{oracle => oracle_ci}/strlen.res.oracle (100%)
rename src/plugins/e-acsl/tests/builtin/{test_config => test_config_ci} (100%)
rename src/plugins/e-acsl/tests/examples/{oracle => oracle_ci}/functions_contiki.res.oracle (100%)
rename src/plugins/e-acsl/tests/examples/{oracle => oracle_ci}/gen_functions_contiki.c (100%)
rename src/plugins/e-acsl/tests/examples/{oracle => oracle_ci}/gen_linear_search.c (100%)
rename src/plugins/e-acsl/tests/examples/{oracle => oracle_ci}/linear_search.res.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/fprintf.res.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/gen_fprintf.c (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/gen_printf.c (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/gen_printf2.c (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/printf.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/printf.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/printf.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/printf.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/printf.err.oracle (100%)
rename src/plugins/e-acsl/tests/format/{oracle => oracle_ci}/printf.res.oracle (100%)
rename src/plugins/e-acsl/tests/format/{test_config => test_config_ci} (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/addrOf.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/addrOf.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/addrOf.res.oracle (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/gen_addrOf.c (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/gen_addrOf2.c (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/gen_let-alias.c (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{oracle => oracle_ci}/let-alias.res.oracle (100%)
rename src/plugins/e-acsl/tests/full-mmodel/{test_config => test_config_ci} (100%)
rename src/plugins/e-acsl/tests/gmp-only/{oracle => oracle_ci}/arith.res.oracle (100%)
rename src/plugins/e-acsl/tests/gmp-only/{oracle => oracle_ci}/functions.res.oracle (100%)
rename src/plugins/e-acsl/tests/gmp-only/{oracle => oracle_ci}/gen_arith.c (100%)
rename src/plugins/e-acsl/tests/gmp-only/{oracle => oracle_ci}/gen_functions.c (100%)
rename src/plugins/e-acsl/tests/gmp-only/{test_config => test_config_ci} (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/false.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/function_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_false.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_function_contract.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_ghost.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_invariant.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_labeled_stmt.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_lazy.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_loop.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_nested_code_annot.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_result.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_stmt_contract.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_true.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/gen_typedef.c (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/ghost.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/invariant.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/labeled_stmt.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/lazy.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/loop.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/nested_code_annot.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/result.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/stmt_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/true.res.oracle (100%)
rename src/plugins/e-acsl/tests/language_constructs/{oracle => oracle_ci}/typedef.res.oracle (100%)
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/addrOf.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/alias.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/base_addr.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/block_length.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/block_valid.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/bypassed_var.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/call.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/compound_initializers.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/constructor.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/ctype_macros.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/decl_in_switch.err.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/decl_in_switch.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/early_exit.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/errno.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/freeable.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_addrOf.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_alias.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_base_addr.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_block_length.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_block_valid.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_bypassed_var.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_call.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_compound_initializers.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_constructor.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_ctype_macros.c (100%)
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_early_exit.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_errno.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_freeable.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_goto.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_hidden_malloc.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_init.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_init_function.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_initialized.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_literal_string.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_local_goto.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_local_init.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_local_var.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_mainargs.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_memalign.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_memsize.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_null.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_offset.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_other_constants.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_ptr.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_ptr_init.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_ranges_in_builtins.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_sizeof.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_stdout.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_valid.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_valid_alias.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_valid_in_contract.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_vector.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/gen_vla.c (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/goto.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/hidden_malloc.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/init.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/init_function.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/initialized.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/literal_string.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/local_goto.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/local_init.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/local_var.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/mainargs.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/memalign.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/memsize.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/null.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/offset.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/other_constants.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/ptr.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/ptr_init.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/ranges_in_builtins.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/sizeof.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/stdout.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/valid.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/valid_alias.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/valid_in_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/vector.res.oracle (100%)
rename src/plugins/e-acsl/tests/memory/{oracle => oracle_ci}/vla.res.oracle (100%)
delete mode 100644 src/plugins/e-acsl/tests/memory/result/.gitkeep
delete mode 100644 src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
delete mode 100644 src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle
rename src/plugins/e-acsl/tests/special/{oracle => oracle_ci}/e-acsl-functions.res.oracle (100%)
rename src/plugins/e-acsl/tests/special/{oracle => oracle_ci}/e-acsl-instrument.res.oracle (81%)
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
rename src/plugins/e-acsl/tests/special/{oracle => oracle_ci}/gen_builtin.c (93%)
rename src/plugins/e-acsl/tests/special/{oracle => oracle_ci}/gen_e-acsl-functions.c (100%)
rename src/plugins/e-acsl/tests/special/{oracle => oracle_ci}/gen_e-acsl-instrument.c (98%)
rename src/plugins/e-acsl/tests/special/{oracle => oracle_ci}/gen_e-acsl-valid.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_addr-by-val.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_args.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_array.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_char.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_darray.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_dpointer.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_fptr.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_fun_lib.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_fun_ptr.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_getenv.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_global_init.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_labels.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_lit_string.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_local_init.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_malloc-asan.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_malloc.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_memcpy.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_scope.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_struct.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/gen_t_while.c (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_addr-by-val.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_args.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_array.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_char.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_darray.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_dpointer.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_fptr.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_fun_lib.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_fun_ptr.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_getenv.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_global_init.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_labels.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_lit_string.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_local_init.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_malloc-asan.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_malloc.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_memcpy.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_scope.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_struct.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{oracle => oracle_ci}/t_while.res.oracle (100%)
rename src/plugins/e-acsl/tests/temporal/{test_config => test_config_ci} (100%)
rename src/plugins/e-acsl/tests/{test_config.in => test_config_ci.in} (100%)
create mode 100644 src/plugins/e-acsl/tests/test_config_dev.in
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 38cfd116691..f5ee39fdfac 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -54,7 +54,9 @@
/tests/*.annot
/tests/*_DEP
/tests/test_config
-/tests/*/result/*
+/tests/test_config_ci
+/tests/test_config_dev
+/tests/*/result*/*
/tests/check/obj/*
.frama-c
tests/ptests_config
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c65ee7fc37a..587c8d50c53 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -181,27 +181,37 @@ PLUGIN_TESTS_DIRS := \
format \
temporal \
special
-
# [JS 2019/02/26] deactivate tests 'builtin' as long as setjmp/longjmp is not
# supported.
-# builtin \
+# builtin
+
+PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.cmxs
+
+DEV=
+ifeq ("$(DEV)","yes")
+ EACSL_TEST_CONFIG=dev
+else
+ EACSL_TEST_CONFIG:=ci
+endif
+PLUGIN_PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG)
-PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
-E_ACSL_TESTS: $(EACSL_PLUGIN_DIR)/tests/test_config
+E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: \
+ $(EACSL_PLUGIN_DIR)/tests/ptests_config \
+ $(EACSL_PLUGIN_DIR)/tests/test_config_$(EACSL_TEST_CONFIG)
-E_ACSL_DEFAULT_TESTS: \
- $(EACSL_PLUGIN_DIR)/tests/test_config \
- $(EACSL_PLUGIN_DIR)/tests/print.cmxs \
- $(EACSL_PLUGIN_DIR)/tests/print.cmo
+$(EACSL_PLUGIN_DIR)/tests/test_config_ci: \
+ $(EACSL_PLUGIN_DIR)/tests/test_config_ci.in \
+ $(EACSL_PLUGIN_DIR)/Makefile
+ $(PRINT_MAKING) $@
+ $(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
-$(EACSL_PLUGIN_DIR)/tests/test_config: \
- $(EACSL_PLUGIN_DIR)/tests/test_config.in \
+$(EACSL_PLUGIN_DIR)/tests/test_config_dev: \
+ $(EACSL_PLUGIN_DIR)/tests/test_config_dev.in \
$(EACSL_PLUGIN_DIR)/Makefile
$(PRINT_MAKING) $@
$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
-tests:: $(EACSL_PLUGIN_DIR)/tests/ptests_config \
- $(EACSL_PLUGIN_DIR)/tests/print.cmxs
+tests:: $(EACSL_PLUGIN_DIR)/tests/ptests_config
clean::
for d in $(E_ACSL_EXTRA_DIRS); do \
diff --git a/src/plugins/e-acsl/tests/memory/decl_in_switch.c b/src/plugins/e-acsl/known_bugs/decl_in_switch.c
similarity index 94%
rename from src/plugins/e-acsl/tests/memory/decl_in_switch.c
rename to src/plugins/e-acsl/known_bugs/decl_in_switch.c
index 4914dfe74a3..16ddbbf61bb 100644
--- a/src/plugins/e-acsl/tests/memory/decl_in_switch.c
+++ b/src/plugins/e-acsl/known_bugs/decl_in_switch.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
DONTRUN:
COMMENT: Variables declared in the body of switch statements so far cannot
COMMENT: be tracked
diff --git a/src/plugins/e-acsl/tests/arith/array.i b/src/plugins/e-acsl/tests/arith/array.i
index 8e988f14f86..6211cf09501 100644
--- a/src/plugins/e-acsl/tests/arith/array.i
+++ b/src/plugins/e-acsl/tests/arith/array.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: arrays
STDOPT: #"-slevel 5"
*/
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index f875751830f..8feb6f4e59d 100644
--- a/src/plugins/e-acsl/tests/arith/functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/functions_rec.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: recursive logic functions
STDOPT: +"-eva-ignore-recursive-calls"
*/
diff --git a/src/plugins/e-acsl/tests/arith/longlong.i b/src/plugins/e-acsl/tests/arith/longlong.i
index e013c42e76b..9be4c44511b 100644
--- a/src/plugins/e-acsl/tests/arith/longlong.i
+++ b/src/plugins/e-acsl/tests/arith/longlong.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: upgrading longlong to GMP
STDOPT: +"-eva-ignore-recursive-calls"
*/
diff --git a/src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/array.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/at.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/cast.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/cast.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/comparison.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/comparison.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/functions.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/functions.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_array.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_at.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_let.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_not.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/integer_constant.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/integer_constant.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/let.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/let.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/not.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/not.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/not.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/not.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/result/.gitkeep b/src/plugins/e-acsl/tests/arith/result_ci/.gitkeep
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/result/.gitkeep
rename to src/plugins/e-acsl/tests/arith/result_ci/.gitkeep
diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i
index 6b82653a96b..ef01c83d78b 100644
--- a/src/plugins/e-acsl/tests/bts/bts1395.i
+++ b/src/plugins/e-acsl/tests/bts/bts1395.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: recursive function
STDOPT: +"-eva-ignore-recursive-calls"
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1304.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1304.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1326.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1326.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1399.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1399.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1478.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1478.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1700.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1700.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1717.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1717.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1718.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1718.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1740.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1740.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1837.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1837.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2191.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2191.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2231.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2231.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2305.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2305.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2386.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2386.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2406.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2406.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue69.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/issue69.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/test_config b/src/plugins/e-acsl/tests/builtin/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/test_config
rename to src/plugins/e-acsl/tests/builtin/test_config_ci
diff --git a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_ci/functions_contiki.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
rename to src/plugins/e-acsl/tests/examples/oracle_ci/functions_contiki.res.oracle
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
rename to src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
rename to src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
diff --git a/src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle
rename to src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
rename to src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/gen_printf.c
rename to src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf2.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/gen_printf2.c
rename to src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.0.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.0.err.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.0.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.0.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.1.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.1.err.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.1.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.1.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.err.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.err.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/printf.c b/src/plugins/e-acsl/tests/format/printf.c
index 2bfcc362380..79b0538a529 100644
--- a/src/plugins/e-acsl/tests/format/printf.c
+++ b/src/plugins/e-acsl/tests/format/printf.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: Check detection of format-string vulnerabilities via printf
DONTRUN:
*/
diff --git a/src/plugins/e-acsl/tests/format/test_config b/src/plugins/e-acsl/tests/format/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/format/test_config
rename to src/plugins/e-acsl/tests/format/test_config_ci
diff --git a/src/plugins/e-acsl/tests/full-mmodel/let-alias.c b/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
index e21140b0295..c1c5817fe5b 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
@@ -6,6 +6,5 @@ int main(void) {
int t[4] = {1,2,3,4};
/*@ assert \let u = t + 1; *(u + 2) == 4; */ ;
/*@ assert (\let u = t + 1; *(u + 2)) == 4; */ ;
-
return 0;
}
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_let-alias.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/gen_let-alias.c
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/let-alias.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/let-alias.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config b/src/plugins/e-acsl/tests/full-mmodel/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/test_config
rename to src/plugins/e-acsl/tests/full-mmodel/test_config_ci
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config b/src/plugins/e-acsl/tests/gmp-only/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/test_config
rename to src/plugins/e-acsl/tests/gmp-only/test_config_ci
diff --git a/src/plugins/e-acsl/tests/language_constructs/invariant.i b/src/plugins/e-acsl/tests/language_constructs/invariant.i
index 5cf1d227529..76cbdb63c71 100644
--- a/src/plugins/e-acsl/tests/language_constructs/invariant.i
+++ b/src/plugins/e-acsl/tests/language_constructs/invariant.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: invariant
STDOPT: +"-slevel 11"
*/
diff --git a/src/plugins/e-acsl/tests/language_constructs/loop.i b/src/plugins/e-acsl/tests/language_constructs/loop.i
index 329c01164f9..4b0b3193ee1 100644
--- a/src/plugins/e-acsl/tests/language_constructs/loop.i
+++ b/src/plugins/e-acsl/tests/language_constructs/loop.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: loop invariants
STDOPT: +"-slevel 160"
*/
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/false.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/false.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/false.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/false.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/function_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/function_contract.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/function_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_false.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_false.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_false.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_false.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_function_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_function_contract.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_function_contract.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_ghost.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_ghost.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_invariant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_invariant.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_invariant.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_labeled_stmt.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_labeled_stmt.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_labeled_stmt.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_lazy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_lazy.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_lazy.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_loop.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_loop.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_loop.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_loop.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_nested_code_annot.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_nested_code_annot.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_nested_code_annot.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_result.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_result.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_result.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_result.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_stmt_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_stmt_contract.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_stmt_contract.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_true.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_true.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_true.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_true.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_typedef.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_typedef.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_typedef.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/ghost.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/ghost.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/ghost.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/invariant.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/invariant.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/invariant.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/labeled_stmt.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/labeled_stmt.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/labeled_stmt.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/lazy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/lazy.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/lazy.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/nested_code_annot.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/nested_code_annot.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/nested_code_annot.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/result.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/result.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/result.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/result.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/stmt_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/stmt_contract.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/stmt_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/true.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/true.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/true.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/true.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/typedef.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/typedef.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/typedef.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/ctype_macros.c b/src/plugins/e-acsl/tests/memory/ctype_macros.c
index 664996beecc..c5f033b1ddc 100644
--- a/src/plugins/e-acsl/tests/memory/ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/ctype_macros.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: Tests for function-based implementation of ctype.h features
*/
diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c
index 2c7440cdb2f..3f088213229 100644
--- a/src/plugins/e-acsl/tests/memory/local_init.c
+++ b/src/plugins/e-acsl/tests/memory/local_init.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: test of a local initializer which contains an annotation
LOG: gen_@PTEST_NAME@.c
STDOPT: #"-lib-entry -eva -e-acsl-prepare -e-acsl-share ./share/e-acsl -then -no-lib-entry"
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
deleted file mode 100644
index 15d0281d5ae..00000000000
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Generated by Frama-C */
-int main(int argc, char **argv)
-{
- int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
- __e_acsl_store_block((void *)(& argc),4UL);
- {
- int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- switch (argc) {
- default: ;
- __e_acsl_full_init((void *)(& p));
- p = & argc;
- break;
- }
- __e_acsl_delete_block((void *)(& p));
- }
- __retres = 0;
- __e_acsl_delete_block((void *)(& argc));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/addrOf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/addrOf.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/base_addr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/base_addr.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/block_length.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/block_length.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/block_valid.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/block_valid.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/bypassed_var.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/bypassed_var.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/call.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/call.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/call.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/call.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/compound_initializers.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/compound_initializers.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.err.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.err.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/early_exit.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/early_exit.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/errno.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/errno.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/freeable.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/freeable.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_call.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
new file mode 100644
index 00000000000..44c5d1497e4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
@@ -0,0 +1,146 @@
+/* Generated by Frama-C */
+typedef unsigned long size_t;
+struct __e_acsl_mpz_struct {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
+typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
+struct __e_acsl_mpq_struct {
+ __e_acsl_mpz_struct _mp_num ;
+ __e_acsl_mpz_struct _mp_den ;
+};
+typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
+typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
+typedef struct _IO_FILE FILE;
+/*@ ghost extern int __e_acsl_init; */
+
+extern size_t __e_acsl_heap_allocation_size;
+
+typedef unsigned short __uint16_t;
+typedef unsigned int __uint32_t;
+typedef unsigned long __uint64_t;
+typedef long __off_t;
+typedef long __off64_t;
+struct _IO_FILE;
+typedef void _IO_lock_t;
+struct _IO_marker {
+ struct _IO_marker *_next ;
+ struct _IO_FILE *_sbuf ;
+ int _pos ;
+};
+struct _IO_FILE {
+ int _flags ;
+ char *_IO_read_ptr ;
+ char *_IO_read_end ;
+ char *_IO_read_base ;
+ char *_IO_write_base ;
+ char *_IO_write_ptr ;
+ char *_IO_write_end ;
+ char *_IO_buf_base ;
+ char *_IO_buf_end ;
+ char *_IO_save_base ;
+ char *_IO_backup_base ;
+ char *_IO_save_end ;
+ struct _IO_marker *_markers ;
+ struct _IO_FILE *_chain ;
+ int _fileno ;
+ int _flags2 ;
+ __off_t _old_offset ;
+ unsigned short _cur_column ;
+ signed char _vtable_offset ;
+ char _shortbuf[1] ;
+ _IO_lock_t *_lock ;
+ __off64_t _offset ;
+ void *__pad1 ;
+ void *__pad2 ;
+ void *__pad3 ;
+ void *__pad4 ;
+ size_t __pad5 ;
+ int _mode ;
+ char _unused2[((unsigned long)15 * sizeof(int) - (unsigned long)4 * sizeof(void *)) - sizeof(size_t)] ;
+};
+/* compiler builtin:
+ unsigned int __builtin_bswap32(unsigned int); */
+/* compiler builtin:
+ unsigned long __builtin_bswap64(unsigned long); */
+__inline static unsigned int __bswap_32(unsigned int __bsx)
+{
+ unsigned int tmp;
+ tmp = __builtin_bswap32(__bsx);
+ return tmp;
+}
+
+__inline static __uint64_t __bswap_64(__uint64_t __bsx)
+{
+ __uint64_t tmp;
+ tmp = __builtin_bswap64(__bsx);
+ return tmp;
+}
+
+__inline static __uint16_t __uint16_identity(__uint16_t __x)
+{
+ return __x;
+}
+
+__inline static __uint32_t __uint32_identity(__uint32_t __x)
+{
+ return __x;
+}
+
+__inline static __uint64_t __uint64_identity(__uint64_t __x)
+{
+ return __x;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__e_acsl_heap_allocation_size,L1) -
+ \at(__e_acsl_heap_allocation_size,L2) ≡ i;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_init)(
+int *x_0, char ***x_1, unsigned long x_2);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_store_block)(
+void *x_0, unsigned long x_1);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_full_init)(
+void *x_0);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_delete_block)(
+void *x_0);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_clean)(
+void);
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_store_block((void *)(& argc),4UL);
+ {
+ int *p;
+ __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),8UL);
+ switch (argc) {
+ default: ;
+ __e_acsl_full_init((void *)(& p));
+ __e_acsl_full_init((void *)(& p));
+ p = & argc;
+ break;
+ }
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& p));
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_memory_clean();
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_init.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_null.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/goto.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/goto.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/init.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/init_function.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/init_function.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/initialized.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/initialized.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/literal_string.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/literal_string.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_var.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/local_var.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/null.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/null.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/null.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/null.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/offset.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/offset.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/other_constants.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/other_constants.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ptr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ptr.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ptr_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ptr_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/sizeof.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/sizeof.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/stdout.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/stdout.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/valid.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/valid.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/valid_alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/valid_alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/valid_in_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/valid_in_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/vector.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/vector.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/result/.gitkeep b/src/plugins/e-acsl/tests/memory/result/.gitkeep
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/special/builtin.i b/src/plugins/e-acsl/tests/special/builtin.i
index d69bd72b8d5..5a4e114c542 100644
--- a/src/plugins/e-acsl/tests/special/builtin.i
+++ b/src/plugins/e-acsl/tests/special/builtin.i
@@ -1,10 +1,7 @@
-/* run.config
- LOG: gen_builtin.c
- OPT: -e-acsl-builtins incr -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c
- EXECNOW: ./scripts/testrun.sh builtin special "1" "--frama-c=@frama-c@ -F -e-acsl-builtins=incr"
- LOG: gen_builtin2.c
- OPT: -e-acsl-builtins incr -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_builtin2.c
+/* run.config_ci
COMMENT: -e-acsl-builtins
+ LOG: gen_builtin.c
+ STDOPT: #"-e-acsl-builtins incr"
*/
int incr(int);
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-functions.c b/src/plugins/e-acsl/tests/special/e-acsl-functions.c
index 4eecfd5f796..dbed3c94901 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-functions.c
@@ -1,7 +1,7 @@
-/* run.config
+/* run.config_ci
COMMENT: test option -e-acsl-functions
LOG: gen_@PTEST_NAME@.c
- OPT: -machdep gcc_x86_64 -e-acsl-functions f -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva-verbose 0 -eva
+ STDOPT: #"-e-acsl-functions f"
*/
/*@ requires \initialized(p);
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
index b0b1206198c..6fa83da7757 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
@@ -1,7 +1,7 @@
-/* run.config
+/* run.config_ci
COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
LOG: gen_@PTEST_NAME@.c
- OPT: -variadic-no-translation -machdep gcc_x86_64 -e-acsl-instrument="@@all,-uninstrument1,-uninstrument2" -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0
+ STDOPT: #"-e-acsl-instrument='@@all,-uninstrument1,-uninstrument2'"
*/
#include <stdarg.h>
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-valid.c b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
index f5582dbc7b9..0991da238f6 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
@@ -1,10 +1,8 @@
-/* run.config
+/* run.config_ci
COMMENT: test option -e-acsl-no-valid
+ DONTRUN:
LOG: gen_@PTEST_NAME@.c
- OPT: -e-acsl-prepare -val -value-verbose 0 -machdep gcc_x86_64 -then -check -e-acsl-valid -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -value-verbose 0
- EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ special "" "--frama-c=@frama-c@"
- LOG: gen_@PTEST_NAME@2.c
- OPT: -e-acsl-prepare -val -value-verbose 0 -machdep gcc_x86_64 -then -check -e-acsl-no-valid -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -value-verbose 0
+ STDOPT: #"-e-acsl-prepare -e-acsl-share ./share/e-acsl -eva -eva-verbose 0 -then -e-acsl-no-valid"
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
deleted file mode 100644
index 274bdbe69e1..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/special/builtin.i (no preprocessing)
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
deleted file mode 100644
index 274bdbe69e1..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/special/builtin.i (no preprocessing)
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
deleted file mode 100644
index 5dff555c37e..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[eva:alarm] tests/special/e-acsl-valid.c:39: Warning:
- function f: precondition \valid(y) got status unknown.
-[e-acsl] beginning translation.
-[e-acsl] tests/special/e-acsl-valid.c:27: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `variant' is not yet supported. Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:31: Warning:
- E-ACSL construct `complete behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:31: Warning:
- E-ACSL construct `disjoint behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:13: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:22: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
deleted file mode 100644
index fb7c8f0d5a3..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-[eva:alarm] tests/special/e-acsl-valid.c:39: Warning:
- function f: precondition \valid(y) got status unknown.
-[e-acsl] beginning translation.
-[e-acsl] tests/special/e-acsl-valid.c:27: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `variant' is not yet supported. Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `complete behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `disjoint behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:12: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
deleted file mode 100644
index 42faeb3e95b..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
+++ /dev/null
@@ -1,58 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-int incr(int x);
-
-/*@ ensures \result ≡ incr(\old(i)); */
-int __gen_e_acsl_f(int i);
-
-int f(int i)
-{
- int j = i + 1;
- return j;
-}
-
-int incr(int x)
-{
- int __retres;
- __retres = x + 1;
- return __retres;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int i = __gen_e_acsl_f(2);
- __retres = 0;
- return __retres;
-}
-
-/*@ ensures \result ≡ incr(\old(i)); */
-int __gen_e_acsl_f(int i)
-{
- int __gen_e_acsl_at;
- int __retres;
- __gen_e_acsl_at = i;
- __retres = f(i);
- {
- __e_acsl_mpz_t __gen_e_acsl_result;
- int __gen_e_acsl_incr_app;
- __e_acsl_mpz_t __gen_e_acsl_app;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
- __gen_e_acsl_incr_app = incr(__gen_e_acsl_at);
- __gmpz_init_set_si(__gen_e_acsl_app,(long)__gen_e_acsl_incr_app);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_app));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
- (char *)"\\result == incr(\\old(i))",12);
- __gmpz_clear(__gen_e_acsl_result);
- __gmpz_clear(__gen_e_acsl_app);
- return __retres;
- }
-}
-
-
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
deleted file mode 100644
index 1818b56a4a2..00000000000
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
+++ /dev/null
@@ -1,116 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-/*@ requires \valid(y);
- requires *x ≥ 0;
- ensures *\old(x) ≡ \old(*x) + 1;
- assigns *x;
- assigns *x \from *x, x;
-
- behavior b1:
- assumes *x ≡ 1;
- ensures *\old(x) < 0;
- assigns \nothing;
-
- behavior b2:
- assumes *x ≡ 0;
- ensures *\old(x) ≡ 1;
-
- complete behaviors b2, b1;
- disjoint behaviors b1, b2;
- */
-void __gen_e_acsl_f(int *x, int *y);
-
-void f(int *x, int *y)
-{
- /*@ requires *x ≥ 0;
- ensures 2 ≥ 1;
- assigns *x; */
- {
- {
- int __gen_e_acsl_valid_read;
- __e_acsl_store_block((void *)(& y),(size_t)8);
- __e_acsl_store_block((void *)(& x),(size_t)8);
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
- (void *)x,(void *)(& x));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
- (char *)"mem_access: \\valid_read(x)",27);
- __e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
- (char *)"*x >= 0",27);
- }
- __e_acsl_initialize((void *)x,sizeof(int));
- (*x) ++;
- __e_acsl_assert(1,(char *)"Postcondition",(char *)"f",(char *)"2 >= 1",
- 28);
- }
- {
- int i = 0;
- /*@ loop invariant 0 ≤ i ≤ 1;
- loop variant 2 - i; */
- while (i < 1) {
- /*@ assert 1 ≡ 1; */ ;
- /*@ assert \valid(y); */ ;
- i ++;
- }
- }
- __e_acsl_delete_block((void *)(& y));
- __e_acsl_delete_block((void *)(& x));
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int x = 0;
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __e_acsl_full_init((void *)(& x));
- int *y = malloc(sizeof(int));
- __e_acsl_store_block((void *)(& y),(size_t)8);
- __e_acsl_full_init((void *)(& y));
- __gen_e_acsl_f(& x,y);
- __retres = 0;
- __e_acsl_delete_block((void *)(& y));
- __e_acsl_delete_block((void *)(& x));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-/*@ requires \valid(y);
- requires *x ≥ 0;
- ensures *\old(x) ≡ \old(*x) + 1;
- assigns *x;
- assigns *x \from *x, x;
-
- behavior b1:
- assumes *x ≡ 1;
- ensures *\old(x) < 0;
- assigns \nothing;
-
- behavior b2:
- assumes *x ≡ 0;
- ensures *\old(x) ≡ 1;
-
- complete behaviors b2, b1;
- disjoint behaviors b1, b2;
- */
-void __gen_e_acsl_f(int *x, int *y)
-{
- {
- int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& y),(size_t)8);
- __e_acsl_store_block((void *)(& x),(size_t)8);
- __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
- (void *)(& y));
- __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
- (char *)"\\valid(y)",12);
- }
- f(x,y);
- __e_acsl_delete_block((void *)(& y));
- __e_acsl_delete_block((void *)(& x));
- return;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle
new file mode 100644
index 00000000000..f829e96e464
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/special/builtin.i:9: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
rename to src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
similarity index 81%
rename from src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
rename to src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
index 10d0bb2429c..aabd7fab72b 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
@@ -8,3 +8,7 @@
[e-acsl] tests/special/e-acsl-instrument.c:58: Warning:
ignoring effect of variadic function vol
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/special/e-acsl-instrument.c:44: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(&tmp);
+ (tmp from vararg)
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
new file mode 100644
index 00000000000..8a102a933b4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
@@ -0,0 +1,40 @@
+[eva:alarm] tests/special/e-acsl-valid.c:36: Warning:
+ function f: precondition \valid(y) got status unknown.
+[e-acsl] beginning translation.
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:165: Warning:
+ Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:181: Warning:
+ Neither code nor specification for function __e_acsl_mspaces_init, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:446: Warning:
+ Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:450: Warning:
+ Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:454: Warning:
+ Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:458: Warning:
+ Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:462: Warning:
+ Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:467: Warning:
+ Neither code nor specification for function __e_acsl_builtin_syslog, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:488: Warning:
+ Neither code nor specification for function __e_acsl_floating_point_exception, generating default assigns from the prototype
+[kernel] Current source was: tests/special/e-acsl-valid.c:33
+ The full backtrace is:
+ Raised at file "src/libraries/project/project.ml", line 405, characters 59-66
+ Called from file "src/main.ml", line 155, characters 14-1023
+ Called from file "src/main.ml", line 121, characters 12-34
+ Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
+ Called from file "src/main.ml", line 258, characters 11-56
+ Called from file "queue.ml", line 121, characters 6-15
+ Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 807, characters 30-76
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
+
+ Unexpected error (E_ACSL.Misc.Unregistered_library_function("__e_acsl_store_block")).
+ Please report as 'crash' at http://bts.frama-c.com/.
+ Your Frama-C version is 19.0+dev (Potassium).
+ Note that a version and a backtrace alone often do not contain enough
+ information to understand the bug. Guidelines for reporting bugs are at:
+ http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
similarity index 93%
rename from src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
index e2cb3cb4898..a1e4cd5f617 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
@@ -42,7 +42,7 @@ int __gen_e_acsl_f(int i)
__gen_e_acsl_incr_app = incr(__gen_e_acsl_at);
__e_acsl_assert(__retres == __gen_e_acsl_incr_app,
(char *)"Postcondition",(char *)"f",
- (char *)"\\result == incr(\\old(i))",12);
+ (char *)"\\result == incr(\\old(i))",9);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
similarity index 98%
rename from src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
index 36e9221c01c..b3bd734d135 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
@@ -75,6 +75,7 @@ int vol(int n , ...)
int tmp;
__builtin_va_start(vl,n);
tmp = __builtin_va_arg (vl, int);
+ /*@ assert Eva: initialization: \initialized(&tmp); */
int r = tmp;
__builtin_va_end(vl);
__retres = 1;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_addr-by-val.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_addr-by-val.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_args.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_args.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_array.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_array.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_array.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_array.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_char.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_char.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_char.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_char.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_darray.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_darray.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_darray.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_darray.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_dpointer.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_dpointer.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fptr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_fptr.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_fptr.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_ptr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_ptr.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_global_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_global_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_global_init.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_global_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_labels.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_labels.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_labels.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_labels.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_lit_string.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_lit_string.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_local_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_local_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_local_init.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_local_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_struct.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_struct.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_struct.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_struct.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_while.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_while.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/test_config b/src/plugins/e-acsl/tests/temporal/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/test_config
rename to src/plugins/e-acsl/tests/temporal/test_config_ci
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config_ci.in
similarity index 100%
rename from src/plugins/e-acsl/tests/test_config.in
rename to src/plugins/e-acsl/tests/test_config_ci.in
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
new file mode 100644
index 00000000000..7a8c9c6721a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -0,0 +1,12 @@
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: GLOBAL -machdep gcc_x86_64 -variadic-no-translation -verbose 0
+MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
+MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
+MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+LOG: gen_@PTEST_NAME@.c
+OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
+EXEC: e-acsl-gcc.sh -c -X -F="-verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run -O @DEST@.run && ./@DEST@.run.e-acsl
+FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
+COMMENT: This regex works around the tendency of Frama-C to transform
+COMMENT: absolute path into relative ones whenever the file is not too far
+COMMENT: away from cwd.
--
GitLab