--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on May 2014 ---
Hi everyone, I'm having some difficulty validating a program with the WP RTE plugin. This program validates: /*@ requires \valid(x); */ void a(int *x, const int y) { if (y > 0) { *x = y; } return; } The -wp-rte option gives this output: $ frama-c -wp -wp-rte foo.c [kernel] preprocessing with "gcc -C -E -I. foo.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function a [wp] 1 goal scheduled [wp] [Qed] Goal typed_a_assert_rte_mem_access : Valid [wp] Proved goals: 1 / 1 Qed: 1 But this program does not produce the same result: int b(int x) { return (x > 0); } /*@ requires \valid(x); */ void a(int *x, const int y) { if (b(y) != 0) { *x = y; } return; } Here is the output of Frama-C with the -wp-print option: $ frama-c -wp -wp-rte bar.c -wp-print [kernel] preprocessing with "gcc -C -E -I. bar.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function a [rte] annotating function b [wp] 1 goal scheduled [wp] [Alt-Ergo] Goal typed_a_assert_rte_mem_access : Unknown [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unknown: 1) ------------------------------------------------------------ Function a ------------------------------------------------------------ Goal Assertion 'rte,mem_access' (file bar.c, line 10): Assume { (* Domain *) Type: (is_sint32 b_0). (* Heap *) Have: (linked Malloc_1). (* Pre-condition (file bar.c, line 5) in 'a' *) (* Pre-condition: *) Have: (valid_rw Malloc_1 x_1 1). (* bar.c:9: Then *) Have: 0!=b_0. } Prove: (valid_rw Malloc_0 x_1 1). Prover Alt-Ergo returns Unknown ------------------------------------------------------------ I don't understand why the condition (valid_rw Malloc_0 x_1 1) cannot be shown to be true. Could someone please explain why it is "Unknown"? Thanks for your time. Mansour