Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] [Value analysis] Validating a function with behavior spec.
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Fri, 13 Apr 2012 11:27:57 +0200
  • In-reply-to: <CAOH62JgyUC8+2cHf-bsPmVnWcL+JxyV88mnVo9gHc0j5Ym=JqQ@mail.gmail.com>
  • References: <CAFaEDLCHYJtescjnsqs6gE5q_Nx5+CWSg_3AD=f9pN_AHhq4=w@mail.gmail.com> <CAOH62JgyUC8+2cHf-bsPmVnWcL+JxyV88mnVo9gHc0j5Ym=JqQ@mail.gmail.com>
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.