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

[Frama-c-discuss] Queries regarding WP plugin



Hello,

Le 15/12/2014 05:17, Debasmita Lohar a ?crit :
> The exact commands and outputs are as follows:
> 1. frama-c -wp-print test.c. Output: [kernel] preprocessing with "gcc -C
> -E -I.  test.c"
> 2. frama-c -wp-out wptest test.c. Output: same. wptest is a directory
> and after the execution of this command it contains nothing.
> 3. frama-c -wp-gen test.c. Output: again same.
> 4. frama-c -wp test.c.
> output: [kernel] preprocessing with "gcc -C -E -I.  test.c"
> [wp] Running WP plugin...
> [wp] Collecting axiomatic usage
> [wp] warning: Missing RTE guards
> [wp] 1 goal scheduled
> [wp] [Qed] Goal typed_main_assert_P : Valid

OK, you have several issues:

  1. You should use *simultaneously* -wp (to generate and prove proof 
obligations) and -wp-out <dir> (to keep them in the given <dir> 
directory) options;

  2. Your program is too simple and the generated proof obligation is 
prove by Qed (line "[Qed] Goal typed_main_assert_P : Valid"), the 
internal prover of WP, and not Alt-Ergo (thus no file are generated). 
You should use -wp-qed-checks but it seems to be broken in WP 0.8 
(generation of truncated Alt-Ergo files).

For 2., another option is to use more complicated proof obligations. For 
example, on the attached simple_wp.c file, verification condition of 
f_complicated() is generated (and not for f()).

I used following command line:
   frama-c -wp-out simple_wp_out -wp simple_wp.c

Best regards,
david

-------------- next part --------------

/*@ requires 0 <= x <= 10;
    ensures 1 <= \result <= 11;
*/
int f(int x)
{
  return x + 1;
}


/*@ requires 0 <= x <= 10;
    ensures 0 <= \result <= 33;
*/
int f_complicated(int x)
{
  return x * 1;
}