--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on July 2019 ---
Hi Virgile, I am working on frama-c 18.0 Argon version. file.acsl /*@ axiomatic example { @ type model_foo_bar = foo | bar; @ } @*/ /*@ lemma test: \forall model_foo_bar f; f == foo || f == bar; */ file.c #include "file.acsl" I have tested your example keeping lemma outside of the axiomatic block command: frama-c -wp -wp-prover coq file.c -wp-out wp-test scenario 1: I am getting the following : (* ---------------------------------------------------------- *) (* --- Lemma 'test' --- *) (* ---------------------------------------------------------- *) Require Import ZArith. Require Import Reals. Require Import BuiltIn. Require Import int.Int. Require Import int.Abs. Require Import int.ComputerDivision. Require Import real.Real. Require Import real.RealInfix. Require Import real.FromInt. Require Import map.Map. Require Import Qedlib. Require Import Qed. (* --- Global Definitions (continued #1) --- *) Require Import A_example. Goal forall (m : A_model_foo_bar), ((C_bar) = m) \/ ((C_foo) = m). Proof. auto with zarith. Qed. So the model_foo_bar exist in the goal definition. scenario 2 : lemma is inside of the axiomatic block : (* ---------------------------------------------------------- *) (* --- Lemma 'test' --- *) (* ---------------------------------------------------------- *) Require Import ZArith. Require Import Reals. Require Import BuiltIn. Require Import int.Int. Require Import int.Abs. Require Import int.ComputerDivision. Require Import real.Real. Require Import real.RealInfix. Require Import real.FromInt. Require Import map.Map. Require Import Qedlib. Require Import Qed. (* --- Axiomatic 'example' --- *) Inductive A_model_foo_bar : Type := | C_foo : A_model_foo_bar. | C_bar : A_model_foo_bar.. Goal forall (m : A_model_foo_bar), ((C_bar) = m) \/ ((C_foo) = m). Proof. auto with zarith. Qed. scenario 3: theorem prover is alt-Ergo , and lemma is outside, I am getting the following (* ---------------------------------------------------------- *) (* --- Lemma 'test' --- *) (* ---------------------------------------------------------- *) (* --- Global Definitions (continued #1) --- *) goal lemma_test: forall m : A_model_foo_bar. (C_bar = m) or (C_foo = m) Again, I can see A_model_foo_bar and proof failed with unknown type. So there must be a some issue with WP. Regards Dragan Stosic -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190722/266e18fe/attachment-0001.html>