Skip to content
Snippets Groups Projects
Commit d0ece096 authored by Allan Blanchard's avatar Allan Blanchard Committed by Virgile Prevosto
Browse files

[wp] update tests oracles

parent c496fa78
No related branches found
No related tags found
No related merge requests found
Showing
with 0 additions and 14 deletions
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing assigns_path.i (no preprocessing) [kernel] Parsing assigns_path.i (no preprocessing)
[kernel:parser:unnamed-typedef] assigns_path.i:1: Warning:
typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
------------------------------------------------------------ ------------------------------------------------------------
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing assigns_path.i (no preprocessing) [kernel] Parsing assigns_path.i (no preprocessing)
[kernel:parser:unnamed-typedef] assigns_path.i:1: Warning:
typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 9 goals scheduled [wp] 9 goals scheduled
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing bts_2079.i (no preprocessing) [kernel] Parsing bts_2079.i (no preprocessing)
[kernel:parser:unnamed-typedef] bts_2079.i:7: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
------------------------------------------------------------ ------------------------------------------------------------
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing bts_2079.i (no preprocessing) [kernel] Parsing bts_2079.i (no preprocessing)
[kernel:parser:unnamed-typedef] bts_2079.i:7: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 2 goals scheduled [wp] 2 goals scheduled
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing dynamic.i (no preprocessing) [kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[kernel:dyncalls] Computing dynamic calls. [kernel:dyncalls] Computing dynamic calls.
[kernel:dyncalls] dynamic.i:32: Calls f1 f2 [kernel:dyncalls] dynamic.i:32: Calls f1 f2
......
# frama-c -wp -wp-no-let [...] # frama-c -wp -wp-no-let [...]
[kernel] Parsing dynamic.i (no preprocessing) [kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[kernel:dyncalls] Computing dynamic calls. [kernel:dyncalls] Computing dynamic calls.
[kernel:dyncalls] dynamic.i:32: Calls f1 f2 [kernel:dyncalls] dynamic.i:32: Calls f1 f2
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing dynamic.i (no preprocessing) [kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] dynamic.i:80: Warning: Missing 'calls' for default behavior [wp] dynamic.i:80: Warning: Missing 'calls' for default behavior
......
# frama-c -wp -wp-no-let [...] # frama-c -wp -wp-no-let [...]
[kernel] Parsing dynamic.i (no preprocessing) [kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 5 goals scheduled [wp] 5 goals scheduled
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing caveat.i (no preprocessing) [kernel] Parsing caveat.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat.i:10: Warning: typedef without a name
[kernel] caveat.i:41: Warning: [kernel] caveat.i:41: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin... [wp] Running WP plugin...
......
# frama-c -wp -wp-model 'Typed (Caveat)' [...] # frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing caveat.i (no preprocessing) [kernel] Parsing caveat.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat.i:10: Warning: typedef without a name
[kernel] caveat.i:41: Warning: [kernel] caveat.i:41: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin... [wp] Running WP plugin...
......
# frama-c -wp -wp-model 'Typed (Caveat)' [...] # frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing caveat2.i (no preprocessing) [kernel] Parsing caveat2.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat2.i:9: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] caveat2.i:14: Warning: Undefined array-size (sint32[]) [wp] caveat2.i:14: Warning: Undefined array-size (sint32[])
......
# frama-c -wp -wp-model 'Typed (Caveat)' [...] # frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing caveat2.i (no preprocessing) [kernel] Parsing caveat2.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat2.i:9: Warning: typedef without a name
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] caveat2.i:14: Warning: Undefined array-size (sint32[]) [wp] caveat2.i:14: Warning: Undefined array-size (sint32[])
......
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