From 06e25b89657540d67a848981985ecaac071dc663 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 19 Apr 2019 17:51:07 +0200
Subject: [PATCH] [wp/why3] update why3 command outputs
---
src/plugins/wp/ProverWhy3.ml | 30 +++++++++++++-----------------
1 file changed, 13 insertions(+), 17 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 56cbd3f35d0..a40c44aecb8 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -133,21 +133,21 @@ class visitor fmt c =
method add_import ?was thy =
self#lines ;
match was with
- | None -> Format.fprintf fmt "use import %s@\n" thy
- | Some was -> Format.fprintf fmt "use import %s as %s@\n" thy was
+ | None -> Format.fprintf fmt "use %s@\n" thy
+ | Some was -> Format.fprintf fmt "use %s as %s@\n" thy was
method add_import2 file thy =
self#lines ;
- Format.fprintf fmt "use import %s.%s@\n" file thy
+ Format.fprintf fmt "use %s.%s@\n" file thy
method add_import3 file thy name =
self#lines ;
- Format.fprintf fmt "use import %s.%s as %s@\n" file thy name
+ Format.fprintf fmt "use %s.%s as %s@\n" file thy name
method on_cluster c =
self#lines ;
let name = (cluster_id c) in
- Format.fprintf fmt "use import %s.%s@\n"
+ Format.fprintf fmt "use %s.%s@\n"
name (Transitioning.String.capitalize_ascii name) ;
deps <- (D_cluster c) :: deps
@@ -348,7 +348,7 @@ let assemble_goal ~id ~title ~theory ?axioms prop fmt =
engine#set_goal true ;
engine#global
begin fun () ->
- v#printf "@[<hv 2>goal %s \"expl:%s\":@ %a@]@\n@\n"
+ v#printf "@[<hv 2>goal %s[@expl:%s]:@ %a@]@\n@\n"
why3_goal_name
title
engine#pp_prop (F.e_prop prop) ;
@@ -469,11 +469,11 @@ let assemble_goal wpo =
open ProverTask
-let p_goal = p_until_space ^ " " ^ p_until_space ^ " " ^ p_until_space ^ " : "
+let p_goal = ".* [a-zA-Z0-9_]+: "
let p_valid = p_goal ^ "Valid (" ^ p_float ^ "s\\(,[^)]*\\)?)"
let p_limit = p_goal ^ "Timeout"
let p_error = "File " ^ p_string ^ ", line " ^ p_int ^ ", characters "
- ^ p_int ^ "-" ^ p_int ^ ":\n\\(warning:\\)?"
+ ^ p_int ^ "-" ^ p_int ^ ":\nsyntax error"
let re_valid = Str.regexp p_valid
let re_limit = Str.regexp p_limit
@@ -515,17 +515,13 @@ class why3 ~timeout ~prover ~pid ~file ~includes ~logout ~logerr =
method private time t = time <- t
method private error (a : pattern) =
- try
- let _warning = a#get_string 5 in
- ()
- with Not_found ->
- let lpos = ProverTask.location (a#get_string 1) (a#get_int 2) in
- error <- Error_Generated ( lpos , a#get_after ~offset:1 4 )
+ let lpos = ProverTask.location (a#get_string 1) (a#get_int 2) in
+ error <- Error_Generated ( lpos , "why3 " ^ a#get_after ~offset:1 4 )
method private valid (a : pattern) =
begin
valid <- true ;
- time <- a#get_float 4 ;
+ time <- a#get_float 1 ;
end
method private limit (_a : pattern) =
@@ -541,10 +537,10 @@ class why3 ~timeout ~prover ~pid ~file ~includes ~logout ~logerr =
match error with
| Error_Generated(pos,message) ->
let source = Cil_datatype.Position.of_lexing_pos pos in
- Wp_parameters.error ~source "Why3 error:@\n%s" message ;
+ Wp_parameters.error ~source "%s" message ;
VCS.failed ~pos message
| Error_No ->
- if r = 0 then
+ if r = 0 || r = 1 then
let verdict =
if valid then VCS.Valid else
if limit then VCS.Timeout else
--
GitLab