--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on April 2012 ---
As mentionned Pascal, this is awork for Wp. frama-c -wp -wp-rte abs8b.i [wp] Running WP plugin... [rte] annotating function abs8 [wp] [Alt-Ergo] Goal store_abs8_assert_rte : Valid [wp] [Alt-Ergo] Goal store_abs8_assert_3 : Valid [wp] [Alt-Ergo] Goal store_abs8_assert_2 : Valid [wp] [Alt-Ergo] Goal store_abs8_assert : Valid [wp] [Alt-Ergo] Goal store_abs8_positive_or_zero_post : Valid [wp] [Alt-Ergo] Goal store_abs8_negative_post : Valid [wp] [Alt-Ergo] Goal store_abs8_disjoint_negative_positive_or_zero : Valid [wp] [Alt-Ergo] Goal store_abs8_complete_negative_positive_or_zero : Valid Provided file 'abs8b.i' contains your function 'abs8' and the following typedefs : typedef signed char int8 ; typedef unsigned char uint8 ; You should notice the option -wp-rte to generate (and prove) necessary guards against arithmetic overflows. L.