From 44d98ec01166f9ca41ed1b17467ac9c5cb7a95a3 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 16 Jun 2020 17:50:16 +0200
Subject: [PATCH] [eacsl] Update tests
---
src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
index 646d3b85588..d2039f2b5ee 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
@@ -2,12 +2,6 @@
#include "stdio.h"
#include "stdlib.h"
int LEN = 10;
-/*@ assigns \nothing;
- frees p; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *p);
-
-/* compiler builtin:
- __attribute__((__FC_BUILTIN__)) void *__builtin_alloca(unsigned long size); */
int main(int argc, char **argv)
{
int __retres;
@@ -67,6 +61,7 @@ int main(int argc, char **argv)
}
__retres = 0;
__e_acsl_delete_block((void *)arr);
+ /* __fc_vla_free((void *)arr); */
__e_acsl_delete_block((void *)(& arr));
__e_acsl_memory_clean();
return __retres;
--
GitLab