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 ff56ccd82d47ba9925f56af23dc6b638f2cea456..f1c48b4d78f3584846dd4ebf21e8e0c605669c4f 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 de8342d87a74aa1c4d12bb1bd09b641a3bce47b3..9b59a37581730e0e503c2db1faa20b405c61be8f 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...