From acae8026405405b3896540e3a33d09c6cc4d7545 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 3 Apr 2020 20:47:36 +0200
Subject: [PATCH] [Eva] Updates test files to use the new option
 -eva-alloc-builtin.

Uses the eva_allocate annotation in the tests that used several builtins for
different calls to the same function.
---
 tests/builtins/Longinit_sequencer.ml   |  6 +++---
 tests/builtins/alloc.c                 |  6 +++---
 tests/builtins/allocated.c             |  2 +-
 tests/builtins/calloc.c                | 10 +++++-----
 tests/builtins/free.c                  |  2 +-
 tests/builtins/from_result.c           |  4 ++--
 tests/builtins/gcc_zero_length_array.c |  2 +-
 tests/builtins/malloc-deps.c           | 17 +++++++----------
 tests/builtins/malloc.c                | 23 ++++++++++++-----------
 tests/builtins/malloc_individual.c     |  4 ++--
 tests/builtins/malloc_memexec.c        | 14 +++++---------
 tests/builtins/realloc.c               |  2 +-
 tests/builtins/realloc_imprecise.c     |  2 +-
 tests/builtins/realloc_multiple.c      |  4 ++--
 tests/libc/stdlib_c.c                  |  6 +++---
 15 files changed, 49 insertions(+), 55 deletions(-)

diff --git a/tests/builtins/Longinit_sequencer.ml b/tests/builtins/Longinit_sequencer.ml
index 173d3b5062e..e08e24d518d 100644
--- a/tests/builtins/Longinit_sequencer.ml
+++ b/tests/builtins/Longinit_sequencer.ml
@@ -35,7 +35,7 @@ let main () =
   let display_results state = Format.fprintf fmt "@[%a@]@\n" !Db.Value.display state in
   Dynamic.Parameter.String.set "" "tests/builtins/long_init.c";
   Dynamic.Parameter.String.set "-eva-save-fun-state" ("init_inner:" ^ tmpfile);
-  Dynamic.Parameter.String.set "-eva-builtin" "malloc:Frama_C_malloc_fresh";
+  Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
   Dynamic.Parameter.Bool.set "-eva-alloc-returns-null" false;
   Dynamic.Parameter.String.set "-eva-warn-key" "builtins:override=inactive";
   !Db.Value.compute ();
@@ -49,7 +49,7 @@ let main () =
   Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_inner:" ^ tmpfile);
   (* set builtins in a different order to force kernel to recompute
      kernel function IDs *)
-  Dynamic.Parameter.String.set "-eva-builtin" "malloc:Frama_C_malloc_fresh";
+  Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
   !Db.Value.compute ();
   Callgraph.Uses.iter_in_rev_order display_results;
   Files.clear ();
@@ -59,7 +59,7 @@ let main () =
   Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_outer:" ^ tmpfile);
   (* set builtins in a different order to force kernel to recompute
      kernel function IDs *)
-  Dynamic.Parameter.String.set "-eva-builtin" "malloc:Frama_C_malloc_fresh";
+  Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
   !Db.Value.compute ();
   Callgraph.Uses.iter_in_rev_order display_results;
   ok:=true (* no error, we can erase the file *)
diff --git a/tests/builtins/alloc.c b/tests/builtins/alloc.c
index 33f24cdc7d6..36f4a7c0333 100644
--- a/tests/builtins/alloc.c
+++ b/tests/builtins/alloc.c
@@ -1,10 +1,10 @@
 /* run.config*
    GCC:
-   STDOPT: #"-eva-no-builtins-auto"
-   STDOPT: #"-eva-no-builtins-auto -absolute-valid-range 0x100-0x200 -main main_abs"
+   STDOPT: #"-eva-alloc-builtin fresh"
+   STDOPT: #"-eva-alloc-builtin fresh -absolute-valid-range 0x100-0x200 -main main_abs"
 */
 
-#define malloc(n) Frama_C_malloc_fresh(n)
+
 #include "share/libc/stdlib.c"
 
 int *p,*q,*r,a,b;
diff --git a/tests/builtins/allocated.c b/tests/builtins/allocated.c
index 5bb5091919b..b09b532881c 100644
--- a/tests/builtins/allocated.c
+++ b/tests/builtins/allocated.c
@@ -1,6 +1,6 @@
 /* run.config*
    STDOPT: +"-slevel 1 -eva-mlevel 0"
-   STDOPT: +"-slevel 999 -eva-builtin malloc:Frama_C_malloc_fresh,__fc_vla_alloc:Frama_C_malloc_fresh,__fc_vla_free:Frama_C_vla_free"
+   STDOPT: +"-slevel 999 -eva-alloc-builtin fresh"
 */
 #define assert_bottom(exp) if (nondet) {exp; Frama_C_show_each_unreachable();}
 
