Skip to content
Snippets Groups Projects
Commit 2710aaa6 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov Committed by Julien Signoles
Browse files

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

parent 18394116
No related branches found
No related tags found
No related merge requests found
......@@ -14,58 +14,58 @@
# endif
# endif
extern size_t __memory_size;
extern size_t __heap_size;
int main(int argc, char **argv) {
// Allocation increases
char *a = malloc(7);
/*@assert (__memory_size == 7); */
/*@assert (__heap_size == 7); */
char *b = malloc(14);
/*@assert (__memory_size == 21); */
/*@assert (__heap_size == 21); */
// Allocation decreases
free(a);
/*@assert (__memory_size == 14); */
/*@assert (__heap_size == 14); */
// Make sure that free with NULL behaves and does not affect allocation
a = NULL;
free(a);
/*@assert (__memory_size == 14); */
/*@assert (__heap_size == 14); */
// Realloc decreases allocation
b = realloc(b, 9);
/*@assert (__memory_size == 9); */
/*@assert (__heap_size == 9); */
// Realloc increases allocation
b = realloc(b, 18);
/*@assert (__memory_size == 18); */
/*@assert (__heap_size == 18); */
// Realloc with 0 is equivalent to free
b = realloc(b, 0);
b = NULL;
/*@assert (__memory_size == 0); */
/*@assert (__heap_size == 0); */
// realloc with 0 is equivalent to malloc
b = realloc(b, 8);
/*@assert (__memory_size == 8); */
/*@assert (__heap_size == 8); */
// Abandon b and behave like malloc again
b = realloc(NULL, 8);
/*@assert (__memory_size == 16); */
/*@assert (__heap_size == 16); */
// Make realloc fail by supplying a huge number
b = realloc(NULL, UINTPTR_MAX);
/*@assert (__memory_size == 16); */
/*@assert (__heap_size == 16); */
/*@assert (b == NULL); */
// Same as test for calloc ...
b = calloc(UINTPTR_MAX,UINTPTR_MAX);
/*@assert (__memory_size == 16); */
/*@assert (__heap_size == 16); */
/*@assert (b == NULL); */
// ... and for malloc
b = malloc(UINTPTR_MAX);
/*@assert (__memory_size == 16); */
/*@assert (__heap_size == 16); */
/*@assert (b == NULL); */
return 0;
}
/* Generated by Frama-C */
extern size_t __memory_size;
int main(int argc, char **argv)
{
int __retres;
......@@ -11,72 +9,72 @@ int main(int argc, char **argv)
__store_block((void *)(& a),8UL);
__full_init((void *)(& a));
a = (char *)__e_acsl_malloc((unsigned long)7);
/*@ assert __memory_size ≡ 7; */
e_acsl_assert(__memory_size == (unsigned long)7,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 7",22);
/*@ assert __heap_size ≡ 7; */
e_acsl_assert(__heap_size == (unsigned long)7,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 7",22);
__full_init((void *)(& b));
b = (char *)__e_acsl_malloc((unsigned long)14);
/*@ assert __memory_size ≡ 21; */
e_acsl_assert(__memory_size == (unsigned long)21,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 21",24);
/*@ assert __heap_size ≡ 21; */
e_acsl_assert(__heap_size == (unsigned long)21,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 21",24);
__e_acsl_free((void *)a);
/*@ assert __memory_size ≡ 14; */
e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 14",28);
/*@ assert __heap_size ≡ 14; */
e_acsl_assert(__heap_size == (unsigned long)14,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 14",28);
__full_init((void *)(& a));
a = (char *)0;
__e_acsl_free((void *)a);
/*@ assert __memory_size ≡ 14; */
e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 14",33);
/*@ assert __heap_size ≡ 14; */
e_acsl_assert(__heap_size == (unsigned long)14,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 14",33);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)9);
/*@ assert __memory_size ≡ 9; */
e_acsl_assert(__memory_size == (unsigned long)9,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 9",37);
/*@ assert __heap_size ≡ 9; */
e_acsl_assert(__heap_size == (unsigned long)9,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 9",37);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)18);
/*@ assert __memory_size ≡ 18; */
e_acsl_assert(__memory_size == (unsigned long)18,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 18",41);
/*@ assert __heap_size ≡ 18; */
e_acsl_assert(__heap_size == (unsigned long)18,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 18",41);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)0);
__full_init((void *)(& b));
b = (char *)0;
/*@ assert __memory_size ≡ 0; */
e_acsl_assert(__memory_size == (unsigned long)0,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 0",46);
/*@ assert __heap_size ≡ 0; */
e_acsl_assert(__heap_size == (unsigned long)0,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 0",46);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)b,(unsigned long)8);
/*@ assert __memory_size ≡ 8; */
e_acsl_assert(__memory_size == (unsigned long)8,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 8",50);
/*@ assert __heap_size ≡ 8; */
e_acsl_assert(__heap_size == (unsigned long)8,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 8",50);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)0,(unsigned long)8);
/*@ assert __memory_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",54);
/*@ assert __heap_size ≡ 16; */
e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 16",54);
__full_init((void *)(& b));
b = (char *)__e_acsl_realloc((void *)0,18446744073709551615UL);
/*@ assert __memory_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",58);
/*@ assert __heap_size ≡ 16; */
e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 16",58);
/*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",59);
__full_init((void *)(& b));
b = (char *)__calloc(18446744073709551615UL,18446744073709551615UL);
/*@ assert __memory_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",63);
/*@ assert __heap_size ≡ 16; */
e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 16",63);
/*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",64);
__full_init((void *)(& b));
b = (char *)__e_acsl_malloc(18446744073709551615UL);
/*@ assert __memory_size ≡ 16; */
e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__memory_size == 16",68);
/*@ assert __heap_size ≡ 16; */
e_acsl_assert(__heap_size == (unsigned long)16,(char *)"Assertion",
(char *)"main",(char *)"__heap_size == 16",68);
/*@ assert b ≡ (char *)((void *)0); */
e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",69);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment