为什么对边的全部不进行迭代，导致无限或有限多个环解？

Question

#include<stdio.h>

#define N 6
#define M 10

typedef int bool;
#define true 1
#define false 0

unsigned int nondet_uint();  

typedef unsigned __CPROVER_bitvector[M] bitvector; 

unsigned int zeroTon(unsigned int n) {
   unsigned int result = nondet_uint();
   __CPROVER_assume(result >=0 && result <=n);
   return result ;
};


//Constrine the value between 0 and 1
unsigned int  nondet (){  
  unsigned int num = nondet_uint();
  __CPROVER_assume( num>= 0 && num  <= 1);
  return num;
}; 

void main() {
   unsigned int pos , i, j, k;

   unsigned int len = 0;
   bool Ch , Ck , C0 ;

  bitvector compartment1 , compartment2 , compartment3 , compartment4, compartment5, compartment6;
bitvector nodes[N] = {compartment1, compartment2, compartment3, compartment4, compartment5, compartment6};


// Represent the graph with given topology 
unsigned int graph[N][N];

for(i=0;i <N; i++) {
    for(j=0;j<N;j++) {
        graph[i][j] = nondet();
    }
}



unsigned int p[N] ;
unsigned int ticks;


   //Make sure that graph is one connected  : just find one hamiltonian cycle 
   //make sure elements are in between node no's and all are distinct

for(i=0; i<N; i++) {
    p[i] = zeroTon(5);
}

for(i=0; i <N; i++) {
     for(j=0; (j<N) && (j!=i) ; j++) {    
    if( p[i] != p[j]){
            C1 = C1 && 1;
        }
        else {
            C1 = C1 && 0;
        }

     }
}

 //hamiltonian One exists 
 for(i=0;i<N-1;i++) {
    if( graph[p[i]][p[i+1]] == 1) {
       Ch = Ch && 1;
    }
   else {
       Ch = Ch && 0;
   }
  }

 len =0;
 for(i=0;i<N;i++) {
   for(j=0;j<N; j++){
          if (graph[i][j] == 1) {
              len = len + 1;
          }
    }
  }

  //THIS IS GOING IN INFINITE LOOP ?? WHY ?? 
  for(i=0;i<len;i++) {
   printf("i'm a disco dancer ");

  }
  __CPROVER_assert(!(Ch && C1) , "Graph has an ham path");
}      

我只想得到一个图，它是有哈密顿路径的总节点6。这在上面的代码中运行得很好。但是当我尝试使用连边，即总no.of边时，在cbmc运行中，我会得到无限的展开。

除非我使用len迭代，否则上面的代码运行良好。cbmc进入无限展开?？有人能解释一下吗。

Answer 1

我不确定堆叠溢出的政策，但为了澄清这个问题，我在CBMC支持论坛上贴出了牛津大学的马丁的回答。

除非我使用len迭代，否则上面的代码运行良好。cbmc进入无限循环?？有人能解释一下吗。 简短的回答:是的，这是预期的，使用-放松。 长答案:CBMC对循环边界的检测相对简单；只有当分支条件在符号执行期间静态地简化为false时，它才会停止展开一个循环(没有循环展开限制)。 因为图的值是不确定的，所以连值是不确定的。当然，从其余代码的工作方式中我们知道len <= N*N，但这不能仅通过简化获得，因此CBMC没有“实现”这一点，因此循环展开本身不会终止。 为什么我们不让绑定检测变得更聪明？比如说，变量的跟踪间隔？我们可以，但除非你有一个完整的决定程序在那里，你总是会发现这样的情况。如果您在那里放置了一个完整的决策过程，您可以执行基于路径的符号执行，这是我们的symex工具所做的，或者您正在执行增量式BMC (我们有可用的工具，它们可能被合并到下一个版本的CBMC中)，这取决于您是分别还是一起决定展开和断言。

谢谢大家的帮助。