From 05573c96aeccb123555814e51f6b595da2ae178d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 19 Aug 2019 14:07:56 +0200
Subject: [PATCH] [Eva] Updates test oracles.
---
tests/builtins/oracle/memchr.res.oracle | 16 ++++++++--------
1 file changed, 8 insertions(+), 8 deletions(-)
diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle
index 94cae8ab088..d77c490f0c7 100644
--- a/tests/builtins/oracle/memchr.res.oracle
+++ b/tests/builtins/oracle/memchr.res.oracle
@@ -100,8 +100,8 @@
[eva] tests/builtins/memchr.c:122: Call to builtin memchr
[eva:alarm] tests/builtins/memchr.c:122: Warning:
function memchr: precondition 'valid' got status unknown.
-[eva] tests/builtins/memchr.c:122:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:122: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva:alarm] tests/builtins/memchr.c:122: Warning:
function memchr: precondition 'danglingness' got status unknown.
[eva] tests/builtins/memchr.c:128: Call to builtin memchr
@@ -134,8 +134,8 @@
[eva] tests/builtins/memchr.c:145: Call to builtin memchr
[eva] tests/builtins/memchr.c:145:
function memchr: precondition 'valid' got status valid.
-[eva] tests/builtins/memchr.c:145:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:145: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva] tests/builtins/memchr.c:145:
function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:145: Frama_C_show_each_mymemchr: {1}
@@ -143,8 +143,8 @@
[eva] tests/builtins/memchr.c:152: Call to builtin memchr
[eva] tests/builtins/memchr.c:152:
function memchr: precondition 'valid' got status valid.
-[eva] tests/builtins/memchr.c:152:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:152: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva] tests/builtins/memchr.c:152:
function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:152: Frama_C_show_each_mymemchr: {3}
@@ -443,8 +443,8 @@
[eva] tests/builtins/memchr.c:348: Call to builtin memchr
[eva] tests/builtins/memchr.c:348:
function memchr: precondition 'valid' got status valid.
-[eva] tests/builtins/memchr.c:348:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:348: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva] tests/builtins/memchr.c:348:
function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:348: Frama_C_show_each_mymemchr: {1}
--
GitLab