From ec3b31c3daec7e974eb5140318fd867c71ed1438 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jan 2022 14:01:18 +0100
Subject: [PATCH] [wp] Test: line numbers changes
---
src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle | 2 +-
src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle
index ff56ccd82d4..f1c48b4d78f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle
@@ -6,7 +6,7 @@
Function abs
------------------------------------------------------------
-Goal Post-condition (file abs.i, line 15) in 'abs':
+Goal Post-condition (file abs.i, line 14) in 'abs':
Assume {
Type: is_sint32(abs_0) /\ is_sint32(x).
If x < 0
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle
index de8342d87a7..9b59a375817 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing float_format.i (no preprocessing)
-[kernel:parser:decimal-float] float_format.i:10: Warning:
+[kernel:parser:decimal-float] float_format.i:9: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
--
GitLab