如何使用Frama-c获取数据和控制依赖关系片

Question

我试着做两件事

1. 根据条件获取一个动态的后向切片。
2. 将片语句映射回实际的源代码。

问题1: Frama返回的切片不返回与标准相关的确切语句，主要是if和else语句。

问题2:如何将切片语句映射回源代码？程序在切片时会更改(例如：int a=9变成了切片代码int a;和a = 9;中的2条语句)。我对这个片段很满意，但是我可以使用什么信息将这些信息映射回源代码中的语句。

这是源代码。

void main(){
   int ip1 = 9;
   int ip2 = 3;
   int option = 1;
   int result = math(option,ip1,ip2);    
   //@ slice pragma expr ((option == 1) || !(result == (ip1+ip2)));    
 }   

int math(int option, int a, int b){
   int answer = 0;
   if (option == 1){   
     answer = a+b;
   }else{   
     if (option == 2) {   
       answer = a-b;   
     }else { // a ^ b   
       for(int i=0 ;i<b; i++){   
           answer=answer*a;   
       }   
     }
   }
   return answer;
   }

我使用下面的命令获取切片。

frama-c t.c -slicing-level 3 -slice-pragma main -slice-print

我从frama-c得到的切片是：

void main(void)
{
  int ip1;
  int ip2;
  int option;
  int result;
  ip1 = 9;
  ip2 = 3;
  option = 1;
  result = math_slice_1(ip1,ip2);
  /*@ slice pragma expr option≡1∨!(result≡ip1+ip2); */ ;
  return;
}

int math_slice_1(int a, int b)
{
  int answer;
  answer = a + b;
      return answer;
}

问题1:我没有得到切片中的if和else条件。我该怎么做才能得到它们？

我期望得到以下部分：

    int math_slice_1(int a, int b)    
    {
      int answer;
       if (option == 1){ 
          answer = a + b; 
       }
      return answer;
    }

问题2：

源代码有：int ip1 = 9;

但是切片代码有：

 int ip1;
 ip1 = 9;

如何将这2条切片语句映射回源代码语句。

Answer 1

对于问题1，测试是切分的，因为主函数中的option设置为1，所以它总是正确的。如果您想保留测试，您必须让option成为一个条目(例如外部全局变量或main的一个参数)，但是这样，math函数中就没有什么可以切片的了.切片试图只保留严格必要的内容，而测试并不是在您的情况下。