diff --git a/tests/builtins/Longinit_sequencer.ml b/tests/builtins/Longinit_sequencer.ml
index 173d3b5062e2a0be3527edf3024c4745e5e49316..e08e24d518d009ebab3543964451095e79f1f765 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 33f24cdc7d6562f40487a3693fa2b380742edc42..36f4a7c0333c46cbd473e24fd4022abf9c670fa5 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 5bb5091919b3bbf490fef6dc3ca2b097f3a1ddf5..b09b532881c9ef6a322b5ad7292035bbdfd3d66e 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 391526efc854f48c1a227508470978787b60aa80..eab8069d1467719ea917befd946c6d86e54e894d 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 f6d55190835a819d9f92c5038cc9319379f1fea5..a16798e5ff968dd534fa977323c62e9eb59112fb 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 1076c7ca5bc3f89a20b05d2ab84271e6dd8226ab..89e1f89ae0d5a0a1eab68b623367bad8f9dcccb1 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 49102dfcfc59a49c49990330bcf851c68f8ef0c0..b990a598b0e4f9c25888f70e5a482fa9dfc4757f 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 a50b7e99b2fc4190bc771320a65cedfedc6bf7de..312e2534df54f1c9d390c49abe5465673dc598cb 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 af2dbc58d5b2eff3d0a49890a02bf98bbfc295c7..fb9377fa0041f543e133230dab5ca534fcc32b61 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 e85945c2ca8273433b7e09ae1e96223a4f761067..790ffba5e5b8e51afd50bc2b27c2eff238af28bc 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 2a0434c008580b6802e46d28c4f5627791898dc9..cac60b4be3121fe0fe79ea701fee95860d0420a3 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 08db98c71601626d53a0f0f78f31fe799cbff246..cea3250e6e112f029f374a3679b684ea6bb98eb0 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 bd9e002b64b2fc82554c3578f90877ee93a1fa45..6009ef09427d0a66ef7d56304e1b9f0f3c895e6e 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 8657eb4bd84b3077a25b7dd0b088be5c485624e6..62bb7514345e37c71f436961d11e4e42b1598d75 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 d265774bec565ed9ea9b83b45ff1620f44465221..f021a7551c10da4cd12bf630fa7df7a4b009086e 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>