From f18cfe09437f70e195287d3cb997142c0c034fae Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 25 Nov 2011 12:12:23 +0000
Subject: [PATCH] [e-acsl] new option -e-acsl to run the plug-in
---
src/plugins/e-acsl/main.ml | 7 ++++---
src/plugins/e-acsl/options.ml | 17 ++++++++++++++---
src/plugins/e-acsl/options.mli | 1 +
.../e-acsl/tests/e-acsl-runtime/addrOf.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/arith.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/array.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/at.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/cast.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/comparison.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/empty.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/false.i | 2 +-
.../tests/e-acsl-runtime/function_contract.i | 2 +-
.../tests/e-acsl-runtime/integer_constant.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i | 2 +-
.../tests/e-acsl-runtime/nested_code_annot.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/not.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/null.i | 2 +-
.../tests/e-acsl-runtime/other_constants.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/result.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/sizeof.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/stmt_contract.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/test_config | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/true.i | 2 +-
src/plugins/e-acsl/tests/test_config.in | 2 +-
25 files changed, 41 insertions(+), 28 deletions(-)
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index a83acf3b11a..a819452f143 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -78,9 +78,10 @@ let generate_code =
generate_code
let main () =
- let s = Options.Project_name.get () in
- if s = "" then begin if Options.Check.get () then fail_check () end
- else ignore (generate_code s)
+ if Options.Run.get () then
+ ignore (generate_code (Options.Project_name.get ()))
+ else
+ if Options.Check.get () then fail_check ()
let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index 467473dec41..65219a1e602 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -36,13 +36,24 @@ module Check =
let kind = `Correctness
end)
+module Run =
+ False
+ (struct
+ let option_name = "-e-acsl"
+ let help = "generate a new project where E-ACSL annotations are \
+translated to executable C code"
+ let kind = `Correctness
+ let arg_name = "prj"
+ end)
+
module Project_name =
- EmptyString
+ String
(struct
let option_name = "-e-acsl-project"
- let help = "generate a new project <prj> from the C program where E-ACSL \
- code is transformed to C code for runtime assertion checking"
+ let help = "the name of the generated project is <prj> \
+(default to \"e-acsl\")"
let kind = `Correctness
+ let default = "e-acsl"
let arg_name = "prj"
end)
diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli
index ef8540b777e..52cb586eca0 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -24,6 +24,7 @@ open Plugin
include S (** implementation of Log.S for E-ACSL *)
module Check: Bool
+module Run: Bool
module Project_name: String
module Use_assert: Bool
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
index 51565e156ed..733255d7400 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: addrOf
- EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c && ./tests/e-acsl-runtime/result/gen_addrOf.out
+ EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c && ./tests/e-acsl-runtime/result/gen_addrOf.out
*/
int main(void) {
int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
index 0c526f6e42c..733bb1d6c65 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: arithmetic operations
COMMENT: add the last assertion when fixing BTS #751
- EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_arith.out ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
+ EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_arith.out ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i b/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
index 9900338f808..2a07bffb0ef 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: arrays
- EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
+ EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
*/
int T1[3],T2[4];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
index 6c5184c2088..15d1e7773bd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \at
- EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
+ EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
*/
int A = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
index 4dfe44dcf37..422b5c47097 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: cast
- EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
+ EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
index 1d07baab466..81af6cca1b8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: comparison operators
- EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_comparison.out ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
+ EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_comparison.out ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
index dc45301b8cf..9671d3e91f4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
@@ -1,4 +1,4 @@
/* run.config
COMMENT: empty file
- OPT: -e-acsl-check -e-acsl-project p -then-on p -print
+ OPT: -e-acsl-check -e-acsl -then-on e-acsl -print
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
index 109f5b28bc9..b5252399865 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: assert \false
- EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c && ./tests/e-acsl-runtime/result/gen_false.out
+ EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c && ./tests/e-acsl-runtime/result/gen_false.out
*/
int main(void) {
int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
index b3a7eed0542..df73c710ff0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: function contract
- EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
+ EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
*/
int X = 0, Y = 2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
index fddc7eba8cc..6d10f4a73ba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: integer constant + a stmt after the assertion
COMMENT: waiting for fixing BTS #745
- EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_integer_constant.out ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
+ EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_integer_constant.out ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
*/
int main(void) {
int x;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
index d0ef7f799a1..2fe2e58ef62 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: predicate using lazy operators
- EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
+ EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i b/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i
index 97290d82949..bb30173f60f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: structured stmt with several code annotations inside
- EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_nested_code_annot.out ./tests/e-acsl-runtime/result/gen_nested_code_annot.c -lgmp && ./tests/e-acsl-runtime/result/gen_nested_code_annot.out
+ EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_nested_code_annot.out ./tests/e-acsl-runtime/result/gen_nested_code_annot.c -lgmp && ./tests/e-acsl-runtime/result/gen_nested_code_annot.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
index 264b6c1e9ca..f43535877a5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: predicate [!p]
- EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c && ./tests/e-acsl-runtime/result/gen_not.out
+ EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c && ./tests/e-acsl-runtime/result/gen_not.out
*/
int main(void) {
int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/null.i b/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
index 656111e89ba..19cb7753a61 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: assert \null == 0
- EXECNOW: LOG gen_null.c BIN gen_null.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/null.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_null.out ./tests/e-acsl-runtime/result/gen_null.c -lgmp && ./tests/e-acsl-runtime/result/gen_null.out
+ EXECNOW: LOG gen_null.c BIN gen_null.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/null.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_null.out ./tests/e-acsl-runtime/result/gen_null.c -lgmp && ./tests/e-acsl-runtime/result/gen_null.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i b/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
index dd42af31853..f0637465796 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: non integer constants
- EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/other_constants.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_other_constants.out ./tests/e-acsl-runtime/result/gen_other_constants.c -lgmp && ./tests/e-acsl-runtime/result/gen_other_constants.out
+ EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/other_constants.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_other_constants.out ./tests/e-acsl-runtime/result/gen_other_constants.c -lgmp && ./tests/e-acsl-runtime/result/gen_other_constants.out
*/
enum bool { false, true };
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
index a0ce8cfb9e3..8edbfae858d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: pointers and pointer arithmetic
- EXECNOW: LOG gen_ptr.c BIN gen_ptr.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/ptr.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_ptr.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_ptr.out ./tests/e-acsl-runtime/result/gen_ptr.c -lgmp && ./tests/e-acsl-runtime/result/gen_ptr.out
+ EXECNOW: LOG gen_ptr.c BIN gen_ptr.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/ptr.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_ptr.out ./tests/e-acsl-runtime/result/gen_ptr.c -lgmp && ./tests/e-acsl-runtime/result/gen_ptr.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
index ade096644dd..f7d5b60114a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \result
- EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp && ./tests/e-acsl-runtime/result/gen_result.out
+ EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp && ./tests/e-acsl-runtime/result/gen_result.out
*/
/*@ ensures \result == (int)(x - x); */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i b/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
index 8c63c59874d..caa836209c6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: sizeof
- EXECNOW: LOG gen_sizeof.c BIN gen_sizeof.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/sizeof.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_sizeof.out ./tests/e-acsl-runtime/result/gen_sizeof.c -lgmp && ./tests/e-acsl-runtime/result/gen_sizeof.out
+ EXECNOW: LOG gen_sizeof.c BIN gen_sizeof.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/sizeof.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_sizeof.out ./tests/e-acsl-runtime/result/gen_sizeof.c -lgmp && ./tests/e-acsl-runtime/result/gen_sizeof.out
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
index 7cce1e5ca10..50cfc48c22d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: stmt contract
- EXECNOW: LOG gen_stmt_contract.c BIN gen_stmt_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/stmt_contract.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_stmt_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_stmt_contract.out ./tests/e-acsl-runtime/result/gen_stmt_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_stmt_contract.out
+ EXECNOW: LOG gen_stmt_contract.c BIN gen_stmt_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/stmt_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stmt_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_stmt_contract.out ./tests/e-acsl-runtime/result/gen_stmt_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_stmt_contract.out
*/
int main(void) {
int x = 0, y = 2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index 28f202ce09a..d49b6f0ad28 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1 +1 @@
-STDOPT: +"-e-acsl-project p" +"-then-on p" +"-check" +"-print" +"-val"
+STDOPT: +"-e-acsl" +"-then-on e-acsl" +"-check" +"-print" +"-val"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
index f7ce1b578c2..ab45a435f5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: assert \true
- EXECNOW: LOG gen_true.c BIN gen_true.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/true.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_true.out ./tests/e-acsl-runtime/result/gen_true.c && ./tests/e-acsl-runtime/result/gen_true.out
+ EXECNOW: LOG gen_true.c BIN gen_true.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/true.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_true.out ./tests/e-acsl-runtime/result/gen_true.c && ./tests/e-acsl-runtime/result/gen_true.out
*/
int main(void) {
int x = 0;
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index 41e30f5f24c..ce1cb611b7a 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -1,3 +1,3 @@
CMD: FRAMAC_SHARE=./share @frama-c@ -cpp-command="gcc -C -E -I${FRAMAC_SHARE}"
OPT: -e-acsl-check
-FILTER:@SEDCMD@ -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|[a-zA-Z/\\]\+frama_c_project_p_[a-z0-9]*|PROJECT_FILE|"
+FILTER:@SEDCMD@ -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|"
--
GitLab