Skip to content
Snippets Groups Projects
Commit 5351eaba authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] conforms to EXIT

parent 4e27ffc1
No related branches found
No related tags found
No related merge requests found
/* run.config
EXIT: 0
OPT: -cpp-extra-args="-DFIT"
EXIT: 1
OPT: -cpp-extra-args="-DLARGE"
*/
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
[kernel] tests/wp_plugin/bigarray.c:26: Warning:
[kernel] tests/wp_plugin/bigarray.c:28: Warning:
Cannot represent length of array as an attribute
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
......@@ -8,13 +8,13 @@
Function f
------------------------------------------------------------
Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 25):
Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 27):
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'f':
Effect at line 26
Effect at line 28
Prove: true.
------------------------------------------------------------
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
[kernel] tests/wp_plugin/bigarray.c:26: Warning:
[kernel] tests/wp_plugin/bigarray.c:28: Warning:
Cannot represent length of array as an attribute
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/bigarray.c:26: Warning:
[wp] tests/wp_plugin/bigarray.c:28: Warning:
Array size too large (0xFFFFFFFFFFFFFFFF)
[wp] tests/wp_plugin/bigarray.c:27: Warning:
[wp] tests/wp_plugin/bigarray.c:29: Warning:
Array size too large (0xFFFFFFFFFFFFFFFF)
[wp] tests/wp_plugin/bigarray.c:19: User Error:
[wp] tests/wp_plugin/bigarray.c:21: User Error:
Array size too large (0xFFFFFFFFFFFFFFFF)
[kernel] Plug-in wp aborted: invalid user input.
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