From 2ed5e4425d0a49d52a422213a3687f761eb89f29 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 27 Nov 2012 07:49:50 +0000
Subject: [PATCH] [E-ACSL] optimizing tests again
---
src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/valid.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c | 2 +-
6 files changed, 8 insertions(+), 8 deletions(-)
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 3eb2e3333c0..0d5c159a5b4 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,7 +1,7 @@
/* run.config
COMMENT: function contract
- EXECNOW: LOG gen_function_contract.c @frama-c@ -e-acsl-share ./share/e-acsl ./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_test.sh function_contract
- EXECNOW: LOG gen_function_contract2.c @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_test.sh function_contract2
+ EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out @frama-c@ -e-acsl-share ./share/e-acsl ./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_test.sh function_contract
+ EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_test.sh function_contract2
*/
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 4d72b51f8ba..6086959108b 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
- EXECNOW: LOG gen_integer_constant.c @frama-c@ -e-acsl-share ./share/e-acsl ./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_test.sh integer_constant
- EXECNOW: LOG gen_integer_constant2.c @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
+ EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out @frama-c@ -e-acsl-share ./share/e-acsl ./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_test.sh integer_constant
+ EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
*/
int main(void) {
int x;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
index ae0498739bb..da412680b27 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: allocation and de-allocation of local variables
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
EXECNOW: LOG gen_localvar.c BIN gen_localvar.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar.c > /dev/null && ./gcc_test.sh localvar
EXECNOW: LOG gen_localvar2.c BIN gen_localvar2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar2.c > /dev/null && ./gcc_test.sh localvar2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
index 8c14c1dc41c..c74dc7aff5c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \valid
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
EXECNOW: LOG gen_valid.c BIN gen_valid.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_test.sh valid
EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_test.sh valid2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
index c9e34945da5..00b6add3803 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \valid in presence of aliasing
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
EXECNOW: LOG gen_valid_alias.c BIN gen_valid_alias.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias.c > /dev/null && ./gcc_test.sh valid_alias
EXECNOW: LOG gen_valid_alias2.c BIN gen_valid_alias2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias2.c > /dev/null && ./gcc_test.sh valid_alias2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
index 262ee31b729..63c607d1e83 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: function contract involving \valid
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
EXECNOW: LOG gen_valid_in_contract.c BIN gen_valid_in_contract.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract.c > /dev/null && ./gcc_test.sh valid_in_contract
EXECNOW: LOG gen_valid_in_contract2.c BIN gen_valid_in_contract2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract2.c > /dev/null && ./gcc_test.sh valid_in_contract2
*/
--
GitLab