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

[wp] Init now supported

parent df7c54da
No related branches found
No related tags found
No related merge requests found
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unsupported_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unsupported_init.i:1: Warning:
Allocation, initialization and danglingness not yet implemented
(r1: \initialized(Y + (0 .. 99)))
------------------------------------------------------------
Function f
------------------------------------------------------------
Goal Assertion 'a1' (file tests/wp_plugin/unsupported_init.i, line 9):
tests/wp_plugin/unsupported_init.i:1: warning from wp:
- Warning: Ignored Hypothesis
Reason: Allocation, initialization and danglingness not yet implemented
(r1: \initialized(Y + (0 .. 99)))
Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition 'r1' in 'cp'' in 'f' at call 'cp' (file tests/wp_plugin/unsupported_init.i, line 8)
:
tests/wp_plugin/unsupported_init.i:1: warning from wp:
- Warning: Target turned to False, looking for context inconsistency
Reason: Allocation, initialization and danglingness not yet implemented
(r1: \initialized(Y + (0 .. 99)))
Prove: false.
------------------------------------------------------------
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unsupported_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unsupported_init.i:1: Warning:
Allocation, initialization and danglingness not yet implemented
(r1: \initialized(Y + (0 .. 99)))
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
[wp] [Alt-Ergo] Goal typed_f_call_cp_requires_r1 : Unsuccess (Degenerated)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 1 - 2 50.0%
------------------------------------------------------------
/*@ requires r1: \initialized(Y+(0 .. 99));
assigns X[0..99];
ensures X[0] == Y[0];
*/
void cp( int *X, int *Y );
void f (int *A, int *B) {
cp(B, A);
/*@ assert a1: A[0] == B[0]; */
}
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