--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2010 ---
Dear Frama-C discussers, I submit to you the program below. It raises three questions: a- should the commented functions main and f be parsable by the front-end? Currently, they can't be parsed with either Boron or the development version. The error message is similar to "u.c:14:[kernel] user error: logic label `cond' not found in annotation" b- if they were parsable, should the assertion in each function be provable? c- should the assertion in parsable function g be provable? Pascal ___ #if 0 int main(void) { int i, j; for (i=0; i<=4; i++) { j=i; cond: if (i%2) { odd: j=1; } } /*@ assert \at( \at(j, odd), cond) == 3; */ return 0; } int f(int c, int d) { int i, j; if (c) i=d; if (c) { then: j=1; } /*@ assert \at(i-d, then) == 0; */ return 0; } #endif int g(int c, int d) { int i, j; if (c) goto next1; i=d; next1: if (c) goto next2; then: j=1; next2: /*@ assert \at(i-d, then) == 0; */ return 0; }