--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on February 2012 ---
Hello, On 02/09/2012 10:20 AM, Boris Hollas wrote: > I see my debug message "Expression processed" 4 times when I run it on > > int foo(int k) { > return 1/k; > } > > How many expression does this code contain? It should have only one > expression (1/k), but the translated code > > int foo(int k) > { > int __retres; > __retres = 1 / k; > return (__retres); > } > > has a new lvalue, so there are 2 expressions in total. No there are 4 expressions in this program: 1, k, 1/k and _retres. You can see each of them by replacing in your code the line print_string "Expression processed" by Nonzero.feedback "Expression %a processed" Cil.d_exp e; Does Frama-c run > on this code? Yes it is. Frama-C analyzers only handle this normalized code (except if you use the so-called cabs-AST/visitor instead of the standard AST/visitor). Is each expression traversed twice? No, it isn't. Hope this helps, Julien