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

  • Subject: [Frama-c-discuss] problem with frama-c to Coq inductive type definition
  • From: dragan.stosic at gmail.com (Dragan)
  • Date: Sun, 21 Jul 2019 10:20:50 +0100
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>