Skip to content
Snippets Groups Projects
Commit 4563cbf8 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Fix init_function.c test

parent f7806a61
No related branches found
No related tags found
No related merge requests found
/* run.config /* run.config
COMMENT: Check if the instrumentation engine still adds __e_acsl_memory init COMMENT: Check that the instrumentation engine still adds __e_acsl_memory_init
COMMENT: is inserted for the case when no malloc is used but no no variable COMMENT: if no variable is instrumented.
COMMENT: is required tracking STDOPT: +"-eva-no-builtins-auto"
*/ */
#include <stdlib.h> #include <stdlib.h>
extern size_t __e_acsl_heap_allocation_size;
int main(void) { int main(void) {
/* @assert (__heap_allocation_size == 0); */ // The asserts check that the memory model of E-ACSL is correctly initialized
char *a = malloc(7); // and updated, but since no memory predicate is used the variable `a` does
/* @assert (__heap_allocation_size == 7); */ // not need to be instrumented (ie. no `store_block` and `delete_block` are
// generated).
/*@ assert __e_acsl_heap_allocation_size == 0; */
char *a = malloc(7);
/*@ assert __e_acsl_heap_allocation_size == 7; */
} }
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