CBMC Model Checking

Question

I'm trying to constraint the table b[4][4] such that only those places which have i>=j and satisfying the condition that (stored[i] & stored[j]) == stored[i] be 1, and the rest be 0.

Why this is not working?

void main(){
  unsigned int i = 0  , j = 0; 
  _Bool b[4][4];
  bitvector stored[4] = {111,001,010,000};
  for(i=0;i<4;i++){
     for(j=0;j<4;j++){
      __CPROVER_assume( !(b[i][j]) || ((i>=j) && (stored[i] & stored[j] == stored[i])));  
      }
   }

CProver assume trying to get an effect that b[i][j] == 1 should imply stored[i]& stored[j] == stored[i]. But the output doesn't have this effect. What's the problem? I'm new to CBMC and to C also.

David Ranieri · Accepted Answer · 2015-03-05T15:27:33.373

2

Note that values in bitvector stored[4] = {111,001,010,000}; are in base 10.

Do you mean base 2 {0b111,0b001,0b010,0b000}?

edited Mar 05 '15 at 15:27

answered Mar 05 '15 at 14:22

David Ranieri

39,972
7
52
94

Thanks. Added that. But also missed a bracket. ( (stored[i] & stored[j]) == stored[i] ) rather than (stored[i] & stored[j] == stored[i]) – user2754673 Mar 05 '15 at 16:02
Thanks again revisiting and you saved my lot of time. – user2754673 Oct 22 '15 at 13:01

CBMC Model Checking

1 Answers1