在下面的代码中有一个调用约定错误（可能导致一个永恒的循环），我无法检测到它。我尝试使用“Satabs”验证代码。什么样的模型可以使错误浮出水面。使用以下模型，我得到一个段错误。通过改变 VLEN 和 TMAX 你可以玩一点。
- Q1。什么是调用约定错误？
- Q2。哪种模型最适合用于查找错误？
#include <stdio.h>
#if MODEL==1
#define VLEN 3
#define TMAX 4
int trans(int T,int*src,int*dst){
if (T < VLEN && T < TMAX && src[T] < 4){
dst[T]=src[T]+1;
return 1;
} else {
return 0;
}
}
#endif
struct next_state {
int next;
int src[VLEN];
};
typedef struct next_state *iterator_t;
void init(iterator_t iter,int *src){
for(int i=0;i<VLEN;i++){
iter->src[i]=src[i];
}
iter->next=0;
}
int next(iterator_t iter,int *dst){
#ifdef FIX_ARRAY
for(int i=0;i<VLEN;i++){
#else
for(int i=0;i<TMAX;i++){
#endif
dst[i]=iter->src[i];
}
int res=0;
while(!res&&iter->next<TMAX){
res=trans(iter->next,iter->src,dst);
iter->next++;
}
return res;
}
int find_depth(iterator_t iter,int *src){
int table[VLEN*TMAX];
int N=0;
init(iter,src);
for(int i=0;i<TMAX;i++){
if(next(iter,&(table[N*VLEN]))){
N++;
}
}
int depth=0;
for(int i=0; i<N;i++){
printf("Eimai stin for \n");
int tmp=find_depth(iter,&(table[i*VLEN]));
printf("tmp= %d\n",tmp);
if(tmp>=depth){
depth=tmp+1;
//assert(depth);
}
}
printf("\n\n");
return depth;
}
int main(int argc,char*argv[]){
int state[VLEN];
struct next_state ns;
for(int i=0;i<VLEN;i++){
state[i]=0;
}
int depth=find_depth(&ns,state);
printf("depth is %d\n",depth);
}