From 4081fb2bc198a2f277ea2feda06f9b5b0e25110e Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 4 Oct 2021 17:43:29 +0200
Subject: [PATCH] [eacsl] Update oracles
---
.../e-acsl/tests/memory/oracle/gen_init_function.c | 10 ++++++++++
.../tests/memory/oracle/init_function.res.oracle | 10 ++++++++++
2 files changed, 20 insertions(+)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
index 7a579dc32d3..0f80a70efb1 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
@@ -4,11 +4,21 @@
#include "stdlib.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+extern size_t __e_acsl_heap_allocation_size;
+
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,1,"Assertion","main",
+ "__e_acsl_heap_allocation_size == 0",
+ "tests/memory/init_function.c",16);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 0; */ ;
char *a = malloc((unsigned long)7);
+ __e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,1,"Assertion","main",
+ "__e_acsl_heap_allocation_size == 7",
+ "tests/memory/init_function.c",18);
+ /*@ assert __e_acsl_heap_allocation_size ≡ 7; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
index efd02631129..f8f3e0f93f7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
@@ -1,2 +1,12 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/init_function.c:16: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/init_function.c:16: Warning:
+ assertion got status unknown.
+[eva] tests/memory/init_function.c:17: Warning:
+ ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/init_function.c:18: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/init_function.c:18: Warning:
+ assertion got status unknown.
--
GitLab