--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on March 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP 0.9 (for Magnesium) Compatible with Coq 8.5?



Hello,

WP 0.9 (for Magnesium-20151002) is compatible with
 > coqc -v
The Coq Proof Assistant, version 8.4pl5 (March 2016)

 > why3 --version
Why3 platform, version 0.85

 > alt-ergo -version
0.99.1

 > frama-c -wp-help
Plug-in name: WP
Plug-in shortname: wp
Description: Weakest Precondition Calculus
WP 0.9 for Magnesium-20151002
...

 > frama-c -wp -wp-prover coq lemma_ptr_inc.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no 
preprocessing)
[kernel] Parsing lemma_ptr_inc.c (with preprocessing)
[wp] 1 goal scheduled
[wp] [Coq] Compiling 'Compound.v'.
[wp] [Coq] Goal typed_lemma_ptr_inc : Unknown
[wp] Proved goals:    0 / 1
      Coq:             0  (unknown: 1)

-- Patrick.

Le 08/03/2016 19:19, Pablo M. S. Farias a écrit :
> Just to say that the compatibility between WP 0.9 and Coq 8.5 is not 
> urgent for me anymore: I created a fresh opam environment with Coq 
> 8.4pl6 + Why3 + Frama-C. (I still cannot verify the lemma, though.)
>
> ---
> Pablo
> http://lia.ufc.br/~pmsf/
>
> Em 2016-03-08 13:22, Pablo M. S. Farias escreveu:
>> Hello, all!
>>
>> As reported in the previous e-mail, I'm having trouble verifying this
>> in WP (also attached):
>>
>>   /*@ lemma ptr_inc:  \forall int n, *v, *p;
>>         n >= 0 ==> \valid_read(v + (0..n-1)) ==> v <= p < v+n ==>
>>         v <= p+1;
>>    */
>>
>> I would like to use Coq to try out a proof, but running
>>
>>   frama-c-gui -wp -wp-prover coqide lemma_ptr_inc.c
>>
>> gives this output:
>>
>>   [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i
>> (no preprocessing)
>>   [kernel] Parsing lemma_ptr_inc.c (with preprocessing)
>>   [wp] Running WP plugin...
>>   [wp] Collecting axiomatic usage
>>   [wp] 1 goal scheduled
>>   [wp] [Coq] Compiling 'BuiltIn.v'.
>>   [wp] [Coq] 'BuiltIn.v' compilation failed.
>>   Don't know what to do with -as bool -as int -as real -as map
>>   See -help for the list of supported options
>>   [wp] [Coq] Goal typed_lemma_ptr_inc : Failed
>>        Error: Compilation of 'BuiltIn.v' failed.
>>   [wp] Proved goals:    0 / 1
>>        Coq:             0  (failed: 1)
>>
>> Is WP 0.9 (for Magnesium-20151002) compatible with Coq 8.5 (which I'm
>> using)? Am I doing something wrong?
>>
>> Thanks in advance,
>>
>> -- 
>> Pablo
>> http://lia.ufc.br/~pmsf/
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss