From 4e848baf2a0f77f77a0eab3b45b2b6814c757e82 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 15 Nov 2017 20:27:21 +0100
Subject: [PATCH] update oracles wrt kernel changes
---
.../e-acsl/tests/runtime/oracle/initialized.res.oracle | 6 +++---
.../e-acsl/tests/temporal/oracle/t_getenv.res.oracle | 2 +-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index 468779b708f..af9ba72736c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -3,11 +3,11 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:348:[value] warning: function realloc: precondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:363:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:358:[value] warning: function realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:373:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
tests/runtime/initialized.c:75:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:77:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:335:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:345:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:86:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index 729b206a280..52d9faea614 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -2,6 +2,6 @@
[e-acsl] warning: annotating undefined function `getenv':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:407:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:417:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
--
GitLab