How do I debug ACSL in frama-c?

Question

I'm trying to learn ACSL but am stumbling with trying to write a complete specification. My code

#include <stdint.h>
#include <stddef.h>

#define NUM_ELEMS (8)

/*@ requires expected != test;
  @ requires \let n = NUM_ELEMS;
  @          \valid_read(expected + (0.. n-1)) && \valid_read(test + (0.. n-1));
  @ assigns \nothing;
  @ behavior matches:
  @   assumes \let n = NUM_ELEMS;
  @           \forall integer i; 0 <= i < n ==> expected[i] == test[i];
  @   ensures \result == 1;
  @ behavior not_matches:
  @   assumes \let n = NUM_ELEMS;
  @           \exists integer i; 0 <= i < n && expected[i] != test[i];
  @   ensures \result == 0;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
int array_equals(const uint32_t expected[static NUM_ELEMS], const uint32_t test[static NUM_ELEMS]) {
  for (size_t i = 0; i < NUM_ELEMS; i++) {
    if (expected[i] != test[i]) {
      return 0;
    }
  }
  return 1;
}

I run it with

frama-c -wp -wp-rte test.c

and I see the following log

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
[rte] annotating function array_equals
test.c:22:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_equals_assign_part1 : Unknown (Qed:2ms) (67ms)
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access_2 : Unknown (Qed:2ms) (128ms)
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access : Unknown (Qed:2ms) (125ms)
[wp] [Alt-Ergo] Goal typed_array_equals_matches_post : Unknown (Qed:10ms) (175ms)
[wp] [Alt-Ergo] Goal typed_array_equals_not_matches_post : Unknown (Qed:7ms) (109ms)
[wp] Proved goals:    4 / 9
     Qed:             4  (0.56ms-4ms)
     Alt-Ergo:        0  (unknown: 5)

So it seems like my two behaviors and the "assigns \nothing" couldn't be proved. So how do I proceed from here?

EDIT: So I figured out the immediate problem. I have no annotate my loop:

  /*@ loop invariant \let n = NUM_ELEMS; 0 <= i <= n;
    @ loop invariant \forall integer k; 0 <= k < i ==> expected[k] == test[k];
    @ loop assigns i;
    @ loop variant \let n = NUM_ELEMS; n-i;
    @*/

My larger question still stands: what's a good way to debug problems? I solved this one by just changing and deleting code and seeing what is proved/not proved.

Answer 1

I'm afraid there cannot be a definitive answer to this question (to be honest, I have considered voting to close it as "too broad"). Here are however a few guidelines that will probably help you in your proof attempts:

Identifying individual clauses

ACSL specifications are quickly composed of many clauses (requires, ensures, loop invariant, assert, ...). It is important to be able to easily distinguish between them. For that, you have two main ingredients:

1. Use the GUI. It makes it much easier to see which annotations are proved (green bullet), proved but under the hypothesis that other, unproved clauses are true (green/yellow), or unproved (yellow).
2. Name your clauses: any ACSL predicate can be attached a name, with the syntax name: pred. When a clause is equipped with a name, WP will use it to refer to the clause.

Usual suspects

It is very easy to miss some very important part of a specification. Here is a quick check list:

1. All loops must be equipped with loop invariant and loop assigns
2. All functions called by the one under analysis must have a contract (with at least an assigns clause)
3. If a memory location mentioned in a loop assigns is not subject of a corresponding loop invariant, you know nothing about the value stored at that location outside of the loop. This might be an issue.

Debugging individual clauses

Once you're confident that you haven't missed anything obvious, it is time to start investigating on specific clauses.

1. Usually, it is much easier to verify that a loop invariant is established (i.e. true when attaining the loop for the first time) rather than preserved (staying true across a of loop step). If you can't establish a loop invariant, it is either wrong, or you forgot some requires to constraint the input of the function (a typical case for algorithm over arrays is loop invariant 0<=i<=n; that can't be proved if you don't requires n>=0;)
2. Similarly assigns and loop assigns should be easier to verify than real functional properties. As long as they are not all proved, you should concentrate on them (a common error is to forget to put the index of a loop in its loop assigns, or to mention that it assigns a[i] and not a[0..i]). Don't forget that assigns must include all possible assignments, including the ones done in callees.
3. Don't hesitate to use assert to check whether WP can prove that a property holds at a given point. This will help you understand where the problems arise. [ edit according to @DavidMENTRÉ's comment below ] Note that in that case, you should take care of the fact that the initial proof obligation might succeed under the hypothesis that the assert holds while the assert itself is not validated. In the GUI, this is reflected by a green/yellow bullet, and of course a yellow bullet in front of the assert. In that case, the proof is not over yet, and you have to understand why the assert is not proved, possibly using the same strategy as above, until you understand exactly where the problem lies.