Skip to content
Snippets Groups Projects
Commit ec3b31c3 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Test: line numbers changes

parent 694d9564
No related branches found
No related tags found
No related merge requests found
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
Function abs Function abs
------------------------------------------------------------ ------------------------------------------------------------
Goal Post-condition (file abs.i, line 15) in 'abs': Goal Post-condition (file abs.i, line 14) in 'abs':
Assume { Assume {
Type: is_sint32(abs_0) /\ is_sint32(x). Type: is_sint32(abs_0) /\ is_sint32(x).
If x < 0 If x < 0
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing float_format.i (no preprocessing) [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. 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) (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin... [wp] Running WP plugin...
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment