From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- contrib/dp/dp.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'contrib/dp/dp.ml') diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index af684e6e..131dd029 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -639,8 +639,8 @@ let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ()) let sprintf = Format.sprintf let call_simplify fwhy = - if Sys.command (sprintf "why --simplify %s" fwhy) <> 0 then - anomaly ("call to why --simplify " ^ fwhy ^ " failed; please report"); + let cmd = sprintf "why --simplify %s" 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 10 Simplify %s > out 2>&1 && grep -q -w Valid out" fsx @@ -652,8 +652,7 @@ let call_simplify fwhy = let call_zenon fwhy = let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in - if Sys.command cmd <> 0 then - anomaly ("call to " ^ cmd ^ " failed; please report"); + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in let cmd = sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn @@ -669,8 +668,8 @@ let call_zenon fwhy = r let call_cvcl fwhy = - if Sys.command (sprintf "why --cvcl %s" fwhy) <> 0 then - anomaly ("call to why --cvcl " ^ fwhy ^ " failed; please report"); + let cmd = sprintf "why --cvcl %s" fwhy in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in let cmd = sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" fcvc @@ -681,8 +680,8 @@ let call_cvcl fwhy = r let call_harvey fwhy = - if Sys.command (sprintf "why --harvey %s" fwhy) <> 0 then - anomaly ("call to why --harvey " ^ fwhy ^ " failed; please report"); + let cmd = sprintf "why --harvey %s" fwhy in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed"); -- cgit v1.2.3