From a9c057385e03948d5f57a979dd2f43ab59abe2fd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 24 Oct 2019 10:37:45 +0200
Subject: [PATCH] [Builtin] Tests for stdlib.h functions
---
src/plugins/builtin/Makefile.in | 2 +-
src/plugins/builtin/stdlib/calloc.ml | 8 +-
src/plugins/builtin/tests/stdlib/calloc.c | 23 +
src/plugins/builtin/tests/stdlib/free.c | 11 +
src/plugins/builtin/tests/stdlib/malloc.c | 23 +
.../tests/stdlib/oracle/calloc.res.oracle | 543 ++++++++++++++++++
.../tests/stdlib/oracle/free.res.oracle | 207 +++++++
.../tests/stdlib/oracle/malloc.res.oracle | 429 ++++++++++++++
src/plugins/builtin/tests/stdlib/test_config | 1 +
9 files changed, 1245 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/builtin/tests/stdlib/calloc.c
create mode 100644 src/plugins/builtin/tests/stdlib/free.c
create mode 100644 src/plugins/builtin/tests/stdlib/malloc.c
create mode 100644 src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
create mode 100644 src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
create mode 100644 src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
create mode 100644 src/plugins/builtin/tests/stdlib/test_config
diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/builtin/Makefile.in
index a124d63c70e..810ca5c502f 100644
--- a/src/plugins/builtin/Makefile.in
+++ b/src/plugins/builtin/Makefile.in
@@ -62,7 +62,7 @@ PLUGIN_CMO := \
PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
#PLUGIN_NO_DEFAULT_TEST := no
-PLUGIN_TESTS_DIRS := string options
+PLUGIN_TESTS_DIRS := string stdlib options
################
# Generic part #
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index 8d11849cc72..10ba0682d7a 100644
--- a/src/plugins/builtin/stdlib/calloc.ml
+++ b/src/plugins/builtin/stdlib/calloc.ml
@@ -61,7 +61,13 @@ let generate_requires ?loc alloc_type num size =
let pinitialized_len ?loc alloc_type num size =
let result = tresult ?loc (ptr_of alloc_type) in
- let initialized ?loc t = pinitialized ?loc (here_label, t) in
+ let initialized ?loc t =
+ let t = match t.term_node, t.term_type with
+ | TLval (lv), Ctype t -> taddrof ?loc lv (Ctype (ptr_of t))
+ | _ -> assert false
+ in
+ pinitialized ?loc (here_label, t)
+ in
let p = if Cil.has_flexible_array_member alloc_type then
let access = Cil.mkTermMem ~addr:result ~off:TNoOffset in
let access = term ?loc (TLval access) (Ctype alloc_type) in
diff --git a/src/plugins/builtin/tests/stdlib/calloc.c b/src/plugins/builtin/tests/stdlib/calloc.c
new file mode 100644
index 00000000000..58286c59dda
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/calloc.c
@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct X {
+ int x ;
+ int y ;
+} ;
+
+struct Flex {
+ int x ;
+ char c ;
+ int f[] ;
+} ;
+
+int main(void){
+ int* pi = calloc(10, sizeof(int)) ;
+ float* pf = calloc(10, sizeof(float)) ;
+ struct X* px = calloc(10, sizeof(struct X)) ;
+ char* pc = calloc(10, sizeof(char)) ;
+
+ int (*pa) [10] = calloc(10, sizeof(int[10])) ;
+
+ struct Flex* f = calloc(1, sizeof(struct Flex) + 3 * sizeof(int)) ;
+}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/free.c b/src/plugins/builtin/tests/stdlib/free.c
new file mode 100644
index 00000000000..eb0ff860035
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/free.c
@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+void foo(int * x){
+ free(x);
+}
+void bar(float * x){
+ free(x);
+}
+void baz(int (*x) [10]){
+ free(x);
+}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/malloc.c b/src/plugins/builtin/tests/stdlib/malloc.c
new file mode 100644
index 00000000000..e39f5d9c638
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/malloc.c
@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct X {
+ int x ;
+ int y ;
+} ;
+
+struct Flex {
+ int x ;
+ char c ;
+ int f[] ;
+} ;
+
+int main(void){
+ int* pi = malloc(sizeof(int) * 10) ;
+ float* pf = malloc(sizeof(float) * 10) ;
+ struct X* px = malloc(sizeof(struct X) * 10) ;
+ char* pc = malloc(10) ;
+
+ int (*pa) [10] = malloc(sizeof(int[10]) * 10) ;
+
+ struct Flex* f = malloc(sizeof(struct Flex) + 3 * sizeof(int)) ;
+}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
new file mode 100644
index 00000000000..e3e9e4bc0c8
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
@@ -0,0 +1,543 @@
+[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stdlib.h"
+struct X {
+ int x ;
+ int y ;
+};
+struct Flex {
+ int x ;
+ char c ;
+ int f[] ;
+};
+/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
+ requires only_one: num ≡ 1;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ \let __fc_flexlen = (size - 8) / 4;
+ \result->x ≡ 0 ∧
+ \result->c ≡ 0 ∧
+ (∀ ℤ j1; 0 ≤ j1 < __fc_flexlen ⇒ \result->f[j1] ≡ 0);
+ ensures
+ initialization:
+ \let __fc_flexlen = (size - 8) / 4;
+ \initialized(&\result->x) ∧
+ \initialized(&\result->c) ∧
+ (∀ ℤ j1;
+ 0 ≤ j1 < __fc_flexlen ⇒ \initialized(&\result->f[j1]));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct Flex *calloc_Flex(size_t num, size_t size)
+{
+ struct Flex *__retres;
+ __retres = (struct Flex *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 40;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < num ⇒
+ (∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(\result + j0))[j1] ≡ 0);
+ ensures
+ initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < num ⇒
+ (∀ ℤ j1;
+ 0 ≤ j1 < 10 ⇒ \initialized(&(*(\result + j0))[j1]));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int (*calloc_arr10_int(size_t num, size_t size))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 1;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+char *calloc_char(size_t num, size_t size)
+{
+ char *__retres;
+ __retres = (char *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 8;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < num ⇒
+ (\result + j0)->x ≡ 0 ∧ (\result + j0)->y ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < num ⇒
+ \initialized(&(\result + j0)->x) ∧
+ \initialized(&(\result + j0)->y);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct X *calloc_X(size_t num, size_t size)
+{
+ struct X *__retres;
+ __retres = (struct X *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(\result + j0) ≡ 0.;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+float *calloc_float(size_t num, size_t size)
+{
+ float *__retres;
+ __retres = (float *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *calloc_int(size_t num, size_t size)
+{
+ int *__retres;
+ __retres = (int *)calloc(num,size);
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int *pi = calloc_int((unsigned int)10,sizeof(int));
+ float *pf = calloc_float((unsigned int)10,sizeof(float));
+ struct X *px = calloc_X((unsigned int)10,sizeof(struct X));
+ char *pc = calloc_char((unsigned int)10,sizeof(char));
+ int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
+ struct Flex *f =
+ calloc_Flex((unsigned int)1,
+ sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ __retres = 0;
+ return __retres;
+}
+
+
+[kernel] Parsing tests/stdlib/result/calloc.c (with preprocessing)
+[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
+[kernel] tests/stdlib/calloc.c:14: Warning:
+ def'n of func main at tests/stdlib/calloc.c:14 (sum 5516) conflicts with the one at tests/stdlib/result/calloc.c:252 (sum 7290); keeping the one at tests/stdlib/result/calloc.c:252.
+/* Generated by Frama-C */
+#include "stdlib.h"
+struct X {
+ int x ;
+ int y ;
+};
+struct Flex {
+ int x ;
+ char c ;
+ int f[] ;
+};
+/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
+ requires only_one: num ≡ 1;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ \let __fc_flexlen = (\old(size) - 8) / 4;
+ \result->x ≡ 0 ∧ \result->c ≡ 0 ∧
+ (∀ ℤ j1; 0 ≤ j1 < __fc_flexlen ⇒ \result->f[j1] ≡ 0);
+ ensures
+ initialization:
+ \let __fc_flexlen = (\old(size) - 8) / 4;
+ \initialized(&\result->x) ∧ \initialized(&\result->c) ∧
+ (∀ ℤ j1;
+ 0 ≤ j1 < __fc_flexlen ⇒ \initialized(&\result->f[j1]));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct Flex *calloc_Flex(size_t num, size_t size)
+{
+ struct Flex *__retres;
+ __retres = (struct Flex *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 40;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < \old(num) ⇒
+ (∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(\result + j0))[j1] ≡ 0);
+ ensures
+ initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < \old(num) ⇒
+ (∀ ℤ j1;
+ 0 ≤ j1 < 10 ⇒ \initialized(&(*(\result + j0))[j1]));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int (*calloc_arr10_int(size_t num, size_t size))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 1;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+char *calloc_char(size_t num, size_t size)
+{
+ char *__retres;
+ __retres = (char *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 8;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < \old(num) ⇒
+ (\result + j0)->x ≡ 0 ∧ (\result + j0)->y ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0;
+ 0 ≤ j0 < \old(num) ⇒
+ \initialized(&(\result + j0)->x) ∧
+ \initialized(&(\result + j0)->y);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct X *calloc_X(size_t num, size_t size)
+{
+ struct X *__retres;
+ __retres = (struct X *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ *(\result + j0) ≡ 0.;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+float *calloc_float(size_t num, size_t size)
+{
+ float *__retres;
+ __retres = (float *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *calloc_int(size_t num, size_t size)
+{
+ int *__retres;
+ __retres = (int *)calloc(num,size);
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int *pi = calloc_int((unsigned int)10,sizeof(int));
+ float *pf = calloc_float((unsigned int)10,sizeof(float));
+ struct X *px = calloc_X((unsigned int)10,sizeof(struct X));
+ char *pc = calloc_char((unsigned int)10,sizeof(char));
+ int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
+ struct Flex *f =
+ calloc_Flex((unsigned int)1,
+ sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
new file mode 100644
index 00000000000..425d46815eb
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
@@ -0,0 +1,207 @@
+[kernel] Parsing tests/stdlib/free.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stdlib.h"
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_int(int *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void foo(int *x)
+{
+ free_int(x);
+ return;
+}
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_float(float *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void bar(float *x)
+{
+ free_float(x);
+ return;
+}
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_arr10_int(int (*ptr)[10])
+{
+ free((void *)ptr);
+ return;
+}
+
+void baz(int (*x)[10])
+{
+ free_arr10_int(x);
+ return;
+}
+
+
+[kernel] Parsing tests/stdlib/result/free.c (with preprocessing)
+[kernel] Parsing tests/stdlib/free.c (with preprocessing)
+[kernel] tests/stdlib/free.c:3: Warning:
+ dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:29
+[kernel] tests/stdlib/free.c:6: Warning:
+ dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:61
+[kernel] tests/stdlib/free.c:9: Warning:
+ dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:93
+/* Generated by Frama-C */
+#include "stdlib.h"
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(\old(ptr));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_int(int *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void foo(int *x)
+{
+ free_int(x);
+ return;
+}
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(\old(ptr));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_float(float *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void bar(float *x)
+{
+ free_float(x);
+ return;
+}
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(\old(ptr));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_arr10_int(int (*ptr)[10])
+{
+ free((void *)ptr);
+ return;
+}
+
+void baz(int (*x)[10])
+{
+ free_arr10_int(x);
+ return;
+}
+
+
diff --git a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
new file mode 100644
index 00000000000..bc6d992efeb
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
@@ -0,0 +1,429 @@
+[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stdlib.h"
+struct X {
+ int x ;
+ int y ;
+};
+struct Flex {
+ int x ;
+ char c ;
+ int f[] ;
+};
+/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct Flex *malloc_Flex(size_t size)
+{
+ struct Flex *__retres;
+ __retres = (struct Flex *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 40;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int (*malloc_arr10_int(size_t size))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 1;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+char *malloc_char(size_t size)
+{
+ char *__retres;
+ __retres = (char *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 8;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct X *malloc_X(size_t size)
+{
+ struct X *__retres;
+ __retres = (struct X *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+float *malloc_float(size_t size)
+{
+ float *__retres;
+ __retres = (float *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *malloc_int(size_t size)
+{
+ int *__retres;
+ __retres = (int *)malloc(size);
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int *pi = malloc_int(sizeof(int) * (unsigned int)10);
+ float *pf = malloc_float(sizeof(float) * (unsigned int)10);
+ struct X *px = malloc_X(sizeof(struct X) * (unsigned int)10);
+ char *pc = malloc_char((unsigned int)10);
+ int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
+ struct Flex *f =
+ malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ __retres = 0;
+ return __retres;
+}
+
+
+[kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing)
+[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
+[kernel] tests/stdlib/malloc.c:14: Warning:
+ def'n of func main at tests/stdlib/malloc.c:14 (sum 5516) conflicts with the one at tests/stdlib/result/malloc.c:198 (sum 7290); keeping the one at tests/stdlib/result/malloc.c:198.
+/* Generated by Frama-C */
+#include "stdlib.h"
+struct X {
+ int x ;
+ int y ;
+};
+struct Flex {
+ int x ;
+ char c ;
+ int f[] ;
+};
+/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct Flex *malloc_Flex(size_t size)
+{
+ struct Flex *__retres;
+ __retres = (struct Flex *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 40;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int (*malloc_arr10_int(size_t size))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 1;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+char *malloc_char(size_t size)
+{
+ char *__retres;
+ __retres = (char *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 8;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+struct X *malloc_X(size_t size)
+{
+ struct X *__retres;
+ __retres = (struct X *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+float *malloc_float(size_t size)
+{
+ float *__retres;
+ __retres = (float *)malloc(size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *malloc_int(size_t size)
+{
+ int *__retres;
+ __retres = (int *)malloc(size);
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int *pi = malloc_int(sizeof(int) * (unsigned int)10);
+ float *pf = malloc_float(sizeof(float) * (unsigned int)10);
+ struct X *px = malloc_X(sizeof(struct X) * (unsigned int)10);
+ char *pc = malloc_char((unsigned int)10);
+ int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
+ struct Flex *f =
+ malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/builtin/tests/stdlib/test_config b/src/plugins/builtin/tests/stdlib/test_config
new file mode 100644
index 00000000000..467fffb4bcb
--- /dev/null
+++ b/src/plugins/builtin/tests/stdlib/test_config
@@ -0,0 +1 @@
+OPT: @PTEST_FILE@ -builtin -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-builtin @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
--
GitLab