diff --git a/tests/builtins/calloc.c b/tests/builtins/calloc.c
index 391526efc85..eab8069d146 100644
--- a/tests/builtins/calloc.c
+++ b/tests/builtins/calloc.c
@@ -1,10 +1,10 @@
 /* run.config*
  STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null"
- STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
- STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
- STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
- STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
- STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_imprecise"
+ STDOPT: #"-eva-alloc-returns-null -eva-alloc-builtin fresh"
+ STDOPT: #"-eva-alloc-returns-null -eva-alloc-builtin by_stack"
+ STDOPT: #"-eva-no-alloc-returns-null -eva-alloc-builtin fresh"
+ STDOPT: #"-eva-no-alloc-returns-null -eva-alloc-builtin by_stack"
+ STDOPT: #"-eva-no-alloc-returns-null -eva-alloc-builtin imprecise"
  */
 #include <stdlib.h>
 #include <stdint.h>
diff --git a/tests/builtins/free.c b/tests/builtins/free.c
index f6d55190835..a16798e5ff9 100644
--- a/tests/builtins/free.c
+++ b/tests/builtins/free.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #" -eva-builtin malloc:Frama_C_malloc_fresh"
+   STDOPT: #" -eva-alloc-builtin fresh"
 */
 #include "stdlib.h" 
 volatile v;
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index 1076c7ca5bc..89e1f89ae0d 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT:  @EVA_CONFIG@ -eva-no-builtins-auto -deps -journal-disable
+   OPT:  @EVA_CONFIG@ -eva-alloc-builtin fresh -deps -journal-disable
 */
-#define malloc(n) Frama_C_malloc_fresh(n)
+
 #include "../../share/libc/stdlib.c"
 
 struct T { int a; int b; };
diff --git a/tests/builtins/gcc_zero_length_array.c b/tests/builtins/gcc_zero_length_array.c
index 49102dfcfc5..b990a598b0e 100644
--- a/tests/builtins/gcc_zero_length_array.c
+++ b/tests/builtins/gcc_zero_length_array.c
@@ -1,5 +1,5 @@
 /* run.config*
-  STDOPT: +"-machdep gcc_x86_32 -eva-builtin malloc:Frama_C_malloc_fresh -slevel 11"
+  STDOPT: +"-machdep gcc_x86_32 -eva-alloc-builtin fresh -slevel 11"
  */
 #include <stdlib.h>
 
diff --git a/tests/builtins/malloc-deps.c b/tests/builtins/malloc-deps.c
index a50b7e99b2f..312e2534df5 100644
--- a/tests/builtins/malloc-deps.c
+++ b/tests/builtins/malloc-deps.c
@@ -1,31 +1,28 @@
 /* run.config*
    OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
 */
-#include <stddef.h>
-//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh(size_t n);
-//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh_weak(size_t n);
-//@ assigns \result \from \nothing;
-void *Frama_C_malloc_by_stack(size_t n);
+#include <stdlib.h>
 
 volatile int v;
 void g(int *p, int k) { p[k] = k; }
 
 void main(int i, int j) {
   int *p, *q;
-  p = Frama_C_malloc_fresh_weak(100);
+  /*@ eva_allocate fresh_weak; */
+  p = malloc(100);
   *p = i;
   *p = j; // Cannnot perform strong update for deps, variable is weak
 
-  q = Frama_C_malloc_fresh(100);
+  /*@ eva_allocate fresh; */
+  q = malloc(100);
   *q = i;
   *q = j; // Can perform strong update for deps
 
 
   int *r;
   for (int l=0; l<10; l++) {
-    r = Frama_C_malloc_by_stack((l+1)*4);
+    /*@ eva_allocate by_stack; */
+    r = malloc((l+1)*4);
     g(r, l+v); // Again, we can only perform weak updates (after iteration 1)
   }
 }
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index af2dbc58d5b..fb9377fa004 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,24 +1,23 @@
 /* run.config*
-   OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
+   OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0 -eva-alloc-builtin by_stack
 */
