From 83bf91d90caf475b170ac8b640413cf1616ea189 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 3 Apr 2020 10:15:46 +0200
Subject: [PATCH] [Eva] Renames allocation builtins *_imprecise_weakest into
*_imprecise.
---
.../value/domains/cvalue/builtins_malloc.ml | 10 +++++-----
tests/builtins/calloc.c | 2 +-
tests/builtins/malloc.c | 6 +++---
tests/builtins/oracle/calloc.5.res.oracle | 12 ++++++------
tests/builtins/oracle/malloc.res.oracle | 16 ++++++----------
.../builtins/oracle/realloc_imprecise.res.oracle | 6 +++---
tests/builtins/realloc_imprecise.c | 2 +-
7 files changed, 25 insertions(+), 29 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index aac96421d2d..2d24e1062e3 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -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]))
diff --git a/tests/builtins/calloc.c b/tests/builtins/calloc.c
index a2fed462f6c..391526efc85 100644
--- a/tests/builtins/calloc.c
+++ b/tests/builtins/calloc.c
@@ -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>
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index e208af715ad..af7f6c2470d 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -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;
diff --git a/tests/builtins/oracle/calloc.5.res.oracle b/tests/builtins/oracle/calloc.5.res.oracle
index 31723119f89..679c1f964b2 100644
--- a/tests/builtins/oracle/calloc.5.res.oracle
+++ b/tests/builtins/oracle/calloc.5.res.oracle
@@ -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.
diff --git a/tests/builtins/oracle/malloc.res.oracle b/tests/builtins/oracle/malloc.res.oracle
index 0fd1847bc24..b9dd7712077 100644
--- a/tests/builtins/oracle/malloc.res.oracle
+++ b/tests/builtins/oracle/malloc.res.oracle
@@ -1,10 +1,10 @@
[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
diff --git a/tests/builtins/oracle/realloc_imprecise.res.oracle b/tests/builtins/oracle/realloc_imprecise.res.oracle
index 7bb0194ab39..346a55355c0 100644
--- a/tests/builtins/oracle/realloc_imprecise.res.oracle
+++ b/tests/builtins/oracle/realloc_imprecise.res.oracle
@@ -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:
diff --git a/tests/builtins/realloc_imprecise.c b/tests/builtins/realloc_imprecise.c
index 3a943140d53..bd9e002b64b 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_weakest,realloc:Frama_C_realloc_imprecise_weakest"
+ STDOPT: +"-eva-builtin malloc:Frama_C_malloc_imprecise,realloc:Frama_C_realloc_imprecise"
*/
#include <stdlib.h>
--
GitLab