From 778ba37f1cb383495ed1a7c3da82c2c3413e72aa Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 09:17:49 +0100
Subject: [PATCH] [Instantiate] Test related to enums for memset/calloc
---
src/plugins/instantiate/tests/stdlib/calloc.c | 3 +
.../tests/stdlib/oracle/calloc.res.oracle | 91 ++++++++++++++++++-
.../instantiate/tests/string/memset_0.c | 6 ++
.../instantiate/tests/string/memset_FF.c | 6 ++
.../instantiate/tests/string/memset_value.c | 6 ++
.../tests/string/oracle/memset_0.res.oracle | 66 +++++++++++++-
.../tests/string/oracle/memset_FF.res.oracle | 66 +++++++++++++-
.../string/oracle/memset_value.res.oracle | 42 +++++++--
8 files changed, 273 insertions(+), 13 deletions(-)
diff --git a/src/plugins/instantiate/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
index 87b1f9338cc..d87508ad415 100644
--- a/src/plugins/instantiate/tests/stdlib/calloc.c
+++ b/src/plugins/instantiate/tests/stdlib/calloc.c
@@ -11,8 +11,11 @@ struct Flex {
int f[] ;
} ;
+enum E { A, B, C };
+
int main(void){
int* pi = calloc(10, sizeof(int)) ;
+ enum E* pe = calloc(10, sizeof(enum E)) ;
float* pf = calloc(10, sizeof(float)) ;
struct X* px = calloc(10, sizeof(struct X)) ;
char* pc = calloc(10, sizeof(char)) ;
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 28d42c036e3..cc72848fd62 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
-[instantiate] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
-[instantiate] tests/stdlib/calloc.c:22: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:24: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:25: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -12,6 +12,11 @@ struct Flex {
char c ;
int f[] ;
};
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
@@ -216,6 +221,43 @@ float *calloc_float(size_t num, size_t 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;
+ */
+enum E *calloc_e_E(size_t num, size_t size)
+{
+ enum E *__retres;
+ __retres = (enum E *)calloc(num,size);
+ return __retres;
+}
+
/*@ requires correct_size: 0 ≡ size % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, num, size;
@@ -257,6 +299,7 @@ int main(void)
{
int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int));
+ enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
float *pf = calloc_float((unsigned int)10,sizeof(float));
struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char));
@@ -283,6 +326,11 @@ struct Flex {
char c ;
int f[] ;
};
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
@@ -490,6 +538,44 @@ float *calloc_float(size_t num, size_t 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;
+ */
+enum E *calloc_e_E(size_t num, size_t size)
+{
+ enum E *__retres;
+ __retres = (enum E *)calloc(num,size);
+ return __retres;
+}
+
/*@ requires correct_size: 0 ≡ size % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, num, size;
@@ -532,6 +618,7 @@ int main(void)
{
int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int));
+ enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
float *pf = calloc_float((unsigned int)10,sizeof(float));
struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char));
diff --git a/src/plugins/instantiate/tests/string/memset_0.c b/src/plugins/instantiate/tests/string/memset_0.c
index ffd73cad6a7..f87d8629005 100644
--- a/src/plugins/instantiate/tests/string/memset_0.c
+++ b/src/plugins/instantiate/tests/string/memset_0.c
@@ -27,6 +27,12 @@ void integer(int dest[10]){
memset(res, 0, 10 * sizeof(int));
}
+enum E { A, B, C } ;
+void with_enum(enum E dest[10]){
+ enum E * res = memset(dest, 0, 10 * sizeof(enum E));
+ memset(res, 0, 10 * sizeof(enum E));
+}
+
void floats(float dest[10]){
float * res = memset(dest, 0, 10 * sizeof(float));
memset(res, 0, 10 * sizeof(float));
diff --git a/src/plugins/instantiate/tests/string/memset_FF.c b/src/plugins/instantiate/tests/string/memset_FF.c
index 17c8260b516..45b8e49cd11 100644
--- a/src/plugins/instantiate/tests/string/memset_FF.c
+++ b/src/plugins/instantiate/tests/string/memset_FF.c
@@ -27,6 +27,12 @@ void integer(int dest[10]){
memset(res, 0xFF, 10 * sizeof(int));
}
+enum E { A, B, C } ;
+void with_enum(enum E dest[10]){
+ enum E * res = memset(dest, 0xFF, 10 * sizeof(enum E));
+ memset(res, 0xFF, 10 * sizeof(enum E));
+}
+
void unsigned_integer(unsigned dest[10]){
unsigned * res = memset(dest, 0xFF, 10 * sizeof(unsigned));
memset(res, 0xFF, 10 * sizeof(unsigned));
diff --git a/src/plugins/instantiate/tests/string/memset_value.c b/src/plugins/instantiate/tests/string/memset_value.c
index 432b8ed6a6d..654466dbc2f 100644
--- a/src/plugins/instantiate/tests/string/memset_value.c
+++ b/src/plugins/instantiate/tests/string/memset_value.c
@@ -27,6 +27,12 @@ void integer(int dest[10], int value){
memset(res, value, 10 * sizeof(int));
}
+enum E { A, B, C } ;
+void with_enum(enum E dest[10], int value){
+ enum E * res = memset(dest, value, 10 * sizeof(enum E));
+ memset(res, value, 10 * sizeof(enum E));
+}
+
void with_named(named dest[10], int value){
named * res = memset(dest, value, 10 * sizeof(named));
memset(res, value, 10 * sizeof(named));
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index 1b7efe66ddf..368076b562a 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memset_0.c (with preprocessing)
-[instantiate] tests/string/memset_0.c:56: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_0.c:57: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:62: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:63: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +10,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -111,6 +116,32 @@ void integer(int * /*[10]*/ dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = len / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 0;
+ ensures result: \result ≡ ptr;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_0(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,0,len);
+ return __retres;
+}
+
+void with_enum(enum E * /*[10]*/ dest)
+{
+ enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
@@ -244,6 +275,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -350,6 +386,32 @@ void integer(int *dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = \old(len) / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 0;
+ ensures result: \result ≡ \old(ptr);
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_0(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,0,len);
+ return __retres;
+}
+
+void with_enum(enum E *dest)
+{
+ enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index ffe160d7caa..7495743e8a2 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memset_FF.c (with preprocessing)
-[instantiate] tests/string/memset_FF.c:82: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_FF.c:83: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:88: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:89: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +10,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -112,6 +117,32 @@ void integer(int * /*[10]*/ dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = len / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295;
+ ensures result: \result ≡ ptr;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_FF(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,255,len);
+ return __retres;
+}
+
+void with_enum(enum E * /*[10]*/ dest)
+{
+ enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
@@ -382,6 +413,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -489,6 +525,32 @@ void integer(int *dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = \old(len) / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295;
+ ensures result: \result ≡ \old(ptr);
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_FF(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,255,len);
+ return __retres;
+}
+
+void with_enum(enum E *dest)
+{
+ enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index 462fc372857..f68d49c8e42 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -3,30 +3,34 @@
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:27: Warning:
Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:31: Warning:
- Ignore call: not well typed
[instantiate] tests/string/memset_value.c:32: Warning:
Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:36: Warning:
+[instantiate] tests/string/memset_value.c:33: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:37: Warning:
Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:41: Warning:
+[instantiate] tests/string/memset_value.c:38: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:42: Warning:
Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:46: Warning:
+[instantiate] tests/string/memset_value.c:43: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:47: Warning:
Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:51: Warning:
+[instantiate] tests/string/memset_value.c:48: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:52: Warning:
Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:56: Warning:
+[instantiate] tests/string/memset_value.c:53: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:57: Warning:
Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:58: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:62: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:63: Warning:
+ Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -36,6 +40,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
@@ -119,6 +128,13 @@ void integer(int * /*[10]*/ dest, int value)
return;
}
+void with_enum(enum E * /*[10]*/ dest, int value)
+{
+ enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
+ memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
void with_named(named * /*[10]*/ dest, int value)
{
named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
@@ -174,6 +190,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
@@ -262,6 +283,13 @@ void integer(int *dest, int value)
return;
}
+void with_enum(enum E *dest, int value)
+{
+ enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
+ memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
void with_named(named *dest, int value)
{
named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
--
GitLab