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

Question

在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;                                                                                                                                                                                                                                                                                                            
}

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

Answer 1

在您的情况下，最简单的方法是插入对 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);
}