3

私は、条件を満たすb[4][4]場所だけが 1 で、残りが 0 になるようにテーブルを制約しようとしています。i>=j(stored[i] & stored[j]) == stored[i]

なぜこれが機能しないのですか？

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も初めてです。

4

1 に答える 1

2

の値は 10 進数であることに注意してくださいbitvector stored[4] = {111,001,010,000};。

ベース2のこと{0b111,0b001,0b010,0b000}ですか？

于 2015-03-05T14:22:12.640 に答える