--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2014 ---
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