0

次のコードには、呼び出し規約エラー (永久ループにつながる可能性があります) があり、それを検出できません。「Satabs」を使用してコードを検証しようとします。どのようなモデルがエラーを表面化させることができますか。次のモデルでは、segfault が発生します。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);  
}
4

2 に答える 2

0

私は「サタブ」を知りませんが、私にとって無限ループの最も有望な候補は

while(!res&&iter->next<TMAX){
  res=trans(iter->next,iter->src,dst);
  iter->next++;
}

他のすべてのループは、修正カウントのように見えます。このループは、いわゆる呼び出し規則エラーがなくても、それ自体が危険である可能性があります。

とにかく、関数transの呼び出しだけでなく、それに対する呼び出しツリー全体を確認する必要があります。

そこにコードを貼り付けることもできます

http://gimpel-online.com//cgi-bin/genPage.py?srcFile=intro.txt&cgiScript=analyseCode.py&title=Introduction+and+Welcome&intro=Introducing+the+testing+facility&compilerOption=online32.lnt&in

もう少しヒントが得られるかもしれません。

推測：

'Satabs' は、次のような未定義のプリプロセッサ条件を好まないのかもしれません。

#if MODEL==1
于 2016-04-12T07:42:08.353 に答える