--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on November 2010 ---
Hello, Le lun. 15 nov. 2010 13:24:19 CET, Pascal Cuoq <pascal.cuoq at gmail.com> a ?crit : > 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" No, they shouldn't, at least for now. The ACSL manual (section 2.4.3) explicitely says that the label mentioned in an \at() expression cannot be in an inner block. [disclaimer: what follows is my personal understanding of what the current ACSL says (or would say, supposing that we allow arbitrary labels in \at)] > b- if they were parsable, should the assertion in each function be provable? yes for main: the value of j the last time we reach odd before evaluating the assert is indeed 3. \at(...,cond) does not play any role here, it is subsumed by the inner \at, no for f: then is not reached when c==0, \at(i-d,then) has no defined value. Basically, we can't say much more than \at(i-d,then) == \at(i-d,then). //@ assert \at(c,Pre) != 0 ==> \at(i-d, then) == 0; would be true, though. > > c- should the assertion in parsable function g be provable? no (same reason as for g above). > #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; > } -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98