From 40c937b0d31c97d1deb7b2d496915a7ed6207531 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 7 Oct 2020 11:16:12 +0200
Subject: [PATCH] WP hypotheses now have a location
---
tests/bugs/oracle/logiccast.res.oracle | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index 6cc69701..b3163d1b 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -8,11 +8,13 @@ Now output intermediate result
[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unsuccess
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unsuccess: 2)
-[wp] Warning: Memory model hypotheses for function '_Z1mPv':
+[wp] tests/bugs/logiccast.cpp:3: Warning:
+ Memory model hypotheses for function '_Z1mPv':
/*@ behavior typed:
requires \separated(r + (..), &_Z4base); */
void _Z1mPv(void *r);
-[wp] Warning: Memory model hypotheses for function '_Z1nPc':
+[wp] tests/bugs/logiccast.cpp:6: Warning:
+ Memory model hypotheses for function '_Z1nPc':
/*@ behavior typed:
requires \separated(r + (..), &_Z4base); */
void _Z1nPc(char *r);
--
GitLab