diff --git a/src/plugins/e-acsl/tests/bts/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c index 5f879d4b6e49bbd57cce4717ded771d5e59c5f49..3f511f5a6ce39c5b81800497e78872f6a12f7fbc 100644 --- a/src/plugins/e-acsl/tests/bts/bts1399.c +++ b/src/plugins/e-acsl/tests/bts/bts1399.c @@ -1,6 +1,6 @@ /* run.config COMMENT: complex fields and indexes + potential RTE in \initialized - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size,free:Frama_C_free -no-val-malloc-returns-null" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -no-val-malloc-returns-null" */ #include "stdlib.h" diff --git a/src/plugins/e-acsl/tests/runtime/call.c b/src/plugins/e-acsl/tests/runtime/call.c index 5b20c0c2f65bba5b9bb81b4e88a426b994b52bb7..385fc002da556a98c9167dcb4e447c34118275e3 100644 --- a/src/plugins/e-acsl/tests/runtime/call.c +++ b/src/plugins/e-acsl/tests/runtime/call.c @@ -1,6 +1,6 @@ /* run.config COMMENT: function call - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size,free:Frama_C_free -no-val-malloc-returns-null" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -no-val-malloc-returns-null" */ #include <stdlib.h> diff --git a/src/plugins/e-acsl/tests/runtime/freeable.c b/src/plugins/e-acsl/tests/runtime/freeable.c index c6c1b02e72ec16e7d6f224b68d30edce8195cda8..ff0a0f2be985bea65a204f5414948a8813cc58e7 100644 --- a/src/plugins/e-acsl/tests/runtime/freeable.c +++ b/src/plugins/e-acsl/tests/runtime/freeable.c @@ -1,6 +1,6 @@ /* run.config COMMENT: \freeable - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size -val-builtin free:Frama_C_free" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh -val-builtin free:Frama_C_free" */ #include <stdlib.h> diff --git a/src/plugins/e-acsl/tests/runtime/ghost.i b/src/plugins/e-acsl/tests/runtime/ghost.i index aa557a23f155216c874a3a4c02d83f975f9a455e..f39aaf901941f09f90fc62d0f7a9820e810c1cc0 100644 --- a/src/plugins/e-acsl/tests/runtime/ghost.i +++ b/src/plugins/e-acsl/tests/runtime/ghost.i @@ -1,6 +1,6 @@ /* run.config COMMENT: ghost code - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size -val-builtin free:Frama_C_free" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh -val-builtin free:Frama_C_free" */ /*@ ghost int G = 0; */ diff --git a/src/plugins/e-acsl/tests/runtime/localvar.c b/src/plugins/e-acsl/tests/runtime/localvar.c index 398d9a53f778a2f48550a5946e683f0bfdde897d..03f21c64d36d43355e0ce5e085ed3bfe1df23bbc 100644 --- a/src/plugins/e-acsl/tests/runtime/localvar.c +++ b/src/plugins/e-acsl/tests/runtime/localvar.c @@ -1,6 +1,6 @@ /* run.config COMMENT: allocation and de-allocation of local variables - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size,free:Frama_C_free -no-val-malloc-returns-null" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -no-val-malloc-returns-null" */ #include <stdlib.h> diff --git a/src/plugins/e-acsl/tests/runtime/valid.c b/src/plugins/e-acsl/tests/runtime/valid.c index 676a71097faeeeadf073d08f6f07db376957b7f3..817f43c78a2b702ae303b2da2c04593fa33db266 100644 --- a/src/plugins/e-acsl/tests/runtime/valid.c +++ b/src/plugins/e-acsl/tests/runtime/valid.c @@ -1,6 +1,6 @@ /* run.config COMMENT: \valid - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size,free:Frama_C_free -no-val-malloc-returns-null" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -no-val-malloc-returns-null" */ #include "stdlib.h" diff --git a/src/plugins/e-acsl/tests/runtime/valid_alias.c b/src/plugins/e-acsl/tests/runtime/valid_alias.c index e3d0a4b52551bcdbe486e2cf0285dbaaa45d96a8..2f915b4f62ba43719f77407fef1c0e7f85e788c6 100644 --- a/src/plugins/e-acsl/tests/runtime/valid_alias.c +++ b/src/plugins/e-acsl/tests/runtime/valid_alias.c @@ -1,6 +1,6 @@ /* run.config COMMENT: \valid in presence of aliasing - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size,free:Frama_C_free -no-val-malloc-returns-null" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -no-val-malloc-returns-null" */ #include "stdlib.h" diff --git a/src/plugins/e-acsl/tests/runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/runtime/valid_in_contract.c index dce261406997da5f135283b0689d2c6140247499..9bfa9dd5ad7b1cd15bcc4c861b64360c9e413ae7 100644 --- a/src/plugins/e-acsl/tests/runtime/valid_in_contract.c +++ b/src/plugins/e-acsl/tests/runtime/valid_in_contract.c @@ -1,6 +1,6 @@ /* run.config COMMENT: function contract involving \valid - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size -val-builtin free:Frama_C_free" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh -val-builtin free:Frama_C_free" */ #include <stdlib.h> diff --git a/src/plugins/e-acsl/tests/runtime/vector.c b/src/plugins/e-acsl/tests/runtime/vector.c index 32772d0672556c7739256dc543117f487faba2b3..1b845b129a711f3b1e3ff0573e54efd3d309be80 100644 --- a/src/plugins/e-acsl/tests/runtime/vector.c +++ b/src/plugins/e-acsl/tests/runtime/vector.c @@ -1,6 +1,6 @@ /* run.config COMMENT: function call + initialized - STDOPT: +"-val-builtin malloc:Frama_C_alloc_size,free:Frama_C_free -no-val-malloc-returns-null" + STDOPT: +"-val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -no-val-malloc-returns-null" */ #include<stdlib.h>