我想做两件事
- 根据条件获取动态后向切片。
- 将切片语句映射回实际的源代码。
问题 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 个切片语句映射回源代码语句。
最佳答案
对于问题 1,测试被切出,因为它始终为真,因为 option
在 main 函数中设置为 1。如果你想保持测试,你必须让 option
成为一个条目(例如外部全局变量或 main
的参数),但是之后,什么都没有在 math
函数中切片......切片试图只保留绝对必要的部分,而测试不在你的情况下。
关于c - 如何使用 Frama-c 获取数据和控制依赖性切片,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25170330/