--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on August 2013 ---
Hi, Coupling Value and WP to the extensive annotations below (discharged by Value) also allows to discharge the last assert by WP. (This is a very verbose solution, indeed, but might be still readable) HTH, D. frama-c-gui -val -wp -wp-rte bits.c //----------------------------------------------- static unsigned char m[] = { (1 << 7), (1 << 6), (1 << 5), (1 << 4), (1 << 3), (1 << 2), (1 << 1), (1 << 0) }; /*@ requires n >= 0; */ int main(int n) { int size, bit; size = 8; bit = n%size; //@ assert 0 <= bit <= 7; //@ assert m[0] == ((unsigned char)(1 << 7)); //@ assert m[1] == ((unsigned char)(1 << 7-(1%8))); //@ assert m[2] == ((unsigned char)(1 << 7-(2%8))); //@ assert m[3] == ((unsigned char)(1 << 7-(3%8))); //@ assert m[4] == ((unsigned char)(1 << 7-(4%8))); //@ assert m[5] == ((unsigned char)(1 << 7-(5%8))); //@ assert m[6] == ((unsigned char)(1 << 7-(6%8))); //@ assert m[7] == ((unsigned char)(1 << 7-(7%8))); //@ assert m[bit] == ((unsigned char)1 << (7-(n%8))); return 0; } > -----Message d'origine----- > De?: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c- > discuss-bounces at lists.gforge.inria.fr] De la part de David MENTRE > Envoy??: jeudi 29 ao?t 2013 15:48 > ??: Frama-C public discussion > Objet?: Re: [Frama-c-discuss] Proving a simple property on bitshift > with WP