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，或者添加例如一个新的抽象域，它将打印表达式。但对于简单的情况来说，这太过分了。

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

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