--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Error on using pp-annot



I have tried clang and it seems to work. I also could reduce the
number of options of the command. This is my command now:

> frama-c -cpp-command 'clang -C -E -I.' -wp -wp-rte -pp-annot constant.c

And the result:

[kernel] preprocessing with "clang -C -E -I.  -dD constant.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function double_it
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_double_it_assert_rte_signed_overflow_2 : Valid (37ms) (3)
[wp] [Alt-Ergo] Goal typed_double_it_assert_rte_signed_overflow : Valid (Qed:3ms) (40ms) (3)
[wp] [Alt-Ergo] Goal typed_double_it_post : Valid (Qed:3ms) (40ms) (3)

All three goals as expected.

So thanks again for your assistance.
Frank