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

[Frama-c-discuss] [Value analysis] Validating a function with behavior spec.



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.