Skip to content
Snippets Groups Projects
Commit c52b2c7a authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

[tests] Fixed memsize test to use __heap_size instead of __memory_size

parent 7054d0da
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
+ 13
− 13
View file @ c52b2c7a
...@@ -14,58 +14,58 @@ ...@@ -14,58 +14,58 @@
# endif # endif
# endif # endif
extern size_t __memory_size; extern size_t __heap_size;
int main(int argc, char **argv) { int main(int argc, char **argv) {
// Allocation increases // Allocation increases
char *a = malloc(7); char *a = malloc(7);
/*@assert (__memory_size == 7); */ /*@assert (__heap_size == 7); */
char *b = malloc(14); char *b = malloc(14);
/*@assert (__memory_size == 21); */ /*@assert (__heap_size == 21); */
// Allocation decreases // Allocation decreases
free(a); free(a);
/*@assert (__memory_size == 14); */ /*@assert (__heap_size == 14); */
// Make sure that free with NULL behaves and does not affect allocation // Make sure that free with NULL behaves and does not affect allocation
a = NULL; a = NULL;
free(a); free(a);
/*@assert (__memory_size == 14); */ /*@assert (__heap_size == 14); */
// Realloc decreases allocation // Realloc decreases allocation
b = realloc(b, 9); b = realloc(b, 9);
/*@assert (__memory_size == 9); */ /*@assert (__heap_size == 9); */
// Realloc increases allocation // Realloc increases allocation
b = realloc(b, 18); b = realloc(b, 18);
/*@assert (__memory_size == 18); */ /*@assert (__heap_size == 18); */
// Realloc with 0 is equivalent to free // Realloc with 0 is equivalent to free
b = realloc(b, 0); b = realloc(b, 0);
b = NULL; b = NULL;
/*@assert (__memory_size == 0); */ /*@assert (__heap_size == 0); */
// realloc with 0 is equivalent to malloc // realloc with 0 is equivalent to malloc
b = realloc(b, 8); b = realloc(b, 8);
/*@assert (__memory_size == 8); */ /*@assert (__heap_size == 8); */
// Abandon b and behave like malloc again // Abandon b and behave like malloc again
b = realloc(NULL, 8); b = realloc(NULL, 8);
/*@assert (__memory_size == 16); */ /*@assert (__heap_size == 16); */
// Make realloc fail by supplying a huge number // Make realloc fail by supplying a huge number
b = realloc(NULL, UINTPTR_MAX); b = realloc(NULL, UINTPTR_MAX);
/*@assert (__memory_size == 16); */ /*@assert (__heap_size == 16); */
/*@assert (b == NULL); */ /*@assert (b == NULL); */
// Same as test for calloc ... // Same as test for calloc ...
b = calloc(UINTPTR_MAX,UINTPTR_MAX); b = calloc(UINTPTR_MAX,UINTPTR_MAX);
/*@assert (__memory_size == 16); */ /*@assert (__heap_size == 16); */
/*@assert (b == NULL); */ /*@assert (b == NULL); */
// ... and for malloc // ... and for malloc
b = malloc(UINTPTR_MAX); b = malloc(UINTPTR_MAX);
/*@assert (__memory_size == 16); */ /*@assert (__heap_size == 16); */
/*@assert (b == NULL); */ /*@assert (b == NULL); */
return 0; return 0;
} }
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
+ 36
− 38
View file @ c52b2c7a
/* Generated by Frama-C */ /* Generated by Frama-C */
extern size_t __memory_size;
int main(int argc, char **argv) int main(int argc, char **argv)
{ {
int __retres; int __retres;
...@@ -11,72 +9,72 @@ int main(int argc, char **argv) ...@@ -11,72 +9,72 @@ int main(int argc, char **argv)
__store_block((void *)(& a),8UL); __store_block((void *)(& a),8UL);
__full_init((void *)(& a)); __full_init((void *)(& a));
a = (char *)__e_acsl_malloc((unsigned long)7); a = (char *)__e_acsl_malloc((unsigned long)7);
/*@ assert __memory_size ≡ 7; */ /*@ assert __heap_size ≡ 7; */
e_acsl_assert(__memory_size == (unsigned long)7,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)7,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 7",22); (char *)"main",(char *)"__heap_size == 7",22);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_malloc((unsigned long)14); b = (char *)__e_acsl_malloc((unsigned long)14);
/*@ assert __memory_size ≡ 21; */ /*@ assert __heap_size ≡ 21; */
e_acsl_assert(__memory_size == (unsigned long)21,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)21,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 21",24); (char *)"main",(char *)"__heap_size == 21",24);
__e_acsl_free((void *)a); __e_acsl_free((void *)a);
/*@ assert __memory_size ≡ 14; */ /*@ assert __heap_size ≡ 14; */
e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)14,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 14",28); (char *)"main",(char *)"__heap_size == 14",28);
__full_init((void *)(& a)); __full_init((void *)(& a));
a = (char *)0; a = (char *)0;
__e_acsl_free((void *)a); __e_acsl_free((void *)a);
/*@ assert __memory_size ≡ 14; */ /*@ assert __heap_size ≡ 14; */
e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)14,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 14",33); (char *)"main",(char *)"__heap_size == 14",33);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)9); b = (char *)__e_acsl_realloc((void *)b,(unsigned long)9);
/*@ assert __memory_size ≡ 9; */ /*@ assert __heap_size ≡ 9; */
e_acsl_assert(__memory_size == (unsigned long)9,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)9,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 9",37); (char *)"main",(char *)"__heap_size == 9",37);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)18); b = (char *)__e_acsl_realloc((void *)b,(unsigned long)18);
/*@ assert __memory_size ≡ 18; */ /*@ assert __heap_size ≡ 18; */
e_acsl_assert(__memory_size == (unsigned long)18,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)18,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 18",41); (char *)"main",(char *)"__heap_size == 18",41);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)0); b = (char *)__e_acsl_realloc((void *)b,(unsigned long)0);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)0; b = (char *)0;
/*@ assert __memory_size ≡ 0; */ /*@ assert __heap_size ≡ 0; */
e_acsl_assert(__memory_size == (unsigned long)0,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)0,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 0",46); (char *)"main",(char *)"__heap_size == 0",46);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)8); b = (char *)__e_acsl_realloc((void *)b,(unsigned long)8);
/*@ assert __memory_size ≡ 8; */ /*@ assert __heap_size ≡ 8; */
e_acsl_assert(__memory_size == (unsigned long)8,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)8,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 8",50); (char *)"main",(char *)"__heap_size == 8",50);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)0,(unsigned long)8); b = (char *)__e_acsl_realloc((void *)0,(unsigned long)8);
/*@ assert __memory_size ≡ 16; */ /*@ assert __heap_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",54); (char *)"main",(char *)"__heap_size == 16",54);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)0,18446744073709551615UL); b = (char *)__e_acsl_realloc((void *)0,18446744073709551615UL);
/*@ assert __memory_size ≡ 16; */ /*@ assert __heap_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",58); (char *)"main",(char *)"__heap_size == 16",58);
/*@ assert b ≡ (char *)((void *)0); */ /*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main", e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",59); (char *)"b == (char *)((void *)0)",59);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__calloc(18446744073709551615UL,18446744073709551615UL); b = (char *)__calloc(18446744073709551615UL,18446744073709551615UL);
/*@ assert __memory_size ≡ 16; */ /*@ assert __heap_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",63); (char *)"main",(char *)"__heap_size == 16",63);
/*@ assert b ≡ (char *)((void *)0); */ /*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main", e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",64); (char *)"b == (char *)((void *)0)",64);
__full_init((void *)(& b)); __full_init((void *)(& b));
b = (char *)__e_acsl_malloc(18446744073709551615UL); b = (char *)__e_acsl_malloc(18446744073709551615UL);
/*@ assert __memory_size ≡ 16; */ /*@ assert __heap_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion", e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",68); (char *)"main",(char *)"__heap_size == 16",68);
/*@ assert b ≡ (char *)((void *)0); */ /*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main", e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",69); (char *)"b == (char *)((void *)0)",69);
......
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