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: Mon, 22 Jul 2019 16:41:48 +0100
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>