CBMC模型检查

Question

我正在尝试约束 table 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 为底。

你是说基数 2 {0b111,0b001,0b010,0b000}？

CBMC模型检查

CBMC Model Checking

c

cbmc