diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
commit | 220afeb0eb1b0b63fccd29e254f3179cac834c12 (patch) | |
tree | 7ff6cc51b5e09034658fe053ccff4675a964ed13 /src/verit/verit.ml | |
parent | a827528c0435f2006560b8cb359420bbffe85881 (diff) | |
parent | 4c348a170ea80d20f08ccd5b20e98f56b9267485 (diff) | |
download | smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.tar.gz smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.zip |
Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13
Diffstat (limited to 'src/verit/verit.ml')
-rw-r--r-- | src/verit/verit.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/verit/verit.ml b/src/verit/verit.ml index eed1dca..7f89943 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -193,25 +193,25 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt = if l = "warning : proof_done: status is still open" then raise Unknown else if l = "Invalid memory reference" then - Structures.warning "verit-warning" ("veriT outputted the warning: " ^ l) + CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ l) else if n >= 7 && String.sub l 0 7 = "warning" then - Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) + CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) else if n >= 8 && String.sub l 0 8 = "error : " then - Structures.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8))) + CoqInterface.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8))) else - Structures.error ("veriT failed with the error: " ^ l) + CoqInterface.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in try - if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); + if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); raise_warnings_errors (); let res = import_trace ra_quant rf_quant logfilename (Some first) lsmt in close_in win; Sys.remove wname; res with x -> close_in win; Sys.remove wname; match x with - | Unknown -> Structures.error "veriT returns 'unknown'" - | VeritSyntax.Sat -> Structures.error "veriT found a counter-example" + | Unknown -> CoqInterface.error "veriT returns 'unknown'" + | VeritSyntax.Sat -> CoqInterface.error "veriT found a counter-example" | _ -> raise x let verit_logic = |