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] problem with frama-c to Coq inductive type definition

Hello,

Le dim. 21 juil. 2019 à 11:21, Dragan <dragan.stosic at gmail.com> a écrit :

> Hi frama-c team,
> I have tried to prove lemma by the Coq theorem prover exporting ACSL model
> and I have noticed the following error :
> /*@ axiomatic example {
>    @type model_foo_bar = foo | bar;
>    @ }
>    @*/
> Inductive A_model_foo_bar : Type :=
> | C_foo :  A_model_foo_bar.
> | C_bar :  A_model_foo_bar..
>
> Notice (dots) in the inductive A_model_foo_bar definition. It should be
> (dot) at the end of inductive type.
>
>
Which version of Frama-C are you using, and what options are using to
produce the Coq fragment you're showing us? As far as I can tell, with 19.0
Potassium and the following example:

/*@ axiomatic example {
   @ type model_foo_bar = foo | bar;
   @ }
   @*/

/*@ lemma test: \forall model_foo_bar f; f == foo || f == bar; */

using frama-c -wp -wp-prover-coq file.c -wp-out wp-test
generates Coq files that simply do not contain a definition of
model_foo_bar. This solves the presence of two dots instead of one, but not
the fact that the result is ill-formed.

In any case, this looks like a bug in WP that ought to be reported. That
said, please bear in mind that support for sum types, both by WP and
Frama-C's kernel itself, is quite rudimentary as of now, and that it might
not be easy to write large annotations that heavily rely on those and are
accepted by the tool.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190722/c3ef0cfc/attachment.html>