Merge branch 'feature/andre/val-builtins-list' into 'master'

synchronize with frama-c/frama-c!1232

See merge request !131

src/plugins/e-acsl/tests/bts/bts1399.c

 /* 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"

src/plugins/e-acsl/tests/runtime/call.c

 /* 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>

src/plugins/e-acsl/tests/runtime/freeable.c

 /* 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>

src/plugins/e-acsl/tests/runtime/ghost.i

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

src/plugins/e-acsl/tests/runtime/localvar.c

 /* 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>

src/plugins/e-acsl/tests/runtime/valid.c

 /* 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"

src/plugins/e-acsl/tests/runtime/valid_alias.c

 /* 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"

src/plugins/e-acsl/tests/runtime/valid_in_contract.c

 /* 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>

src/plugins/e-acsl/tests/runtime/vector.c

 /* 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>