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 bae1b1682f26fdff0479de31f8fb7363616665fc..66fe087cc2a1038cc064ca6e3d61474ab2a3030b 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 -load-module E_ACSL ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c + EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c */ void main() { 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 3435f843a7e7d483e68d29e9399618c9913b64b1..148415d0fa41ec37b9652f88cbbd5bb37dd270e8 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 -load-module E_ACSL ./tests/e-acsl-runtime/arith.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_arith.out -lgmp ./tests/e-acsl-runtime/result/gen_arith.c + EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_arith.out -lgmp ./tests/e-acsl-runtime/result/gen_arith.c */ void main() { 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 24f7609b4a354ca4d15c9fcd412745261c03837b..d0faa4247612be309bfc735a2cfd5b7dab6fdc35 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 -load-module E_ACSL ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c + EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c */ void main() { 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 10252afb5557998ca53aaa1ab4e09f1329e3957e..7b9ede66903b9839cb88031bf0a3bfa9dbe50763 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 -load-module E_ACSL ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out -lgmp ./tests/e-acsl-runtime/result/gen_comparison.c + EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out -lgmp ./tests/e-acsl-runtime/result/gen_comparison.c */ void main() { 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 1a1a80bf026c91cb06f82083658d9e69e427b57a..cd0a76b0dd5f52a71e72528105ee6d6fa1a3a9e0 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 -load-module E_ACSL ./tests/e-acsl-runtime/false.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c + EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c */ void main() { int x = 0; 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 9e8e9105a9b81ba1ccc835d52453a51d2e5197a8..36c04c8d72e929034bef6a4aed4c7789c274bb0b 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 COMMENT: waiting for fixing BTS #745 - EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out -lgmp ./tests/e-acsl-runtime/result/gen_integer_constant.c + 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 -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out -lgmp ./tests/e-acsl-runtime/result/gen_integer_constant.c */ void main() { /*@ assert 0 == 0; */ 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 54c44a75bc5e912cf74936fcafc5eabbf44675c1..a0a15273c626c1478210c494d5e892950c6ef9de 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 -load-module E_ACSL ./tests/e-acsl-runtime/not.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c + EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c */ void main() { int x = 0; 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 aa0c1e7a7e1f8b8cfeccfe854954ad4c68a621c5..3c78f3b935d1361725bdb84573873f0f6e637714 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 -load-module E_ACSL ./tests/e-acsl-runtime/sizeof.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_sizeof.out ./tests/e-acsl-runtime/result/gen_sizeof.c + EXECNOW: LOG gen_sizeof.c BIN gen_sizeof.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/sizeof.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_sizeof.out ./tests/e-acsl-runtime/result/gen_sizeof.c */ void main() { diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i index b99966e26aac12631f66ec02cceeec73624f02cc..cfa24130520d49e2fc6e87bbec366f6bac49a928 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i @@ -1,6 +1,6 @@ /* run.config COMMENT: string literal - EXECNOW: LOG gen_string_literal.c BIN gen_string_literal.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/string_literal.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_string_literal.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_string_literal.out ./tests/e-acsl-runtime/result/gen_string_literal.c + EXECNOW: LOG gen_string_literal.c BIN gen_string_literal.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/string_literal.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_string_literal.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_string_literal.out ./tests/e-acsl-runtime/result/gen_string_literal.c */ void main() { /*@ assert "toto" != "titi"; */ 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 46f5aad15b9982aaa0bb8bbaa928339093e1d416..83615a256eddd2be21296f3c67ecf20dcdcda67d 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 -load-module E_ACSL ./tests/e-acsl-runtime/true.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_true.out ./tests/e-acsl-runtime/result/gen_true.c + EXECNOW: LOG gen_true.c BIN gen_true.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/true.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_true.out ./tests/e-acsl-runtime/result/gen_true.c */ void main() { int x = 0;