Skip to content
Snippets Groups Projects
Commit 778ba37f authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[Instantiate] Test related to enums for memset/calloc

parent c6773228
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 273 additions and 13 deletions
src/plugins/instantiate/tests/stdlib/calloc.c
+ 3
− 0
View file @ 778ba37f
......@@ -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)) ;
......
src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+ 89
− 2
View file @ 778ba37f
[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));
......
src/plugins/instantiate/tests/string/memset_0.c
+ 6
− 0
View file @ 778ba37f
......@@ -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));
......
src/plugins/instantiate/tests/string/memset_FF.c
+ 6
− 0
View file @ 778ba37f
......@@ -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));
......
src/plugins/instantiate/tests/string/memset_value.c
+ 6
− 0
View file @ 778ba37f
......@@ -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));
......
src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+ 64
− 2
View file @ 778ba37f
[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));
......
src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+ 64
− 2
View file @ 778ba37f
[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));
......
src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+ 35
− 7
View file @ 778ba37f
......@@ -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));
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment