From ba1b5a77d8cac325a2a8f89ec261616e298045d1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 20 Jan 2020 19:05:15 +0100
Subject: [PATCH] [Eva] add typing checks for malloc builtins; fix some tests
---
src/plugins/value/domains/cvalue/builtins.ml | 4 +-
.../value/domains/cvalue/builtins_malloc.ml | 35 ++++++--
.../builtins/{malloc-deps.i => malloc-deps.c} | 8 +-
tests/builtins/malloc-optimistic.c | 4 +-
tests/builtins/malloc.c | 6 +-
tests/builtins/malloc_memexec.c | 6 +-
tests/builtins/memexec-malloc.c | 6 +-
tests/builtins/oracle/malloc-deps.res.oracle | 86 +++++++++----------
.../builtins/oracle/memexec-malloc.res.oracle | 63 +++++++-------
9 files changed, 119 insertions(+), 99 deletions(-)
rename tests/builtins/{malloc-deps.i => malloc-deps.c} (82%)
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 2465cf27635..f521fcac3b7 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -149,8 +149,10 @@ let prepare_builtin kf builtin_name builtin expected_typ =
then
Value_parameters.warning ~source ~once:true
~wkey:Value_parameters.wkey_builtins_override
- "The builtin %s will not be used for function %a of incompatible type."
+ "The builtin %s will not be used for function %a of incompatible type.@ \
+ (got: %a)."
builtin_name Kernel_function.pretty kf
+ Printer.pp_typ (Kernel_function.get_type kf)
else
match find_builtin_specification kf with
| None ->
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 7c83a1be556..2efd15c1339 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -354,8 +354,14 @@ let alloc_fresh ?(prefix="malloc") weak region state actuals =
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
-let () = Builtins.register_builtin "Frama_C_malloc_fresh" (alloc_fresh Strong Base.Malloc)
-let () = Builtins.register_builtin "Frama_C_malloc_fresh_weak" (alloc_fresh Weak Base.Malloc)
+let () =
+ Builtins.register_builtin "Frama_C_malloc_fresh"
+ (alloc_fresh Strong Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
+let () =
+ Builtins.register_builtin "Frama_C_malloc_fresh_weak"
+ (alloc_fresh Weak Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let alloc_size_ok intended_size =
try
@@ -404,8 +410,14 @@ let calloc_abstract calloc_f state actuals =
let calloc_fresh weak state actuals =
calloc_abstract (alloc_abstract weak Base.Malloc) state actuals
-let () = Builtins.register_builtin "Frama_C_calloc_fresh" (calloc_fresh Strong)
-let () = Builtins.register_builtin "Frama_C_calloc_fresh_weak" (calloc_fresh Weak)
+let () =
+ Builtins.register_builtin "Frama_C_calloc_fresh" (calloc_fresh Strong)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
+let () =
+ Builtins.register_builtin "Frama_C_calloc_fresh_weak" (calloc_fresh Weak)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
(* Variables that have been returned by a call to an allocation function
at this callstack. The first allocated variable is at the top of the
@@ -493,12 +505,15 @@ let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin =
;;
let () = Builtins.register_builtin
~replace:"malloc" "Frama_C_malloc_by_stack" (alloc_by_stack Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
~replace:"__fc_vla_alloc" "Frama_C_vla_alloc_by_stack"
(alloc_by_stack Base.VLA ~returns_null:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
~replace:"alloca" "Frama_C_alloca"
(alloc_by_stack ~prefix:"alloca" Base.Alloca ~returns_null:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
(* Equivalent to [alloc_by_stack], but for [calloc]. *)
let calloc_by_stack : Db.Value.builtin = fun state actuals ->
@@ -506,6 +521,8 @@ let calloc_by_stack : Db.Value.builtin = fun state actuals ->
let () = Builtins.register_builtin
~replace:"calloc" "Frama_C_calloc_by_stack" calloc_by_stack
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
(** {1 Free} *)
@@ -614,7 +631,9 @@ let frama_c_free state actuals =
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
-let () = Builtins.register_builtin ~replace:"free" "Frama_C_free" frama_c_free
+let () =
+ Builtins.register_builtin ~replace:"free" "Frama_C_free" frama_c_free
+ ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
(* built-in for [__fc_vla_free] function. By construction, VLA should always
be mapped to a single base. *)
@@ -633,6 +652,7 @@ let frama_c_vla_free state actuals =
let () =
Builtins.register_builtin
~replace:"__fc_vla_free" "Frama_C_vla_free" frama_c_vla_free
+ ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
let free_automatic_bases stack state =
(* free automatic bases that were allocated in the current function *)
@@ -792,9 +812,12 @@ let realloc ~multiple state args = match args with
let () = Builtins.register_builtin
~replace:"realloc" "Frama_C_realloc" (realloc ~multiple:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
+ Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
"Frama_C_realloc_multiple" (realloc ~multiple:true)
-
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
+ Cil.theMachine.Cil.typeOfSizeOf]))
(** {1 Leak detection} *)
diff --git a/tests/builtins/malloc-deps.i b/tests/builtins/malloc-deps.c
similarity index 82%
rename from tests/builtins/malloc-deps.i
rename to tests/builtins/malloc-deps.c
index 9c514cf7f03..a50b7e99b2f 100644
--- a/tests/builtins/malloc-deps.i
+++ b/tests/builtins/malloc-deps.c
@@ -1,15 +1,15 @@
/* run.config*
OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
*/
+#include <stddef.h>
//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh(unsigned long n);
+void *Frama_C_malloc_fresh(size_t n);
//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh_weak(unsigned long n);
+void *Frama_C_malloc_fresh_weak(size_t n);
//@ assigns \result \from \nothing;
-void *Frama_C_malloc_by_stack(unsigned long n);
+void *Frama_C_malloc_by_stack(size_t n);
volatile int v;
-
void g(int *p, int k) { p[k] = k; }
void main(int i, int j) {
diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c
index bb1e66301f3..1d1afd57f2a 100644
--- a/tests/builtins/malloc-optimistic.c
+++ b/tests/builtins/malloc-optimistic.c
@@ -1,9 +1,9 @@
/* run.config*
STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -eva-memexec"
*/
-
+#include <stddef.h>
//@ assigns \result \from \nothing;
-void *malloc(unsigned long size);
+void *malloc(size_t size);
//@ assigns \nothing; frees p;
void free(void *p);
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index eb00026fa89..c62203fa9dd 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,9 +1,9 @@
/* run.config*
OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
*/
-
-void *Frama_C_malloc_by_stack(unsigned long i);
-void *Frama_C_malloc_fresh(unsigned long i);
+#include <stddef.h>
+void *Frama_C_malloc_by_stack(size_t i);
+void *Frama_C_malloc_fresh(size_t i);
void main(int c) {
int x;
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 463f80de13f..2a0434c0085 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,12 +1,12 @@
/* run.config*
OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
*/
-
+#include <stddef.h>
//@ assigns \result;
-void *Frama_C_malloc_fresh(unsigned long n);
+void *Frama_C_malloc_fresh(size_t n);
//@ assigns \result;
-void *Frama_C_malloc_fresh_weak(unsigned long n);
+void *Frama_C_malloc_fresh_weak(size_t n);
void f(int *p, int i) {
diff --git a/tests/builtins/memexec-malloc.c b/tests/builtins/memexec-malloc.c
index 0d3b65f3862..13755b28f84 100644
--- a/tests/builtins/memexec-malloc.c
+++ b/tests/builtins/memexec-malloc.c
@@ -1,7 +1,7 @@
/* run.config*
- STDOPT: #"-eva-malloc-functions alloc,Frama_C_malloc_by_stack -eva-mlevel 0"
+ STDOPT: #"-eva-malloc-functions alloc -eva-mlevel 0"
*/
-
+#include <stdlib.h>
#define N 2000
int t[N];
@@ -12,7 +12,7 @@ void f() {
}
int *alloc() {
- return Frama_C_malloc_by_stack(4);
+ return malloc(4);
}
int *k() {
diff --git a/tests/builtins/oracle/malloc-deps.res.oracle b/tests/builtins/oracle/malloc-deps.res.oracle
index f76d408d0cf..3d9d469a191 100644
--- a/tests/builtins/oracle/malloc-deps.res.oracle
+++ b/tests/builtins/oracle/malloc-deps.res.oracle
@@ -1,106 +1,106 @@
-[kernel] Parsing tests/builtins/malloc-deps.i (no preprocessing)
+[kernel] Parsing tests/builtins/malloc-deps.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
-[eva] tests/builtins/malloc-deps.i:17: Call to builtin Frama_C_malloc_fresh_weak
-[eva] tests/builtins/malloc-deps.i:17:
+[eva] tests/builtins/malloc-deps.c:17: Call to builtin Frama_C_malloc_fresh_weak
+[eva] tests/builtins/malloc-deps.c:17:
allocating weak variable __malloc_w_main_l17
-[eva] tests/builtins/malloc-deps.i:21: Call to builtin Frama_C_malloc_fresh
-[eva] tests/builtins/malloc-deps.i:21: allocating variable __malloc_main_l21
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva] tests/builtins/malloc-deps.i:28: allocating variable __malloc_main_l28
+[eva] tests/builtins/malloc-deps.c:21: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/malloc-deps.c:21: allocating variable __malloc_main_l21
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/malloc-deps.c:28: allocating variable __malloc_main_l28
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
-[eva:alarm] tests/builtins/malloc-deps.i:13: Warning:
+ Called from tests/builtins/malloc-deps.c:29.
+[eva:alarm] tests/builtins/malloc-deps.c:13: Warning:
out of bounds write. assert \valid(p + k);
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc:weak] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc:weak] tests/builtins/malloc-deps.c:28:
marking variable `__malloc_main_l28' as weak
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31) to fit 0..63
-[eva:alarm] tests/builtins/malloc-deps.i:29: Warning:
+[eva:alarm] tests/builtins/malloc-deps.c:29: Warning:
signed overflow. assert l + v ≤ 2147483647;
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/63) to fit 0..95
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/95) to fit 0..127
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/127) to fit 0..159
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/159) to fit 0..191
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:27: starting to merge loop iterations
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:27: starting to merge loop iterations
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/191) to fit 0..191/223
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/223) to fit 0..191/255
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/255) to fit 0..191/319
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/319) to fit 0..191/319
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
@@ -147,13 +147,13 @@
__malloc_w_main_l28[0..9] FROM v (and SELF)
[from] ====== END OF DEPENDENCIES ======
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_malloc_fresh_weak at tests/builtins/malloc-deps.i:17 (by main):
+[from] call to Frama_C_malloc_fresh_weak at tests/builtins/malloc-deps.c:17 (by main):
\result FROM \nothing
-[from] call to Frama_C_malloc_fresh at tests/builtins/malloc-deps.i:21 (by main):
+[from] call to Frama_C_malloc_fresh at tests/builtins/malloc-deps.c:21 (by main):
\result FROM \nothing
-[from] call to Frama_C_malloc_by_stack at tests/builtins/malloc-deps.i:28 (by main):
+[from] call to Frama_C_malloc_by_stack at tests/builtins/malloc-deps.c:28 (by main):
\result FROM \nothing
-[from] call to g at tests/builtins/malloc-deps.i:29 (by main):
+[from] call to g at tests/builtins/malloc-deps.c:29 (by main):
__malloc_w_main_l28[0..9] FROM p; k (and SELF)
[from] entry point:
__malloc_w_main_l17[0] FROM i; j (and SELF)
diff --git a/tests/builtins/oracle/memexec-malloc.res.oracle b/tests/builtins/oracle/memexec-malloc.res.oracle
index 7a3b162c3f6..a6ebfd55f71 100644
--- a/tests/builtins/oracle/memexec-malloc.res.oracle
+++ b/tests/builtins/oracle/memexec-malloc.res.oracle
@@ -1,8 +1,4 @@
[kernel] Parsing tests/builtins/memexec-malloc.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/builtins/memexec-malloc.c:15: Warning:
- Calling undeclared function Frama_C_malloc_by_stack. Old style K&R code?
-[kernel:annot:missing-spec] tests/builtins/memexec-malloc.c:22: Warning:
- Neither code nor specification for function Frama_C_malloc_by_stack, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -24,15 +20,13 @@
[eva] tests/builtins/memexec-malloc.c:29: Reusing old results for call to f
[eva] computing for function alloc <- main.
Called from tests/builtins/memexec-malloc.c:31.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_main_l31
[eva] Recording results for alloc
[eva] Done for function alloc
[eva] computing for function alloc <- main.
Called from tests/builtins/memexec-malloc.c:32.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_main_l32
[eva] Recording results for alloc
[eva] Done for function alloc
@@ -40,8 +34,7 @@
Called from tests/builtins/memexec-malloc.c:34.
[eva] computing for function alloc <- k <- main.
Called from tests/builtins/memexec-malloc.c:19.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_k_l19
[eva] Recording results for alloc
[eva] Done for function alloc
@@ -51,8 +44,7 @@
Called from tests/builtins/memexec-malloc.c:35.
[eva] computing for function alloc <- k <- main.
Called from tests/builtins/memexec-malloc.c:19.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_k_l19_0
[eva] Recording results for alloc
[eva] Done for function alloc
@@ -61,57 +53,60 @@
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function alloc:
- __retres ∈
- {{ &__malloc_main_l31 ; &__malloc_main_l32 ; &__malloc_k_l19 ;
- &__malloc_k_l19_0 }}
[eva:final-states] Values at end of function f:
t[0..1999] ∈ [0..1999]
i ∈ {2000}
+[eva:final-states] Values at end of function alloc:
+ __fc_heap_status ∈ [--..--]
[eva:final-states] Values at end of function k:
-
+ __fc_heap_status ∈ [--..--]
[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
t[0..1999] ∈ [0..1999]
p1 ∈ {{ &__malloc_main_l31 }}
p2 ∈ {{ &__malloc_main_l32 }}
p3 ∈ {{ &__malloc_k_l19 }}
p4 ∈ {{ &__malloc_k_l19_0 }}
-[from] Computing for function alloc
-[from] Computing for function Frama_C_malloc_by_stack <-alloc
-[from] Done for function Frama_C_malloc_by_stack
-[from] Done for function alloc
[from] Computing for function f
[from] Done for function f
+[from] Computing for function alloc
+[from] Computing for function malloc <-alloc
+[from] Done for function malloc
+[from] Done for function alloc
[from] Computing for function k
[from] Done for function k
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_by_stack:
- \result FROM x_0
-[from] Function alloc:
- \result FROM \nothing
[from] Function f:
t[0..1999] FROM \nothing (and SELF)
+[from] Function malloc:
+ __fc_heap_status FROM __fc_heap_status; size (and SELF)
+ \result FROM __fc_heap_status; size
+[from] Function alloc:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ \result FROM __fc_heap_status
[from] Function k:
- \result FROM \nothing
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ \result FROM __fc_heap_status
[from] Function main:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
t[0..1999] FROM \nothing (and SELF)
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function alloc:
- tmp; __retres
-[inout] Inputs for function alloc:
- \nothing
[inout] Out (internal) for function f:
t[0..1999]; i
[inout] Inputs for function f:
\nothing
+[inout] Out (internal) for function alloc:
+ __fc_heap_status; tmp
+[inout] Inputs for function alloc:
+ __fc_heap_status
[inout] Out (internal) for function k:
- tmp
+ __fc_heap_status; tmp
[inout] Inputs for function k:
- \nothing
+ __fc_heap_status
[inout] Out (internal) for function main:
- t[0..1999]; p1; p2; p3; p4
+ __fc_heap_status; t[0..1999]; p1; p2; p3; p4
[inout] Inputs for function main:
- t[1..2]
+ __fc_heap_status; t[1..2]
--
GitLab