From a056d8c46a8749480c109fcddc276656ccbca872 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 30 Mar 2017 18:25:40 +0200
Subject: [PATCH] synchronize with frama-c/frama-c!1232

---
 src/plugins/e-acsl/tests/bts/bts1399.c               | 2 +-
 src/plugins/e-acsl/tests/runtime/call.c              | 2 +-
 src/plugins/e-acsl/tests/runtime/freeable.c          | 2 +-
 src/plugins/e-acsl/tests/runtime/ghost.i             | 2 +-
 src/plugins/e-acsl/tests/runtime/localvar.c          | 2 +-
 src/plugins/e-acsl/tests/runtime/valid.c             | 2 +-
 src/plugins/e-acsl/tests/runtime/valid_alias.c       | 2 +-
 src/plugins/e-acsl/tests/runtime/valid_in_contract.c | 2 +-
 src/plugins/e-acsl/tests/runtime/vector.c            | 2 +-
 9 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/plugins/e-acsl/tests/bts/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c
index 5f879d4b6e4..3f511f5a6ce 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 5b20c0c2f65..385fc002da5 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 c6c1b02e72e..ff0a0f2be98 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 aa557a23f15..f39aaf90194 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 398d9a53f77..03f21c64d36 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 676a71097fa..817f43c78a2 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 e3d0a4b5255..2f915b4f62b 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 dce26140699..9bfa9dd5ad7 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 32772d06725..1b845b129a7 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>
-- 
GitLab