--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Mon Nov 15 14:59:53 2010 +0100
@@ -6,6 +6,7 @@
theory Boogie_Dijkstra
imports Boogie
+uses ("Boogie_Dijkstra.b2i")
begin
text {*
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Mon Nov 15 14:59:53 2010 +0100
@@ -6,6 +6,7 @@
theory Boogie_Max
imports Boogie
+uses ("Boogie_Max.b2i")
begin
text {*
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Mon Nov 15 14:59:53 2010 +0100
@@ -6,6 +6,7 @@
theory Boogie_Max_Stepwise
imports Boogie
+uses ("Boogie_Max.b2i")
begin
text {*
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Mon Nov 15 14:59:53 2010 +0100
@@ -6,6 +6,7 @@
theory VCC_Max
imports Boogie
+uses ("VCC_Max.b2i")
begin
text {*
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 15 14:59:53 2010 +0100
@@ -19,16 +19,16 @@
val ext = "b2i"
fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
val base_path = add_ext (Path.explode base_name)
- val path_id = Thy_Load.check_file [Thy_Load.master_directory thy] base_path
+ val (full_path, _) =
+ Thy_Load.check_file [Thy_Load.master_directory thy] base_path
val _ = Boogie_VCs.is_closed thy orelse
error ("Found the beginning of a new Boogie environment, " ^
"but another Boogie environment is still open.")
in
thy
- |> Thy_Load.require base_path
- |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id)
- |> Thy_Load.provide (base_path, path_id)
+ |> Boogie_Loader.load_b2i (not quiet) offsets full_path
+ |> Thy_Load.provide_file base_path
end
--- a/src/HOL/Library/Quotient_Option.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Mon Nov 15 14:59:53 2010 +0100
@@ -9,7 +9,7 @@
begin
fun
- option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
+ option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
where
"option_rel R None None = True"
| "option_rel R (Some x) None = False"
--- a/src/HOL/Library/Quotient_Product.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Mon Nov 15 14:59:53 2010 +0100
@@ -9,7 +9,7 @@
begin
definition
- prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+ prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
--- a/src/HOL/Library/Quotient_Sum.thy Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Mon Nov 15 14:59:53 2010 +0100
@@ -9,7 +9,7 @@
begin
fun
- sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+ sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
where
"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
--- a/src/HOL/Tools/SMT/smt_failure.ML Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_failure.ML Mon Nov 15 14:59:53 2010 +0100
@@ -10,6 +10,7 @@
Counterexample of bool * term list |
Time_Out |
Out_Of_Memory |
+ Solver_Crashed of int |
Other_Failure of string
val string_of_failure: Proof.context -> failure -> string
exception SMT of failure
@@ -22,6 +23,7 @@
Counterexample of bool * term list |
Time_Out |
Out_Of_Memory |
+ Solver_Crashed of int |
Other_Failure of string
fun string_of_failure ctxt (Counterexample (real, ex)) =
@@ -36,6 +38,8 @@
end
| string_of_failure _ Time_Out = "Timed out"
| string_of_failure _ Out_Of_Memory = "Ran out of memory"
+ | string_of_failure _ (Solver_Crashed err) =
+ "Solver crashed with error code " ^ string_of_int err
| string_of_failure _ (Other_Failure msg) = msg
exception SMT of failure
--- a/src/HOL/Tools/SMT/smt_solver.ML Sun Nov 14 17:33:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 15 14:59:53 2010 +0100
@@ -106,24 +106,25 @@
map File.shell_quote (solver @ args) @
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
+fun check_return_code {output, redirected_output, return_code} =
+ if return_code <> 0 then
+ raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
+ else (redirected_output, output)
+
fun run ctxt cmd args input =
(case C.certificates_of ctxt of
- NONE =>
- let
- val {output, redirected_output, ...} =
- Cache_IO.run (make_cmd (choose cmd) args) input
- in (redirected_output, output) end
+ NONE => Cache_IO.run (make_cmd (choose cmd) args) input
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
- if Config.get ctxt C.fixed
- then error ("Bad certificates cache: missing certificate")
- else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
- input
+ if Config.get ctxt C.fixed then
+ error ("Bad certificates cache: missing certificate")
+ else
+ Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
| (SOME output, _) =>
(tracing ("Using cached certificate from " ^
File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
- output)))
+ output))) |> check_return_code
in
--- a/src/Tools/cache_io.ML Sun Nov 14 17:33:28 2010 +0100
+++ b/src/Tools/cache_io.ML Mon Nov 15 14:59:53 2010 +0100
@@ -9,18 +9,20 @@
(*IO wrapper*)
val with_tmp_file: string -> (Path.T -> 'a) -> 'a
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
- val run: (Path.T -> Path.T -> string) -> string ->
- {output: string list, redirected_output: string list, return_code: int}
+ type result = {
+ output: string list,
+ redirected_output: string list,
+ return_code: int}
+ val run: (Path.T -> Path.T -> string) -> string -> result
(*cache*)
type cache
val make: Path.T -> cache
val cache_path_of: cache -> Path.T
- val lookup: cache -> string -> (string list * string list) option * string
+ val lookup: cache -> string -> result option * string
val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
- string -> string list * string list
- val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
- string list * string list
+ string -> result
+ val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
end
structure Cache_IO : CACHE_IO =
@@ -45,6 +47,11 @@
val _ = try File.rm_tree path
in Exn.release x end
+type result = {
+ output: string list,
+ redirected_output: string list,
+ return_code: int}
+
fun run make_cmd str =
with_tmp_file cache_io_prefix (fn in_path =>
with_tmp_file cache_io_prefix (fn out_path =>
@@ -98,7 +105,9 @@
else if i < p + len1 then (i+1, apfst (cons line) xsp)
else if i < p + len2 then (i+1, apsnd (cons line) xsp)
else (i, xsp)
- in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
+ val (out, err) =
+ pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
+ in {output=err, redirected_output=out, return_code=0} end
fun lookup (Cache {path=cache_path, table}) str =
let val key = SHA1.digest str
@@ -110,9 +119,8 @@
fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
let
- val {output=err, redirected_output=out, ...} = run make_cmd str
- val res = (out, err)
- val (l1, l2) = pairself length res
+ val {output=err, redirected_output=out, return_code} = run make_cmd str
+ val (l1, l2) = pairself length (out, err)
val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
val lines = map (suffix "\n") (header :: out @ err)
@@ -121,7 +129,7 @@
else
let val _ = File.append_list cache_path lines
in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
- in res end
+ in {output=err, redirected_output=out, return_code=return_code} end
fun run_cached cache make_cmd str =
(case lookup cache str of