Add 0001-Update-for-why-2.19.patch

2 files changed, 92 insertions, 0 deletions

diff --git a/debian/patches/0001-Update-for-why-2.19.patch b/debian/patches/0001-Update-for-why-2.19.patch
new file mode 100644
index 00000000..fc6ab68f
--- /dev/null
+++ b/debian/patches/0001-Update-for-why-2.19.patch
@@ -0,0 +1,91 @@
+From: Stephane Glondu <steph@glondu.net>
+Date: Sat, 29 Aug 2009 16:35:56 +0200
+Subject: [PATCH] Update for why 2.19
+
+Patch taken from upstream SVN.
+
+Signed-off-by: Stephane Glondu <steph@glondu.net>
+---
+ contrib/dp/dp.ml |   18 +++++++++---------
+ 1 files changed, 9 insertions(+), 9 deletions(-)
+
+diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
+index 79ffaf3..d880384 100644
+--- a/contrib/dp/dp.ml
++++ b/contrib/dp/dp.ml
+@@ -701,7 +701,7 @@ let file_contents f =
+ let timeout_sys_command cmd =
+   if !debug then Format.eprintf "command line: %s@." cmd;
+   let out = Filename.temp_file "out" "" in
+-  let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
++  let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
+   let ret = Sys.command cmd in
+   if !debug then 
+     Format.eprintf "Output file %s:@.%s@." out (file_contents out);
+@@ -731,12 +731,12 @@ let why_files f = String.concat " " (!prelude_files @ [f])
+ 
+ let call_simplify fwhy =
+   let cmd = 
+-    sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy) 
++    sprintf "why --simplify %s" (why_files fwhy)
+   in
+   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+   let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
+   let cmd = 
+-    sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out" 
++    sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
+       !timeout fsx
+   in
+   let out = Sys.command cmd in
+@@ -747,7 +747,7 @@ let call_simplify fwhy =
+   r
+ 
+ let call_ergo fwhy =
+-  let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
++  let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
+   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+   let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
+   let ftrace = Filename.temp_file "ergo_trace" "" in
+@@ -797,12 +797,12 @@ let call_zenon fwhy =
+ 
+ let call_yices fwhy =
+   let cmd = 
+-    sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
++    sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
+   in
+   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+   let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
+   let cmd = 
+-    sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out" 
++    sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
+       !timeout fsmt
+   in
+   let out = Sys.command cmd in
+@@ -814,7 +814,7 @@ let call_yices fwhy =
+ 
+ let call_cvcl fwhy =
+   let cmd = 
+-    sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
++    sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
+   in
+   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+   let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
+@@ -831,7 +831,7 @@ let call_cvcl fwhy =
+ 
+ let call_harvey fwhy =
+   let cmd = 
+-    sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
++    sprintf "why --harvey --encoding strat %s" (why_files fwhy)
+   in
+   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+   let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
+@@ -856,7 +856,7 @@ let call_harvey fwhy =
+   r
+ 
+ let call_gwhy fwhy =
+-  let cmd = sprintf "gwhy --no-arrays  %s" (why_files fwhy) in
++  let cmd = sprintf "gwhy %s" (why_files fwhy) in
+   if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
+   NoAnswer
+ 
+-- 
diff --git a/debian/patches/series b/debian/patches/series
new file mode 100644
index 00000000..1693a782
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1 @@
+0001-Update-for-why-2.19.patch