--- layout: fc_discuss_archives title: Message 24 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 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>