ACSL list example in the documentation generate a bad sounding warning

Question

I tried the list example (Example 2.23 on page 37, in Section "Function Contracts") from the ACSL manual, but I hid the implementation of incr_list and changed the return type. Full source below.

struct list {
  int hd;
  struct list *next;
};

/*@ inductive reachable{L} (struct list *root,struct list *to) {
  @ case empty{L}: \forall  struct list *l; reachable(l,l) ;
  @ case non_empty{L}:\forall struct list *l1,*l2;
  @ \valid(l1) && reachable(l1->next,l2) ==> reachable(l1,l2) ;
  @ }
  */

// The requires clause forbids giving a circular list
/*@ requires reachable(p,\null);
  @ assigns \result \from { q->hd | struct list *q ; reachable(p,q) } ;
  @
*/
int incr_list(struct list *p);

int main() {
  struct list l = {.hd=0, .next=0};
  struct list l2 = {.hd=1, .next=&l};
  return incr_list(&l2);
}

I am running this with the slicer frama-c test-1.c -slice-calls incr_list -then-last -print. The output seems fine, but I worry about the warnings that are generated when running this command:

[inout] test-1.c:23: Warning: 
  failed to interpret inputs in assigns clause 'assigns \result
                                                  \from {q->hd |
                                                         struct list *q
                                                         ; reachable{Old}(p, q)};'
[eva:alarm] test-1.c:23: Warning: 
  function incr_list: precondition got status unknown.
[eva] test-1.c:23: Warning: 
  cannot interpret 'from'
  clause 'assigns \result \from {q->hd | struct list *q; reachable{Old}(p, q)};'
  (error in AST: non-lval term {q->hd | struct list *q; reachable{Old}(p, q)}; please report)

In particular the first and third one. It seems like something unexpected is happening? I don't quite understand what exact issue the tool is having here.

score 1 · Answer 1 · answered Jun 09 '20 at 07:54

The last line of Eva's warning is indeed a bit frightening, and ought to be further investigated, as the \from part is perfectly legitimate (it basically says that the value returned by incr_list depends on all the elements contained in the list passed as arguments). On the other hand, Eva does not know how to interpret set comprehension (not to mention the fact that the reachable inductive predicate is also outside of its capabilities), and the cannot interpret 'from' clause part of the warning is completely true.

This in turn might have an impact on the slicing, since it means that data dependencies between the value returned by incr_list and its parameter are not represented accurately. More generally, all Eva-based analyses dealing with dependencies (from, inout, slicing, impact, ...) need \from clauses that Eva can interpret, or stub definitions for the corresponding functions (if you have a definition, Eva won't need a specification).

ACSL list example in the documentation generate a bad sounding warning

1 Answers1