From 5298e1888ff8b1594ff7db28abe7ec67a334c9fe Mon Sep 17 00:00:00 2001
From: Jerry James <jamesjer@betterlinux.com>
Date: Sep 08 2014 17:17:08 +0000
Subject: Merge branch 'f21'


---

diff --git a/frama-c-why3.patch b/frama-c-why3.patch
new file mode 100644
index 0000000..a02f88d
--- /dev/null
+++ b/frama-c-why3.patch
@@ -0,0 +1,131 @@
+--- ./src/wp/share/why3/Memory.v.orig	2014-03-12 09:07:51.000000000 -0600
++++ ./src/wp/share/why3/Memory.v	2014-09-06 21:30:00.000000000 -0600
+@@ -137,29 +137,29 @@ Definition separated (p:addr) (a:Z) (q:a
+   (((offset p) + a)%Z <= (offset q))%Z))).
+ 
+ (* Why3 assumption *)
+-Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map
+-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT))
+-  (p:addr) (a1:Z): Prop := forall (q:addr), (included q 1%Z p a1) ->
++Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(map.Map.map addr a))
++  (m2:(map.Map.map addr a)) (p:addr) (a1:Z): Prop :=
++  forall (q:addr), (included q 1%Z p a1) ->
+   ((map.Map.get m1 q) = (map.Map.get m2 q)).
+ 
+ (* Why3 assumption *)
+-Definition havoc {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map
+-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT))
+-  (p:addr) (a1:Z): Prop := forall (q:addr), (separated q 1%Z p a1) ->
++Definition havoc {a:Type} {a_WT:WhyType a} (m1:(map.Map.map addr a))
++  (m2:(map.Map.map addr a)) (p:addr) (a1:Z): Prop :=
++  forall (q:addr), (separated q 1%Z p a1) ->
+   ((map.Map.get m1 q) = (map.Map.get m2 q)).
+ 
+ (* Why3 assumption *)
+-Definition valid_rd (m:(@map.Map.map Z _ Z _)) (p:addr) (n:Z): Prop :=
++Definition valid_rd (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
+   (0%Z < n)%Z -> ((0%Z <= (offset p))%Z /\
+   (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z).
+ 
+ (* Why3 assumption *)
+-Definition valid_rw (m:(@map.Map.map Z _ Z _)) (p:addr) (n:Z): Prop :=
++Definition valid_rw (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
+   (0%Z < n)%Z -> ((0%Z < (base p))%Z /\ ((0%Z <= (offset p))%Z /\
+   (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z)).
+ 
+ (* Why3 goal *)
+-Lemma valid_rw_rd : forall (m:(@map.Map.map Z _ Z _)), forall (p:addr),
++Lemma valid_rw_rd : forall (m:(map.Map.map Z Z)), forall (p:addr),
+   forall (n:Z), (valid_rw m p n) -> (valid_rd m p n).
+ intros m p n.
+ unfold valid_rw. unfold valid_rd.
+@@ -167,7 +167,7 @@ intuition (auto with zarith).
+ Qed.
+ 
+ (* Why3 goal *)
+-Lemma valid_string : forall (m:(@map.Map.map Z _ Z _)), forall (p:addr),
++Lemma valid_string : forall (m:(map.Map.map Z Z)), forall (p:addr),
+   ((base p) < 0%Z)%Z -> (((0%Z <= (offset p))%Z /\
+   ((offset p) < (map.Map.get m (base p)))%Z) -> ((valid_rd m p 1%Z) /\
+   ~ (valid_rw m p 1%Z))).
+@@ -227,17 +227,17 @@ Definition region: Z -> Z.
+ Admitted.
+ 
+ (* Why3 goal *)
+-Definition linked: (@map.Map.map Z _ Z _) -> Prop.
++Definition linked: (map.Map.map Z Z) -> Prop.
+ Admitted.
+ 
+ (* Why3 goal *)
+-Definition sconst: (@map.Map.map addr addr_WhyType Z _) -> Prop.
++Definition sconst: (map.Map.map addr Z) -> Prop.
+ Admitted.
+ 
+ (* Why3 assumption *)
+-Definition framed (m:(@map.Map.map addr addr_WhyType
+-  addr addr_WhyType)): Prop := forall (p:addr), ((region (base (map.Map.get m
+-  p))) <= 0%Z)%Z.
++Definition framed (m:(map.Map.map addr addr)): Prop :=
++  forall (p:addr), ((region (base (map.Map.get m p (a_WT := addr_WhyType)
++  (b_WT := addr_WhyType)))) <= 0%Z)%Z.
+ 
+ (* Why3 goal *)
+ Lemma separated_included : forall (p:addr) (q:addr), forall (a:Z) (b:Z),
+@@ -283,22 +283,22 @@ Qed.
+ 
+ (* Why3 goal *)
+ Lemma eqmem_included : forall {a:Type} {a_WT:WhyType a},
+-  forall (m1:(@map.Map.map addr addr_WhyType a a_WT)) (m2:(@map.Map.map
+-  addr addr_WhyType a a_WT)), forall (p:addr) (q:addr), forall (a1:Z) (b:Z),
++  forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
++  forall (p:addr) (q:addr), forall (a1:Z) (b:Z),
+   (included p a1 q b) -> ((eqmem m1 m2 q b) -> (eqmem m1 m2 p a1)).
+ intros a a_WT m1 m2 p q a1 b h1 h2.
+ Admitted.
+ 
+ (* Why3 goal *)
+-Lemma eqmem_sym : forall {a:Type} {a_WT:WhyType a}, forall (m1:(@map.Map.map
+-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT)),
++Lemma eqmem_sym : forall {a:Type} {a_WT:WhyType a},
++  forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
+   forall (p:addr), forall (a1:Z), (eqmem m1 m2 p a1) -> (eqmem m2 m1 p a1).
+  intros A m1 m2 p a. unfold eqmem.
+ Admitted.
+ 
+ (* Why3 goal *)
+-Lemma havoc_sym : forall {a:Type} {a_WT:WhyType a}, forall (m1:(@map.Map.map
+-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT)),
++Lemma havoc_sym : forall {a:Type} {a_WT:WhyType a},
++  forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
+   forall (p:addr), forall (a1:Z), (havoc m1 m2 p a1) -> (havoc m2 m1 p a1).
+ Admitted.
+ 
+--- ./src/wp/share/why3/Qedlib.v.orig	2014-03-12 09:07:51.000000000 -0600
++++ ./src/wp/share/why3/Qedlib.v	2014-09-06 21:00:00.000000000 -0600
+@@ -187,13 +187,14 @@ Definition real_hex := real_base 2%R.
+ 
+ Record farray (A B : Type) := { whytype1 : BuiltIn.WhyType A ;
+                                whytype2 : BuiltIn.WhyType B ;
+-                               access :> @Map.map A whytype1 B whytype2 }.
++                               access :> Map.map A B }.
+ Definition array (A : Type) := farray Z A.
+ Hypothesis extensionality: forall (A B : Type) (f g : A -> B),
+   (forall x, f x = g x) -> f = g.
+ 
+ Definition select {A B : Type}
+-  (m : farray A B) (k : A) : B := Map.get m k.
++  (m : farray A B) (k : A) : B := Map.get m k
++  (a_WT := whytype1 m) (b_WT := whytype2 m).
+ 
+ Lemma farray_eq : forall A B (m1 m2 : farray A B),
+    whytype1 m1 = whytype1 m2 -> whytype2 m1 = whytype2 m2 ->
+@@ -210,7 +211,8 @@ Qed.
+ 
+ Definition update {A B : Type}
+   (m : farray A B) (k : A) (v : B) : (farray A B) :=
+-  {| whytype1 := whytype1 m; whytype2 := whytype2 m; access := Map.set m k v|}.
++  {| whytype1 := whytype1 m; whytype2 := whytype2 m;
++     access := Map.set m k v (a_WT := whytype1 m) (b_WT := whytype2 m) |}.
+ 
+ Notation " a .[ k ] " := (select a k) (at level 60).
+ Notation " a .[ k <- v ] " := (update a k v) (at level 60).
diff --git a/frama-c.spec b/frama-c.spec
index ec90eb4..60b4853 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -16,7 +16,7 @@
 
 Name:           frama-c
 Version:        1.10
-Release:        15%{?dist}
+Release:        16%{?dist}
 Summary:        Framework for source code analysis of C software
 
 # Licensing breakdown in source file frama-c-1.6-licensing
@@ -40,6 +40,8 @@ Source13:       http://frama-c.com/download/wp-manual-%{pkgversion}.pdf
 Source14:       %{name}-icons.tar.xz
 # Adapt to ocamlgraph 1.8.5
 Patch0:         %{name}-ocamlgraph.patch
+# Adapt to why3 0.84
+Patch1:         %{name}-why3.patch
 
 BuildRequires:  alt-ergo
 BuildRequires:  coq
@@ -141,6 +143,7 @@ support.
 %setup -q -T -D -a 1 -n %{name}-%{pkgversion}
 %setup -q -T -D -a 14 -n %{name}-%{pkgversion}
 %patch0
+%patch1
 
 # Copy in the manuals
 mkdir doc/manuals
@@ -162,8 +165,8 @@ sed -ri 's/^CP[[:blank:]]+=.*/& -p/' share/Makefile.common
 # Remove spurious executable bits
 find -O3 . -perm /0111 \( -name \*.ml -o -name \*.mli \) | xargs chmod 0644
 
-# Adapt to why3 0.83
-sed -i 's/0\.82/0.83/g' configure src/wp/configure
+# Adapt to why3 0.84
+sed -i 's/0\.82/0.84/g' configure src/wp/configure
 
 %build
 # This option prints the actual make commands so we can see what's
@@ -280,6 +283,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
 %{_xemacs_sitelispdir}/acsl.el
 
 %changelog
+* Thu Sep  4 2014 Jerry James <loganjerry@gmail.com> - 1.10-16
+- Adapt to why3 0.84
+
 * Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 1.10-15
 - Rebuild for final ocaml 4.02.0 release
 - Fix license handling