From 24d43e0a3c88b1248022014771fba2b4e0cde5ff Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 9 Sep 2016 14:00:40 +0200
Subject: [PATCH] Added new test folder for exploring -eacsl-full-mmodel
instrumentation option
---
src/plugins/e-acsl/.gitignore | 12 ++--
src/plugins/e-acsl/Makefile.in | 2 +-
.../e-acsl/tests/full-mmodel/README.md | 1 +
src/plugins/e-acsl/tests/full-mmodel/addrOf.i | 18 ++++++
.../full-mmodel/oracle/addrOf.0.err.oracle | 0
.../full-mmodel/oracle/addrOf.0.res.oracle | 22 +++++++
.../full-mmodel/oracle/addrOf.1.err.oracle | 0
.../full-mmodel/oracle/addrOf.1.res.oracle | 22 +++++++
.../tests/full-mmodel/oracle/gen_addrOf.c | 44 +++++++++++++
.../tests/full-mmodel/oracle/gen_addrOf2.c | 62 +++++++++++++++++++
.../e-acsl/tests/full-mmodel/test_config | 5 ++
11 files changed, 180 insertions(+), 8 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/README.md
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/addrOf.i
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.err.oracle
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
create mode 100644 src/plugins/e-acsl/tests/full-mmodel/test_config
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 75d11316c61..9ffaed22dd9 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -54,14 +54,12 @@
/tests/*_DEP
/tests/test_config
/tests/runtime/*.cm*
-/tests/runtime/result/*.log
-/tests/runtime/result/gen_*.c
-/tests/runtime/result/gen_*.out
-/tests/reject/result/*.log
-/tests/no-main/result/*.log
+/tests/runtime/result/*
+/tests/no-main/result/*
+/tests/full-mmodel/result/*
/tests/bts/result/*
-/tests/gmp/result/*.log
-/tests/gmp/result/gen*.c
+/tests/gmp/result/*
+/tests/reject/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 b9f74b3d5b7..d0e0b8e158d 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -101,7 +101,7 @@ $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION
ifeq (@MAY_RUN_TESTS@,yes)
-PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main
+PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main full-mmodel
PLUGIN_TESTS_LIB := $(PLUGIN_DIR)/tests/print.ml
E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config
diff --git a/src/plugins/e-acsl/tests/full-mmodel/README.md b/src/plugins/e-acsl/tests/full-mmodel/README.md
new file mode 100644
index 00000000000..9e2bd153f80
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/README.md
@@ -0,0 +1 @@
+Like runtime, but also test instrumentation with --e-acsl-full-mmodel
diff --git a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
new file mode 100644
index 00000000000..c797facb0f9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: addrOf
+*/
+
+void f(){
+ int m, *u, *p;
+ u = &m;
+ p = u;
+ m = 123;
+ //@ assert \initialized(p);
+}
+
+int main(void) {
+ int x = 0;
+ f();
+ /*@ assert &x == &x; */ ;
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.err.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
new file mode 100644
index 00000000000..254eb5cf46b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
@@ -0,0 +1,22 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __e_acsl_heap_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
+[value] using specification for function __e_acsl_store_block
+[value] using specification for function __e_acsl_full_init
+[value] using specification for function __e_acsl_initialized
+[value] using specification for function __e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+[value] using specification for function __e_acsl_delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.err.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
new file mode 100644
index 00000000000..254eb5cf46b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
@@ -0,0 +1,22 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __e_acsl_heap_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
+[value] using specification for function __e_acsl_store_block
+[value] using specification for function __e_acsl_full_init
+[value] using specification for function __e_acsl_initialized
+[value] using specification for function __e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+[value] using specification for function __e_acsl_delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
new file mode 100644
index 00000000000..27863938989
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
@@ -0,0 +1,44 @@
+/* Generated by Frama-C */
+void f(void)
+{
+ int m;
+ int *u;
+ int *p;
+ __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& u),8UL);
+ __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_full_init((void *)(& u));
+ u = & m;
+ __e_acsl_full_init((void *)(& p));
+ p = u;
+ __e_acsl_full_init((void *)(& m));
+ m = 123;
+ /*@ assert \initialized(p); */
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f",
+ (char *)"\\initialized(p)",10);
+ }
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& u));
+ __e_acsl_delete_block((void *)(& m));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ x = 0;
+ f();
+ /*@ assert &x ≡ &x; */
+ __e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
+ (char *)"&x == &x",16);
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
new file mode 100644
index 00000000000..6a753014472
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
@@ -0,0 +1,62 @@
+/* Generated by Frama-C */
+void f(void)
+{
+ int m;
+ int *u;
+ int *p;
+ __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& u),8UL);
+ __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_full_init((void *)(& u));
+ u = & m;
+ __e_acsl_full_init((void *)(& p));
+ p = u;
+ __e_acsl_full_init((void *)(& m));
+ m = 123;
+ /*@ assert \initialized(p); */
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f",
+ (char *)"\\initialized(p)",10);
+ }
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& u));
+ __e_acsl_delete_block((void *)(& m));
+ return;
+}
+
+void __e_acsl_globals_init(void)
+{
+ __e_acsl_store_block((void *)(& __fc_rand_max),8UL);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ __e_acsl_store_block((void *)(& __fc_random_counter),4UL);
+ __e_acsl_full_init((void *)(& __fc_random_counter));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_globals_init();
+ __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& __retres),4UL);
+ __e_acsl_full_init((void *)(& x));
+ x = 0;
+ f();
+ /*@ assert &x ≡ &x; */
+ __e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
+ (char *)"&x == &x",16);
+ __e_acsl_full_init((void *)(& __retres));
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& __fc_rand_max));
+ __e_acsl_delete_block((void *)(& __fc_random_counter));
+ __e_acsl_delete_block((void *)(& x));
+ __e_acsl_delete_block((void *)(& __retres));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config b/src/plugins/e-acsl/tests/full-mmodel/test_config
new file mode 100644
index 00000000000..31e1db413b1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/test_config
@@ -0,0 +1,5 @@
+LOG: gen_@PTEST_NAME@.c
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel "1" "--frama-c=@frama-c@ --full-mmodel"
+LOG: gen_@PTEST_NAME@2.c
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
--
GitLab