-#include <stddef.h>
-void *Frama_C_malloc_by_stack(size_t i);
-void *Frama_C_malloc_fresh(size_t i);
-void *Frama_C_malloc_imprecise(size_t i);
+#include <stdlib.h>
+
 void main(int c) {
   int x;
   int *s;
   if(c) {
     x = 1;
-    s = Frama_C_malloc_by_stack(100);
+    s = malloc(100);
   } else {
     x = 2;
     s = 0;
   }
 
-  int *p = Frama_C_malloc_by_stack(c);
-  int *q = Frama_C_malloc_by_stack(12);
-  int *r = Frama_C_malloc_fresh(100);
+  int *p = malloc(c);
+  int *q = malloc(12);
+  /*@ eva_allocate fresh; */
+  int *r = malloc(100);
   *p = 1;
   *(p+2) = 3;
   *(p+24999) = 4;
@@ -30,9 +29,11 @@ void main(int c) {
   *r = 1;
   *(r+2) = 3;
 
-  int *mw = Frama_C_malloc_imprecise(42);
+  /*@ eva_allocate imprecise; */
+  int *mw = malloc(42);
   *mw = 1;
-  int *mw2 = Frama_C_malloc_imprecise(42);
+  /*@ eva_allocate imprecise; */
+  int *mw2 = malloc(42);
   *mw2 = 2;
 
   //  *s = 1;
diff --git a/tests/builtins/malloc_individual.c b/tests/builtins/malloc_individual.c
index e85945c2ca8..790ffba5e5b 100644
--- a/tests/builtins/malloc_individual.c
+++ b/tests/builtins/malloc_individual.c
@@ -1,7 +1,7 @@
 /* run.config*
-   STDOPT: #"-eva-no-builtins-auto"
+   STDOPT: #"-eva-alloc-builtin fresh"
 */
-#define malloc(n) Frama_C_malloc_fresh(n)
+
 #include "share/libc/stdlib.c"
 
 int *p;
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 2a0434c0085..cac60b4be31 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,13 +1,7 @@
 /* run.config*
    OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
 */
-#include <stddef.h>
-//@ assigns \result;
-void *Frama_C_malloc_fresh(size_t n);
-
-//@ assigns \result;
-void *Frama_C_malloc_fresh_weak(size_t n);
-
+#include <stdlib.h>
 
 void f(int *p, int i) {
   *p = i;
@@ -16,7 +10,8 @@ void f(int *p, int i) {
 volatile v;
 
 void main() {
-  int *p = Frama_C_malloc_fresh (4);
+  /*@ eva_allocate fresh; */
+  int *p = malloc (4);
   if (v) {
     f(p, 2);
     f(p, 1); // This call or the corresponding one below could be cached. It is not, because we forbid memexec to take full updates to a strong variable into account for malloced bases, because they may become weak later
@@ -24,7 +19,8 @@ void main() {
     f(p, 1);
   }
 
-  int *q = Frama_C_malloc_fresh_weak (4);
+  /*@ eva_allocate fresh_weak; */
+  int *q = malloc (4);
   if (v) {
     f(q, 2);
     f(q, 1);
diff --git a/tests/builtins/realloc.c b/tests/builtins/realloc.c
index 08db98c7160..cea3250e6e1 100644
--- a/tests/builtins/realloc.c
+++ b/tests/builtins/realloc.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh -eva-warn-copy-indeterminate @all"
+   STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-warn-copy-indeterminate @all"
 */
 
 #include <stdlib.h>
diff --git a/tests/builtins/realloc_imprecise.c b/tests/builtins/realloc_imprecise.c
index bd9e002b64b..6009ef09427 100644
--- a/tests/builtins/realloc_imprecise.c
+++ b/tests/builtins/realloc_imprecise.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: +"-eva-builtin malloc:Frama_C_malloc_imprecise,realloc:Frama_C_realloc_imprecise"
+   STDOPT: +"-eva-alloc-builtin imprecise -eva-builtin realloc:Frama_C_realloc_imprecise"
 */
 
 #include <stdlib.h>
diff --git a/tests/builtins/realloc_multiple.c b/tests/builtins/realloc_multiple.c
index 8657eb4bd84..62bb7514345 100644
--- a/tests/builtins/realloc_multiple.c
+++ b/tests/builtins/realloc_multiple.c
@@ -1,6 +1,6 @@
 /* run.config*
-   STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh,realloc:Frama_C_realloc_multiple -eva-malloc-functions malloc,realloc"
-   STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh,realloc:Frama_C_realloc_multiple -eva-malloc-functions malloc,realloc -eva-alloc-returns-null"
+   STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-builtin realloc:Frama_C_realloc_multiple -eva-malloc-functions malloc,realloc"
+   STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-builtin realloc:Frama_C_realloc_multiple -eva-malloc-functions malloc,realloc -eva-alloc-returns-null"
 */
 #include <stdlib.h>
 #include "__fc_builtin.h"
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index d265774bec5..f021a7551c1 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -1,10 +1,10 @@
 /* run.config
-   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc_by_stack -eva-msg-key malloc"
-   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc_by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
+   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
+   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
    STDOPT: #"-eva-no-builtins-auto"
 */ // slevel is used to unroll loops
 
-#define malloc(n) Frama_C_malloc_by_stack(n)
+#define malloc(n) Frama_C_malloc(n)
 #include "stdlib.c"
 #include "__fc_builtin.h"
 #include <stdint.h>
-- 
GitLab