如何使用 Frama-c 获取数据和控制依赖切片答案

【问题标题】：How to get Data & Control Dependency Slice using Frama-c如何使用 Frama-c 获取数据和控制依赖切片
【发布时间】：2014-08-06 21:13:32
【问题描述】：

我试图做两件事

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

问题 1：Frama-C 返回的切片没有返回与条件相关的确切语句 - 主要是 if 和 else 语句。

问题 2：如何将切片语句映射回源代码？切片时程序会发生变化（例如：int a=9 成为切片代码中的 2 个语句 int a; 和 a = 9;。）我对切片没问题，但我可以使用哪些信息将这些映射回源代码。

这是源代码。

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 个切片语句映射回源代码语句。

【问题讨论】：

对于问题 2，源程序是“规范化的”，因此在 C 中表达相同事物的数千种方式被减少到最少数量的构造。但是，如果这是返回到您感兴趣的源代码语句的那种映射，您仍然应该能够以编程方式获得赋值 ip1 = 9; 源自文件 t.c 中的第 2 行的信息。

标签： c slice frama-c program-slicing

【解决方案1】：

对于问题 1，测试被切掉，因为它始终为真，因为 option 在主函数中设置为 1。如果要保留测试，则必须将option 设为条目（例如，外部全局变量或main 的参数），但随后，math 函数中将没有任何内容可切片。 . 切片尝试仅保留严格必要的内容，而测试不适用于您的情况。

【讨论】：