--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on October 2015 ---
Hello, Le 15/10/2015 09:16, GERARD Benoit a écrit : > My question is the following : is this problem potentially solvable (by > frama-c developers or may be using ACSL) Interesting issue! :-) I tried various approaches but the only one that worked for me was to put an assert that "bound <= 10" in test2() (see attached code) and then use wp to prove it (easy for Alt-Ergo in 21ms): frama-c-gui -val min-example.c -then -wp > or should people take the habit > of using an intermediate variable to perform computations before using > it in the macro (which option may ease the code review and avoid some > errors anyway)? But it is true that using an intermediate variable helps Value: no need of additional annotation and use of WP. So if you have the ability to guide people to use this style, I would go for it. Best regards, david -------------- next part -------------- #include "__fc_builtin.h" #define MIN(a,b) (((a)<(b))?(a):(b)) void test1() { char tab[10]; int i, a = Frama_C_interval(0,1000), b = 10; int bound = MIN(a,b); for ( i = 0 ; i < bound ; i ++ ) tab[i] = i; } void test2() { char tab[10]; int i, a = Frama_C_interval(0,1000), b = 10; int bound = MIN(a & 0xFF,b); //@ assert bound <= 10; for ( i = 0 ; i < bound ; i ++ ) tab[i] = i; } void test3() { char tab[10]; int i, a = Frama_C_interval(0,1000), b = 10; int atemp = a & 0xFF; int bound = MIN(atemp,b); for ( i = 0 ; i < bound ; i ++ ) tab[i] = i; } int main() { test1(); test2(); test3(); return 0; }