From 4563cbf8ffc36c152053b886925fb6655650aa0b Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 4 Oct 2021 17:43:20 +0200
Subject: [PATCH] [eacsl] Fix init_function.c test
---
.../e-acsl/tests/memory/init_function.c | 18 ++++++++++++------
1 file changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/tests/memory/init_function.c b/src/plugins/e-acsl/tests/memory/init_function.c
index 133c99f201d..0b6f90eb086 100644
--- a/src/plugins/e-acsl/tests/memory/init_function.c
+++ b/src/plugins/e-acsl/tests/memory/init_function.c
@@ -1,13 +1,19 @@
/* run.config
- COMMENT: Check if 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: is required tracking
+ COMMENT: Check that the instrumentation engine still adds __e_acsl_memory_init
+ COMMENT: if no variable is instrumented.
+ STDOPT: +"-eva-no-builtins-auto"
*/
#include <stdlib.h>
+extern size_t __e_acsl_heap_allocation_size;
+
int main(void) {
- /* @assert (__heap_allocation_size == 0); */
- char *a = malloc(7);
- /* @assert (__heap_allocation_size == 7); */
+ // The asserts check that the memory model of E-ACSL is correctly initialized
+ // and updated, but since no memory predicate is used the variable `a` does
+ // 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; */
}
--
GitLab