--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with frama-c to Coq inductive type definition



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.
Regards
Dragan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190721/60f2483b/attachment.html>