如何跟踪C源代码和Frama-C预处理代码之间的差异？

Question

在frama-C中,当我加载源文件时,它会进行预处理,并执行自动纠错,如"自动类型转换",如下所示(int被类型化为浮动).

现在,我如何才能看到预处理后所做的所有更改.

是否有任何方法或日志文件或警告消息显示frama-c所做的所有更改.这是我的源代码:

int main() {
int a, b;

printf("Input two integers to divide\n");
scanf("%d%d", &a, &b);
printf("%d/%d = %.2f\n", a, b, a/(float)b);

}

这是我的frama-C预处理代码:

extern int (/* missing proto */ printf)();
extern int (/* missing proto */ scanf)();
int main(void) {
int a;
int b;
int __retres;
printf("Input two integers to divide\n");
scanf("%d%d", &a, &b);
printf("%d/%d = %.2f\n", a, b, (float)a/(float)b);
__retres =0;
return (__retres);
}

Answer 1

Frama-C的API提出了一定数量的钩子,这些钩子将针对不同的规范化情况触发.请注意,它不执行"自动纠错".完成的转换不会改变程序的语义.

这些钩子位于cil/src/frontc/cabs2cil.mli例如,你找到:

val typeForInsertedCast:
  (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ) ref

typeForInsertedCast e t1 t2当e类型的表达式t1必须被隐式转换为类型时调用t2(在C标准的6.3节中关于隐式转换的条件中).通过插件在此处提供您自己的功能,您可以跟踪程序中发生的所有隐式转换.

用户手册中提供了编写Frama-C插件的教程(需要OCaml知识).