--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on July 2019 ---
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>