From 35b4442ffc32b30eecfc55ad575e3bf7211039db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 13 Mar 2020 18:21:47 +0100
Subject: [PATCH] [Eva] Updates test oracles.
---
tests/value/numerors/oracle/numerors.res.oracle | 4 ++--
tests/value/traces/oracle/test1.res.oracle | 2 +-
tests/value/traces/oracle/test2.res.oracle | 2 +-
tests/value/traces/oracle/test3.res.oracle | 2 +-
tests/value/traces/oracle/test4.res.oracle | 2 +-
tests/value/traces/oracle/test5.res.oracle | 2 +-
6 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/tests/value/numerors/oracle/numerors.res.oracle b/tests/value/numerors/oracle/numerors.res.oracle
index 96be7457bfd..6dc3b08df0f 100644
--- a/tests/value/numerors/oracle/numerors.res.oracle
+++ b/tests/value/numerors/oracle/numerors.res.oracle
@@ -1,10 +1,10 @@
-[eva:experimental] Warning: The numerors domain is experimental.
[kernel] Parsing tests/value/numerors/numerors.c (with preprocessing)
[kernel:parser:decimal-float] tests/value/numerors/numerors.c:24: Warning:
Floating-point constant 0.69314718056 is not represented exactly. Will use 0x1.62e42fefa3bdcp-1.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[kernel:typing:implicit-function-declaration] tests/value/numerors/numerors.c:246: Warning:
Calling undeclared function DPRINTFrama_C_domain_show_each_ex10. Old style K&R code?
+[eva:experimental] Warning: The numerors domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -298,7 +298,7 @@
In these functions, 257 statements reached (out of 257): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
+ by the Eva analyzer: 0 errors 1 warning
by the Frama-C kernel: 0 errors 3 warnings
----------------------------------------------------------------------------
0 alarms generated by the analysis.
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 3d86f189430..c89a9da2b49 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test1.c (with preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 200e815eb5c..3e1b821db9e 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test2.i (no preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index 1557613f545..bff1a57599b 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test3.i (no preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index ffd3f1dd1ce..45691fa981c 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test4.i (no preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 0715058c74b..739104c81f0 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -1,7 +1,7 @@
-[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test5.i (no preprocessing)
[kernel:typing:implicit-function-declaration] tests/value/traces/test5.i:21: Warning:
Calling undeclared function my_switch. Old style K&R code?
+[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
--
GitLab