Commit 83bf91d9 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Renames allocation builtins *_imprecise_weakest into *_imprecise.

parent 271b5b9a
......@@ -449,7 +449,7 @@ let alloc_imprecise_weakest ?returns_null region state actuals =
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () = Builtins.register_builtin
"Frama_C_malloc_imprecise_weakest" (alloc_imprecise_weakest Base.Malloc)
"Frama_C_malloc_imprecise" (alloc_imprecise_weakest Base.Malloc)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let zero_to_max_bytes () = Ival.inject_range
......@@ -601,7 +601,7 @@ let () = Builtins.register_builtin
(alloc_by_stack Base.VLA ~returns_null:false)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
"Frama_C_vla_alloc_imprecise_weakest"
"Frama_C_vla_alloc_imprecise"
(alloc_imprecise_weakest Base.VLA ~returns_null:false)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
......@@ -609,7 +609,7 @@ let () = Builtins.register_builtin
(alloc_by_stack ~prefix:"alloca" Base.Alloca ~returns_null:false)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
"Frama_C_alloca_imprecise_weakest"
"Frama_C_alloca_imprecise"
(alloc_imprecise_weakest Base.Alloca ~returns_null:false)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
......@@ -630,7 +630,7 @@ let calloc_imprecise_weakest : Db.Value.builtin = fun state actuals ->
calloc_abstract calloc_f state actuals
let () = Builtins.register_builtin
"Frama_C_calloc_imprecise_weakest" calloc_imprecise_weakest
"Frama_C_calloc_imprecise" calloc_imprecise_weakest
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
Cil.theMachine.Cil.typeOfSizeOf]))
......@@ -952,7 +952,7 @@ let realloc_imprecise_weakest state args = match args with
| _ -> raise (Builtins.Invalid_nb_of_args 2)
let () = Builtins.register_builtin
"Frama_C_realloc_imprecise_weakest" realloc_imprecise_weakest
"Frama_C_realloc_imprecise" realloc_imprecise_weakest
~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
Cil.theMachine.Cil.typeOfSizeOf]))
......
......@@ -4,7 +4,7 @@
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_weakest"
STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_imprecise"
*/
#include <stdlib.h>
#include <stdint.h>
......
......@@ -4,7 +4,7 @@
#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_weakest(size_t i);
void *Frama_C_malloc_imprecise(size_t i);
void main(int c) {
int x;
int *s;
......@@ -30,9 +30,9 @@ void main(int c) {
*r = 1;
*(r+2) = 3;
int *mw = Frama_C_malloc_imprecise_weakest(42);
int *mw = Frama_C_malloc_imprecise(42);
*mw = 1;
int *mw2 = Frama_C_malloc_imprecise_weakest(42);
int *mw2 = Frama_C_malloc_imprecise(42);
*mw2 = 1;
// *s = 1;
......
......@@ -5,24 +5,24 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] tests/builtins/calloc.c:14:
Call to builtin Frama_C_calloc_imprecise_weakest for function calloc
Call to builtin Frama_C_calloc_imprecise for function calloc
[eva:malloc:imprecise] tests/builtins/calloc.c:14: Warning:
allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
[eva] tests/builtins/calloc.c:17:
Call to builtin Frama_C_calloc_imprecise_weakest for function calloc
Call to builtin Frama_C_calloc_imprecise for function calloc
[eva] tests/builtins/calloc.c:20:
Call to builtin Frama_C_calloc_imprecise_weakest for function calloc
Call to builtin Frama_C_calloc_imprecise for function calloc
[eva] tests/builtins/calloc.c:23:
Call to builtin Frama_C_calloc_imprecise_weakest for function calloc
Call to builtin Frama_C_calloc_imprecise for function calloc
[eva:alarm] tests/builtins/calloc.c:26: Warning: assertion got status unknown.
[eva:alarm] tests/builtins/calloc.c:27: Warning: assertion got status unknown.
[eva] tests/builtins/calloc.c:30:
Call to builtin Frama_C_calloc_imprecise_weakest for function calloc
Call to builtin Frama_C_calloc_imprecise for function calloc
[eva:alarm] tests/builtins/calloc.c:33: Warning: assertion got status unknown.
[eva:alarm] tests/builtins/calloc.c:34: Warning: assertion got status unknown.
[eva:alarm] tests/builtins/calloc.c:35: Warning: assertion got status unknown.
[eva] tests/builtins/calloc.c:38:
Call to builtin Frama_C_calloc_imprecise_weakest for function calloc
Call to builtin Frama_C_calloc_imprecise for function calloc
[eva] tests/builtins/calloc.c:38: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
[eva] tests/builtins/calloc.c:40: assertion got status valid.
......
[kernel] Parsing tests/builtins/malloc.c (with preprocessing)
[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning:
Neither code nor specification for function Frama_C_malloc_fresh, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning:
Neither code nor specification for function Frama_C_malloc_imprecise_weakest, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning:
Neither code nor specification for function Frama_C_malloc_by_stack, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning:
Neither code nor specification for function Frama_C_malloc_imprecise, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -34,18 +34,14 @@
Frama_C_show_each: {{ &__malloc_main_l20 + {8} }}
[eva] tests/builtins/malloc.c:27:
Frama_C_show_each: {{ &__malloc_main_l20 + {8} }}
[eva] tests/builtins/malloc.c:33:
Call to builtin Frama_C_malloc_imprecise_weakest
[eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise
[eva:malloc:imprecise] tests/builtins/malloc.c:33: Warning:
allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
[eva] tests/builtins/malloc.c:33:
Call to builtin Frama_C_malloc_imprecise_weakest
[eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise
[eva:alarm] tests/builtins/malloc.c:34: Warning:
out of bounds write. assert \valid(mw);
[eva] tests/builtins/malloc.c:35:
Call to builtin Frama_C_malloc_imprecise_weakest
[eva] tests/builtins/malloc.c:35:
Call to builtin Frama_C_malloc_imprecise_weakest
[eva] tests/builtins/malloc.c:35: Call to builtin Frama_C_malloc_imprecise
[eva] tests/builtins/malloc.c:35: Call to builtin Frama_C_malloc_imprecise
[eva:alarm] tests/builtins/malloc.c:36: Warning:
out of bounds write. assert \valid(mw2);
[eva] Recording results for main
......
......@@ -5,19 +5,19 @@
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
[eva] tests/builtins/realloc_imprecise.c:10:
Call to builtin Frama_C_malloc_imprecise_weakest for function malloc
Call to builtin Frama_C_malloc_imprecise for function malloc
[eva:malloc:imprecise] tests/builtins/realloc_imprecise.c:10: Warning:
allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
[eva:alarm] tests/builtins/realloc_imprecise.c:11: Warning:
out of bounds write. assert \valid(p);
[eva] tests/builtins/realloc_imprecise.c:13:
Call to builtin Frama_C_realloc_imprecise_weakest for function realloc
Call to builtin Frama_C_realloc_imprecise for function realloc
[eva] tests/builtins/realloc_imprecise.c:13:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] tests/builtins/realloc_imprecise.c:13:
weak free on bases: {__alloc_w_main}
[eva] tests/builtins/realloc_imprecise.c:15:
Call to builtin Frama_C_realloc_imprecise_weakest for function realloc
Call to builtin Frama_C_realloc_imprecise for function realloc
[eva] tests/builtins/realloc_imprecise.c:15:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] tests/builtins/realloc_imprecise.c:15:
......
/* run.config*
STDOPT: +"-eva-builtin malloc:Frama_C_malloc_imprecise_weakest,realloc:Frama_C_realloc_imprecise_weakest"
STDOPT: +"-eva-builtin malloc:Frama_C_malloc_imprecise,realloc:Frama_C_realloc_imprecise"
*/
#include <stdlib.h>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment