--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Executing a visitor



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