Unexpected error: This potentially side-effecting expression is not supported in this position

[weds...@gmail.com]

Hello there,

I was going through the tutorial and ran into the error "This potentially side-effecting expression is not supported in this position, because of C's unspecified evaluation order".

Full details are below, but if I replace "r += sum(n->next)" with "r = sum(n->next)" then everything works fine. I fail to understand why this is unspecified in C; could anyone clarify this? (Or confirm that this is a bug in verifast?)

Thanks,

-Wedson

$ cat ~/tmp/test.c

struct node {

struct node *next;

int value;

};

/*@

predicate nodes(struct node *node, int count) = node == 0 ? count == 0 :

count > 0 &*& node->next |-> ?next &*& node->value |-> _ &*&

malloc_block_node(node) &*& nodes(next, count - 1);

@*/

int sum(struct node *n)

//@ requires nodes(n, ?count);

//@ ensures nodes(n, count);

{

int r = 0;

//@ open nodes(n, count);

if (n) {

r += sum(n->next);

r += n->value;

}

//@ close nodes(n, count);

return r;

}

$./verifast -shared -disable_overflow_check ~/tmp/test.c

/Users/wedsonaf/tmp/test.c

/Users/wedsonaf/tmp/test.c(20,8-11): This potentially side-effecting expression is not supported in this position, because of C's unspecified evaluation order

$ diff ~/tmp/test.c ~/tmp/test1.c

20c20

< r += sum(n->next);

---

> r = sum(n->next);

$ ./verifast -shared -disable_overflow_check ~/tmp/test1.c

/Users/wedsonaf/tmp/test1.c

0 errors found (5 statements verified)

Linking...

Program linked successfully.