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>
- Follow-Ups:
- [Frama-c-discuss] problem with frama-c to Coq inductive type definition
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] problem with frama-c to Coq inductive type definition
- Prev by Date: [Frama-c-discuss] Warnings for call to memcpy()... why?
- Next by Date: [Frama-c-discuss] Why does a string literal not satisfy valid_read_string?
- Previous by thread: [Frama-c-discuss] Frama-C on Windows 10 via WSL
- Next by thread: [Frama-c-discuss] problem with frama-c to Coq inductive type definition
- Index(es):