The following commit has been merged in the master branch:
commit 31d1c6cd273ed00e47f3545a19436769f9702ce5
Author: Mehdi Dogguy
Date: Thu Dec 8 16:41:23 2011 +0100
Update patches
diff --git a/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
b/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
index c662fe6..d134d8d 100644
--- a/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
+++ b/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
@@ -7,10 +7,10 @@ Subject: Why 2.29 do support Coq 8.3
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index edaf366..8856081 100644
+index e298bcf..a2068e5 100644
--- a/tools/dpConfig.ml
+++ b/tools/dpConfig.ml
-@@ -199,7 +199,7 @@ let coq =
+@@ -221,7 +221,7 @@ let coq =
version = "";
version_switch = "-v";
version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)";
diff --git a/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
b/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
index d3f4192..a2b00b0 100644
--- a/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
+++ b/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
@@ -1,22 +1,22 @@
-From: Mehdi Dogguy
-Date: Sat, 23 Apr 2011 20:07:20 +0200
-Subject: Mark alt-ergo 0.93 as compatible
+From: Mehdi Dogguy
+Date: Thu, 8 Dec 2011 16:42:30 +0100
+Subject: Mark alt-ergo > 0.93 as compatible
---
tools/dpConfig.ml |2 +-
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index 8856081..fe72bf9 100644
+index a2068e5..8266412 100644
--- a/tools/dpConfig.ml
+++ b/tools/dpConfig.ml
@@ -84,7 +84,7 @@ let alt_ergo =
version = "";
version_switch = "-version";
version_regexp = ".*Ergo \\([^ ]*\\)";
--versions_ok = ["0.91"; "0.92.1"; "0.92.2"];
-+versions_ok = ["0.91"; "0.92.1"; "0.92.2"; "0.93"];
- versions_old = ["0.8"; "0.9"];
+-versions_ok = ["0.93"];
++versions_ok = ["0.93"; "0.93.1"; "0.94"];
+ versions_old = ["0.8"; "0.9" ; "0.91"; "0.92.1"; "0.92.2" ];
command = "alt-ergo";
command_switches = "";
--
diff --git
a/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
b/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
index 2b22c73..54177f4 100644
---
a/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
+++
b/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
@@ -7,7 +7,7 @@ Subject: Fix non-exhaustive pattern-matching in
jc_annot_inference.ml
1 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/jc/jc_annot_inference.ml b/jc/jc_annot_inference.ml
-index e7a1eae..d62a53c 100644
+index f4c9791..d9dbbd7 100644
--- a/jc/jc_annot_inference.ml
+++ b/jc/jc_annot_inference.ml
@@ -148,7 +148,7 @@ let rec destruct_pointer t =
diff --git a/debian/patches/0004-Default-to-why2-for-jessie-atp.patch
b/debian/patches/0004-Default-to-why2-for-jessie-atp.patch
new file mode 100644
index 000..31da14c
--- /dev/null
+++ b/debian/patches/0004-Default-to-why2-for-jessie-atp.patch
@@ -0,0 +1,22 @@
+From: Mehdi Dogguy
+Date: Thu, 8 Dec 2011 16:46:48 +0100
+Subject: Default to why2 for -jessie-atp
+
+---
+ frama-c-plugin/jessie_options.ml |2 +-
+ 1 files changed, 1 insertions(+), 1 deletions(-)
+
+diff --git a/frama-c-plugin/jessie_options.ml
b/frama-c-plugin/jessie_options.ml
+index 8e57656..8da0b66 100644
+--- a/frama-c-plugin/jessie_options.ml
b/frama-c-plugin/jessie_options.ml
+@@ -175,7 +175,7 @@ module Atp =
+ (struct
+let option_name = "-jessie-atp"
+let module_name = "-jessie-atp"
+- let default = "why3ml"
++ let default = "why2"
+let arg_name = ""
+let help = "use given automated theorem prover, among `alt-ergo',
`cvc3', `simplify', `vampire', `yices' and `z3'. Use `goals' to simply generate
goals in Why syntax."
+let kind = `Tuning
+--
diff --git a/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
b/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
new file mode 100644
index 000..cdb459b
--- /dev/null
+++ b/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
@@ -0,0 +1,22 @@
+From: Mehdi Dogguy
+Date: Thu, 8 Dec 2011 17:08:36 +0100
+Subject: Fix Jc_annot_inference (use old_reg_pos)
+
+---
+ jc/jc_annot_inference.ml |2 +-
+ 1 files changed, 1 insertions(+), 1 deletions(-)
+
+diff --git a/jc/jc_annot_inference.ml b/jc/jc_annot_inference.ml
+index d9dbbd7..08e66e4 100644
+--- a/jc/jc_annot_inference.ml
b/jc/jc_annot_inference.ml
+@@ -491,7 +491,7 @@ let reg_annot ?id ?kind ?name ~pos ~anchor a =
+ in
+ Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
+ let formula = Format.flush_str_formatter () in
+- let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
++ let lab = Output.old_reg_pos "G" ?id ?kind
