diff --git a/src/plugins/instantiate/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
index 87b1f9338ccb5ecdd99d339551a383459f8305bc..d87508ad415bcf21b677949b5429c8b8b376fc97 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 28d42c036e394314e15f148be188d770b46886e9..cc72848fd620f5aee8c2dce2f91fa4e145383d34 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 ffd73cad6a70f0b48b2e47fa34756d3a982456b3..f87d862900577f5b3f9047f1f3c3df7c7fbfe9b1 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 17c8260b5165b3f8b6ff0fdfd04a2c5c4eabc653..45b8e49cd11a595270606364836e897a89ba3c73 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 432b8ed6a6d3aa03bbb2d99e449641a6e4ac7d1c..654466dbc2f9ee2777f40c0935494700e7b82649 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 1b7efe66ddfaf3924b521e046ee4ebff7779483e..368076b562a058ace4515686e79749ec84e3ebcc 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 ffe160d7caa31fe89b889cdcc11c09f58f3192ab..7495743e8a2cb7de538494ee23edb207bb6c5f48 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 462fc372857d8a254614e0759e958ffd2d99b85d..f68d49c8e424bb07a8256d8804001f17aad4fe39 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));