static analysis - How to track differences between the C source and Frama-C's preprocessed code? -

in frama-c when load source file pre processing , automatic error correction "automatic typecast " shown below (int typecasted float).

now how can see changes made after preprocessing.

is there method or log file or warning message shows changes made frama-c.! source code:

int main() { int a, b;  printf("input 2 integers divide\n"); scanf("%d%d", &a, &b); printf("%d/%d = %.2f\n", a, b, a/(float)b);  } 

this frama-c preprocessed code:

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

frama-c's api proposes number of hooks triggered difference cases of normalization. note not perform "automatic error correction". transformations done not alter semantics of program.

these hooks located in cil/src/frontc/cabs2cil.mli instance, find there:

val typeforinsertedcast:   (cil_types.exp -> cil_types.typ -> cil_types.typ -> cil_types.typ) ref 

typeforinsertedcast e t1 t2 called when expression e of type t1 must implicitely converted type t2 (in conditions described section 6.3 of c standard implicit conversions). providing own function here via plugin, can track implicit conversions happen in program.

a tutorial on writing frama-c plugins available in user manual (requires ocaml knowledge).