Frama-C - 通过命令行获取函数输入值

问题描述

在GUI上分析下面的代码，可以检查函数div0的输入值。

int div0(int x,int y)                                                                                                                                                                                                                                                                                                 
{                                                                                                                                                                                                                                                                                                                      
  return (x/y);                                                                                                                                                                                                                                                                                                        
}                                                                                                                                                                                                                                                                                                                      
                                                                                                                                                                                                                                                                                                                       
int main()                                                                                                                                                                                                                                                                                                             
{                                                                                                                                                                                                                                                                                                                      
  int res;                                                                                                                                                                                                                                                                                                             
  int a = 4;                                                                                                                                                                                                                                                                                                           
  int b = 2;                                                                                                                                                                                                                                                                                                           
                                                                                                                                                                                                                                                                                                                       
  res = div0(a,b);                                                                                                                                                                                                                                                                                                     
                                                                                                                                                                                                                                                                                                                       
  return 0;                                                                                                                                                                                                                                                                                                            
}

是否可以通过命令行获取此值？

解决方法

在您的情况下，最简单的方法是插入对 Frama_C_show_each 的调用，这是一个特殊的 Frama-C 内置函数，每次解释器通过程序点时，它都会打印给定表达式的内部 Eva 状态。例如：

int div0(int x,int y)
{
  Frama_C_show_each_div0(x,y);
  return (x/y);
}

在修改后的程序上运行 frama-c -eva 将打印：

[eva] file.c:3: Frama_C_show_each_div0: {4},{2}

您可以为您想要的每一行选择 Frama_C_show_each 之后的后缀。例如，如果您更喜欢单独打印每个变量：

int div0(int x,int y)
{
  Frama_C_show_each_x(x);
  Frama_C_show_each_y(y);
  return (x/y);
}

将改为打印：

[eva] file.c:3: Frama_C_show_each_x: {4}
[eva] file.c:4: Frama_C_show_each_y: {2}

对于更复杂的情况，或者为了避免修改源代码，其他替代方案是可能的，但它们可能需要编写一些 OCaml 代码，或者直接修改 Eva，或者添加例如将打印表达式的新抽象域。但对于简单的案例来说，这太过分了。

顺便说一句，如果您希望您的代码仍能正常编译，只需使用 Frama_C_show_each 守卫保护对 #ifdef __FRAMAC__ 的调用：

int div0(int x,int y)
{
#ifdef __FRAMAC__
  Frama_C_show_each_div0(x,y);
#endif
  return (x/y);
}