--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on August 2013 ---
Hello, I would like to prove the property "m[bit] == ((unsigned char)1 << (7-(n%8)))" in the following program using WP but I am currently failing doing so. Any suggestion to help me prove it? I run WP with: frama-c-gui -wp -wp-rte q1_bitshift.c I have tried to use a more detailed memory model with "-wp-model "Typed,int" " without success. I am using Frama-C Fluorine 20130501, Why3 0.81 and Alt-Ergo 0.95.1. === 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[bit] == ((unsigned char)1 << (7-(n%8))); return 0; } ===== Best regards, david