Coq proofs under Frama-C 19.0 beta

[jensgerlach]

No description provided.

[jensgerlach]

Frama-C 19 requires some changes in our Coq proofs.
A typical example is the following line

replace (1 + i - 1) with i by lia.

where Coq now (in contrast to Frama-C 18) complains

The term "i" has type "int" while it is expected to have type "nat".

I fix this issue by changing the above line to

replace (1 + i - 1)%Z with i by lia.

I have two questions:

1. Which changes in Frama-C/WP causes these error messages by Coq?
2. Is there another (maybe smarter way) to fix this issue that does not require adding %Z to quite a lot of lines?

Note that I am using the same version 8.7.2 of Coq that we had been using with Frama-C 18.0.

[vprevosto]

I confirm that I had the same problem (thanks for the workaround by the way 😛) with one of my Coq proofs.

[jensgerlach]

I am glad I could help!-)
Maybe someone from the WP-team could shed some light on this new behavior.

[bobot]

You could open the int scope at the start of the proof. Perhaps we added or removed a scope opening in Coq generation in the last version. Does one of you have a simple example?

[jensgerlach]

I am not sure the following example helps but it shows some differences in the generated coq code.
It starts with processing the following wrong ACSL lemma

/*@
  lemma Foo: \forall integer i; i > 0;
*/

When processing it with frama-c-gui -wp -wp-prover coq foo.c and opening the Coq-IDE the
I see the following code under Frama-C 18.0

(* ---------------------------------------------------------- *)
(* --- Lemma 'Foo'                                        --- *)
(* ---------------------------------------------------------- *)
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   --- *)

Goal forall (i : Z), (0 < i)%Z.

Proof.
(* auto with zarith. *)
Qed.

With Frama-C 19 beta the code contains more Requires clauses and looks like this

(* ---------------------------------------------------------- *)
(* --- Lemma 'Foo'                                        --- *)
(* ---------------------------------------------------------- *)
Require Import ZArith.
Require Import Reals.
Require Import BuiltIn.
Require Import HighOrd.
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 bool.Bool.
Require Import Qedlib.
Require Import Qed.

(* --- Global Definitions   --- *)

Goal forall (i : Z), (0 < i)%Z.

Proof.
(* auto with zarith. *)
Qed.