Skip to content
Snippets Groups Projects
Commit 0f4ee44b authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] update oracles for ill-formed tests with anonymous typedef

parent 9661df55
No related branches found
No related tags found
No related merge requests found
Showing
with 16 additions and 0 deletions
# frama-c -wp [...]
[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] Warning: Missing RTE guards
------------------------------------------------------------
......
# frama-c -wp [...]
[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] Warning: Missing RTE guards
[wp] 9 goals scheduled
......
# frama-c -wp [...]
[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] Warning: Missing RTE guards
------------------------------------------------------------
......
# frama-c -wp [...]
[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] Warning: Missing RTE guards
[wp] 2 goals scheduled
......
# frama-c -wp [...]
[kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin...
[kernel:dyncalls] Computing dynamic calls.
[kernel:dyncalls] dynamic.i:32: Calls f1 f2
......
# frama-c -wp -wp-no-let [...]
[kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin...
[kernel:dyncalls] Computing dynamic calls.
[kernel:dyncalls] dynamic.i:32: Calls f1 f2
......
# frama-c -wp [...]
[kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] dynamic.i:80: Warning: Missing 'calls' for default behavior
......
# frama-c -wp -wp-no-let [...]
[kernel] Parsing dynamic.i (no preprocessing)
[kernel:parser:unnamed-typedef] dynamic.i:21: Warning: typedef without a name
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
......
# frama-c -wp [...]
[kernel] Parsing caveat.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat.i:10: Warning: typedef without a name
[kernel] caveat.i:41: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
......
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing caveat.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat.i:10: Warning: typedef without a name
[kernel] caveat.i:41: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
......
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing caveat2.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat2.i:9: Warning: typedef without a name
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] caveat2.i:14: Warning: Undefined array-size (sint32[])
......
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing caveat2.i (no preprocessing)
[kernel:parser:unnamed-typedef] caveat2.i:9: Warning: typedef without a name
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] caveat2.i:14: Warning: Undefined array-size (sint32[])
......
[kernel] Parsing enum_call.i (no preprocessing)
[kernel:parser:unnamed-typedef] enum_call.i:1: Warning: typedef without a name
/* Generated by Frama-C */
enum E {
C0 = 0,
......
[kernel] Parsing enum.i (no preprocessing)
[kernel:parser:unnamed-typedef] enum.i:5: Warning: typedef without a name
[eva] Analyzing a complete application starting at f
[eva] Computing initial state
[eva] Initial state computed
......
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