frama-c

RTE Assertions Dependent on *Unknown* Post-conditions Are Proved *Surely Valid*

WP distinguishes these two classes of properties: surely valid and valid under hypotheses (see Sect 2.1, Page 15 of WP Plug-in Manual). However, I observe an RTE assertion (rte_4, *p_1 + 1 <= INT_MAX at search.c:39) being marked surely valid (Figure 1) despite depending on an unproven post-condition (ensures \result == \null || *\result <= INT_MAX-1 at search.c:7, see Figure 2). This occurs when running frama-c search.c -wp -then -report (See the report and Figures 1-2).

Futhermore, foo() lacks pre-conditions to enforce search()'s requirements at the call site (line 35). This allows violations when invalid inputs are passed (e.g, main() passing NULL at line 46), yet assertions depending on search()'s post-conditions (e.g., rte_2/rte_3 in foo()) are marked surely valid.

I understand the current behavior might reflect the WP's strategy for property classfication. However, I still have some questions:

search.c:

#include <stddef.h>
#include <limits.h>

/*@
requires \valid(array + (0 .. length-1));
ensures \result == \null || \valid(\result);
ensures \result == \null || *\result <= INT_MAX-1;
*/
int *search(int *array, size_t length, int element)
{
  int *__retres;
  {
    size_t i = (size_t)0;
    /*@
    loop invariant 0 <= i <= length;
    loop invariant \valid_read(array + (0 .. length-1));
    loop assigns i;
    loop variant length - i;
    */
    while (i < length) {
      /*@ assert rte_1: mem_access: \valid_read(array + i); */
      if (*(array + i) == element) {
        __retres = array + i;
        goto return_label;
      }
      i ++;
    }
  }
  __retres = (int *)0;
  return_label: return __retres;
}

void foo(int *array, size_t length)
{
  int *p_1 = search(array,length,0);
  if (p_1) 
    /*@ assert rte_2: mem_access: \valid(p_1); */
    /*@ assert rte_3: mem_access: \valid_read(p_1); */
    /*@ assert rte_4: signed_overflow: *p_1 + 1 ≤ INT_MAX; */
    (*p_1) ++;
}

void main(void)
{
  int array[5] = {0, 1, 2, 3, 4};
  foo(NULL,(size_t)5);
  return;
}

The report of frama-c search.c -wp -then -report:

--------------------------------------------------------------------------------
--- Properties of Function 'search'
--------------------------------------------------------------------------------

[    -    ] Pre-condition (file search.c, line 5)
            tried with Call Preconditions.
[  Valid  ] Post-condition (file search.c, line 6)
            by Wp.typed.
[    -    ] Post-condition (file search.c, line 7)
            tried with Wp.typed.
[  Valid  ] Exit-condition (generated)
            by Unreachable Annotations.
[  Valid  ] Termination-condition (generated)
            by Trivial Termination.
[  Valid  ] Loop assigns (file search.c, line 17)
            by Wp.typed.
[  Valid  ] Loop variant at loop (file search.c, line 20)
            by Wp.typed.
[  Valid  ] Invariant (file search.c, line 15)
            by Wp.typed.
[  Valid  ] Invariant (file search.c, line 16)
            by Wp.typed.
[  Valid  ] Assertion 'rte_1,mem_access' (file search.c, line 21)
            by Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.

--------------------------------------------------------------------------------
--- Properties of Function 'foo'
--------------------------------------------------------------------------------

[  Valid  ] Exit-condition (generated)
            by Wp.typed.
[  Valid  ] Termination-condition (generated)
            by Wp.typed.
[  Valid  ] Assertion 'rte_2,mem_access' (file search.c, line 37)
            by Wp.typed.
[  Valid  ] Assertion 'rte_3,mem_access' (file search.c, line 38)
            by Wp.typed.
[  Valid  ] Assertion 'rte_4,signed_overflow' (file search.c, line 39)
            by Wp.typed.
[  Valid  ] Default behavior
            by Frama-C kernel.
[    -    ] Instance of 'Pre-condition (file search.c, line 5)' at initialization of 'p_1' (file search.c, line 35)

            tried with Wp.typed.

--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------

[  Valid  ] Exit-condition (generated)
            by Wp.typed.
[  Valid  ] Termination-condition (generated)
            by Wp.typed.
[  Valid  ] Default behavior
            by Frama-C kernel.

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
    17 Completely validated
     4 To be validated
    21 Total
--------------------------------------------------------------------------------

Figure 1 (properties rte_2, rte_3, rte_3 in foo() are marked as surely valid): Figure 1 (properties rte_2, rte_3, rte_3 in foo() are marked as surely valid)

Figure 2 (one post-condition of search() is unknown): Figure 2 (one post-condition of search() is unknown)

Figure 3 (valid-under-hypotheses properties reported together with their dependency listings by the plug-in report): Figure 2 (valid-under-hypotheses properties reported together with their dependency listings by the plug-in report)

Solution

  • First, you should note that it is not WP itself that marks the annotation as completely or partially validated. Plug-ins only give a local status, and optionally a set of dependencies (annotation that have been assumed valid to prove the current one). It is then up to the kernel to consolidate all statuses and dependencies information into a global status, according to a complex algorithm described in an paper from FMICS'12.

    Apparently, Wp does not give post-conditions as dependencies of the annotations of the caller, so that the consolidation algorithm does not take them into account (this is a case of weak correctness of analyzers in the referenced paper). More generally, the only thing that is guaranteed by Frama-C is that if every annotation is marked as valid, then the program is correct with respect to its specification (theorem 1 of the paper, in the case where only Valid local statuses are emitted). The Valid_under_hypothesis status is a refinement, but without completeness guarantees.