c - CBMC模型检查

Question

我试图约束表b[4][4]，使得只有那些具有i>=j并满足条件(stored[i] & stored[j]) == stored[i]为 1 的地方，其余为 0。

为什么这不起作用？

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 假设试图获得b[i][j] == 1应该暗示的效果stored[i]& stored[j] == stored[i]。但是输出没有这个效果。有什么问题？我是 CBMC 和 C 的新手。

Answer 1

请注意，其中的值以bitvector stored[4] = {111,001,010,000};10 为底。

你的意思是base 2 {0b111,0b001,0b010,0b000}？