Added new test folder for exploring -eacsl-full-mmodel instrumentation

option

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

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
 

src/plugins/e-acsl/tests/full-mmodel/README.md

+Like runtime, but also test instrumentation with --e-acsl-full-mmodel

src/plugins/e-acsl/tests/full-mmodel/addrOf.i

+/* 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;
+}

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle

+[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

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle

+[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

src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c

+/* 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;
+}
+
+

src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c

+/* 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;
+}
+
+

src/plugins/e-acsl/tests/full-mmodel/test_config

+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