--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP RTE mem_access condition is Unknown



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