From c6c1d1a119b3e99bc01d7aa936d21a0bb81dc827 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jan 2022 13:36:35 +0100
Subject: [PATCH] [wp] Removes native:alt-ergo
---
src/plugins/wp/Cmath.ml | 2 -
src/plugins/wp/GuiGoal.ml | 8 +-
src/plugins/wp/GuiList.ml | 2 -
src/plugins/wp/GuiNavigator.ml | 2 -
src/plugins/wp/GuiProver.ml | 6 +-
src/plugins/wp/Lang.ml | 11 +-
src/plugins/wp/Lang.mli | 1 -
src/plugins/wp/LogicBuiltins.ml | 2 +-
src/plugins/wp/Makefile.in | 4 +-
src/plugins/wp/MemMemory.ml | 8 +-
src/plugins/wp/MemVal.ml | 6 +-
src/plugins/wp/Plang.ml | 2 +-
src/plugins/wp/ProverErgo.ml | 513 --------------------------------
src/plugins/wp/ProverErgo.mli | 32 --
src/plugins/wp/ProverScript.ml | 2 +-
src/plugins/wp/VCS.ml | 17 +-
src/plugins/wp/VCS.mli | 1 -
src/plugins/wp/Vlist.ml | 2 -
src/plugins/wp/driver.mll | 10 +-
src/plugins/wp/prover.ml | 1 -
src/plugins/wp/wpo.ml | 4 +-
21 files changed, 23 insertions(+), 613 deletions(-)
delete mode 100644 src/plugins/wp/ProverErgo.ml
delete mode 100644 src/plugins/wp/ProverErgo.mli
diff --git a/src/plugins/wp/Cmath.ml b/src/plugins/wp/Cmath.ml
index bb51d8d1d63..d0cb850341f 100644
--- a/src/plugins/wp/Cmath.ml
+++ b/src/plugins/wp/Cmath.ml
@@ -182,7 +182,6 @@ let builtin_strict_leq lfun ~domain ~zero ~monotonic a b =
let f_iabs =
extern_f ~library:"cmath"
~link:{
- altergo = Qed.Engine.F_call "abs_int";
why3 = Qed.Engine.F_call "IAbs.abs";
coq = Qed.Engine.F_call "Z.abs";
} "\\iabs"
@@ -191,7 +190,6 @@ let f_rabs =
extern_f ~library:"cmath"
~result:Real ~params:[Sreal]
~link:{
- altergo = Qed.Engine.F_call "abs_real";
why3 = Qed.Engine.F_call "RAbs.abs";
coq = Qed.Engine.F_call "R.abs";
} "\\rabs"
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index c1a83ee641d..c0420177356 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -118,7 +118,6 @@ class pane (gprovers : GuiConfig.provers) =
let iformat = new iformat in
let rformat = new rformat in
let strategies = new GuiTactic.strategies () in
- let native = List.mem "native:alt-ergo" (Wp_parameters.Provers.get ()) in
object(self)
val mutable state : state = Empty
@@ -140,15 +139,11 @@ class pane (gprovers : GuiConfig.provers) =
Config.config_float ~key:"GuiGoal.palette" ~default:0.8 content
);
layout#populate (Wbox.panel ~top:toolbar content#widget) ;
- let native_ergo =
- if native then [
- new GuiProver.prover ~console:text ~prover:VCS.NativeAltErgo
- ] else [] in
let why3_provers =
List.map
(fun dp -> new GuiProver.prover ~console:text ~prover:(VCS.Why3 dp))
(Why3.Whyconf.Sprover.elements gprovers#get) in
- provers <- native_ergo @ why3_provers ;
+ provers <- why3_provers ;
List.iter (fun p -> palette#add_tool p#tool) provers ;
palette#add_tool strategies#tool ;
Strategy.iter strategies#register ;
@@ -275,7 +270,6 @@ class pane (gprovers : GuiConfig.provers) =
autofocus#set mode ; self#update
method private provers =
- (if native then [ VCS.NativeAltErgo ] else []) @
(List.map (fun dp -> VCS.Why3 dp)
(Why3.Whyconf.Sprover.elements gprovers#get))
diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/GuiList.ml
index 5bd26da272a..8363dfff62d 100644
--- a/src/plugins/wp/GuiList.ml
+++ b/src/plugins/wp/GuiList.ml
@@ -152,8 +152,6 @@ class pane (gprovers:GuiConfig.provers) =
self#create_prover
[ VCS.Qed ; VCS.Tactical ] ;
let prv = Wp_parameters.Provers.get () in
- if List.mem "native:alt-ergo" prv then
- self#create_prover VCS.NativeAltErgo ;
if List.mem "native:coq" prv then
self#create_prover VCS.NativeCoq ;
ignore (list#add_column_empty) ;
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 49b85d6d685..62afceed657 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -262,7 +262,6 @@ class behavior
let mode = match mode , prover with
| Some m , _ -> m
| None , VCS.NativeCoq -> VCS.Edit
- | None , VCS.NativeAltErgo -> VCS.Fix
| _ -> if VCS.is_auto prover then VCS.Batch else VCS.Fix in
schedule (Prover.prove w ~mode ~result prover) ;
refresh w
@@ -346,7 +345,6 @@ class behavior
| None | Some Tactical -> popup_tip#run ()
| Some Qed -> popup_qed#run ()
| Some NativeCoq -> popup_coq#run ()
- | Some NativeAltErgo -> popup_ergo#run ()
| Some (Why3 _ as p) ->
if VCS.is_auto p
then popup_why3_auto#run ()
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 2105cb52f79..7de00bf46ae 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -28,14 +28,14 @@ let smoke_status = `Share "theme/default/valid_under_hyp.png"
let filter = function
| VCS.Qed | VCS.Tactical | VCS.NativeCoq -> false
- | VCS.Why3 _ | VCS.NativeAltErgo -> true
+ | VCS.Why3 _ -> true
(* -------------------------------------------------------------------------- *)
(* --- Palette Tool --- *)
(* -------------------------------------------------------------------------- *)
let timeout_for = function
- | VCS.NativeAltErgo | VCS.Why3 _ ->
+ | VCS.Why3 _ ->
let value = Wp_parameters.Timeout.get () in
let spin = new Widget.spinner
~tooltip:"Prover Timeout (0 for none)"
@@ -44,7 +44,7 @@ let timeout_for = function
| _ -> None
let stepout_for = function
- | VCS.NativeAltErgo ->
+ | VCS.Why3 _ ->
let value = Wp_parameters.Steps.get () in
let spin = new Widget.spinner
~tooltip:"Prover Step Limit (0 for none)"
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index a75ac05e65c..e62d3942fbc 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -106,7 +106,6 @@ let lemma_id l = Printf.sprintf "Q_%s" (avoid_leading_backlash l)
type 'a infoprover =
{
- altergo: 'a;
why3 : 'a;
coq : 'a;
}
@@ -114,13 +113,11 @@ type 'a infoprover =
(* generic way to have different informations for the provers *)
let infoprover x = {
- altergo = x;
why3 = x;
coq = x;
}
let map_infoprover f i = {
- altergo = f i.altergo;
why3 = f i.why3;
coq = f i.coq;
}
@@ -259,8 +256,8 @@ struct
type t = adt
let basename = function
- | Mtype a -> basename "M" a.ext_link.altergo
- | Mrecord(r,_) -> basename "R" r.ext_link.altergo
+ | Mtype a -> basename "M" a.ext_link.why3
+ | Mrecord(r,_) -> basename "R" r.ext_link.why3
| Comp (c,KValue) -> basename (if c.cstruct then "S" else "U") c.corig_name
| Comp (c,KInit) -> basename (if c.cstruct then "IS" else "IU") c.corig_name
| Atype lt -> basename "A" lt.lt_name
@@ -331,7 +328,7 @@ let datatype ~library name =
Mtype m
let record ~link ~library fts =
- let m = new_extern ~link ~library ~debug:link.altergo in
+ let m = new_extern ~link ~library ~debug:link.why3 in
let r = { fields = [] } in
let fs = List.map (fun (f,t) -> Mfield(m,r,f,t)) fts in
r.fields <- fs ; Mrecord(m,r)
@@ -527,7 +524,7 @@ let extern_p ~library ?bool ?prop ?link ?(params=[]) ?(coloring=false) () =
| _ , _ , Some info -> info
| _ , _ , _ -> assert false
in
- let debug = Export.debug link.altergo in
+ let debug = Export.debug link.why3 in
Model {
m_category = Logic.Function;
m_params = params ;
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index c685aeaaca3..a508d69de73 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -36,7 +36,6 @@ type library = string
In case a Qed.Engine.link is used, [F_subst] patterns
are not supported for Why-3. *)
type 'a infoprover = {
- altergo: 'a;
why3 : 'a;
coq : 'a;
}
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 5808c304bcf..4d012aefea2 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -239,7 +239,7 @@ let add_logic ~source result name kinds ~library ?category ~link () =
let add_predicate ~source name kinds ~library ~link () =
let params = List.map skind kinds in
- let lfun = Lang.extern_fp ~library ~params ~link link.altergo in
+ let lfun = Lang.extern_fp ~library ~params ~link link.why3 in
register ~source name kinds (LFUN lfun)
let add_ctor ~source name kinds ~library ~link () =
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index d9c8c5f2903..ed8e8a09187 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -94,7 +94,7 @@ PLUGIN_CMO:= \
TacSequence \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
- ProverTask ProverErgo ProverCoq \
+ ProverTask ProverCoq \
filter_axioms Cache ProverWhy3 \
driver prover ProverSearch ProverScript \
Factory \
@@ -305,13 +305,11 @@ clean::
ALL_COQ_SOURCES= $(addprefix coqwp/, $(COQ_LIBS_CEA) $(COQ_LIBS_INRIA))
ALL_COQ_BINARIES= $(addsuffix o, $(ALL_COQ_SOURCES))
-ALL_ERGO_SOURCES= $(addprefix ergo/, $(ERGO_LIBS_CEA) $(ERGO_LIBS_INRIA))
ALL_WHY3_SOURCES= $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA))
ALL_RESOURCES= \
wp.driver \
$(ALL_COQ_SOURCES) \
- $(ALL_ERGO_SOURCES) \
$(ALL_WHY3_SOURCES)
INSTALL_OPT?=
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 2a1f2ec14ab..a9c94fe2263 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -34,13 +34,11 @@ let library = "memory"
let a_addr = Lang.datatype ~library "addr"
let t_addr = L.Data(a_addr,[])
let f_base = Lang.extern_f ~library ~result:L.Int
- ~link:{altergo = Qed.Engine.F_subst("%1.base");
- why3 = Qed.Engine.F_call "base";
+ ~link:{why3 = Qed.Engine.F_call "base";
coq = Qed.Engine.F_subst("(base %1)");
} "base"
let f_offset = Lang.extern_f ~library ~result:L.Int
- ~link:{altergo = Qed.Engine.F_subst("%1.offset");
- why3 = Qed.Engine.F_call "offset";
+ ~link:{why3 = Qed.Engine.F_call "offset";
coq = Qed.Engine.F_subst("(offset %1)");
} "offset"
let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
@@ -62,13 +60,11 @@ let ty_fst_arg = function
let l_havoc = Qed.Engine.{
coq = F_call "fhavoc" ;
- altergo = F_call "havoc" ;
why3 = F_call "havoc" ;
}
let l_set_init = Qed.Engine.{
coq = F_call "fset_init" ;
- altergo = F_call "set_init" ;
why3 = F_call "set_init" ;
}
diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
index 41fe7034755..b880015256d 100644
--- a/src/plugins/wp/MemVal.ml
+++ b/src/plugins/wp/MemVal.ml
@@ -93,13 +93,11 @@ let library = "memory"
let a_addr = Lang.datatype ~library "addr"
let t_addr = Logic.Data(a_addr,[])
let f_base = Lang.extern_f ~library ~result:Logic.Int
- ~link:{altergo = Qed.Engine.F_subst("%1.base");
- why3 = Qed.Engine.F_subst("%1.base");
+ ~link:{why3 = Qed.Engine.F_subst("%1.base");
coq = Qed.Engine.F_subst("(base %1)");
} "base"
let f_offset = Lang.extern_f ~library ~result:Logic.Int
- ~link:{altergo = Qed.Engine.F_subst("%1.offset");
- why3 = Qed.Engine.F_subst("%1.offset");
+ ~link:{why3 = Qed.Engine.F_subst("%1.offset");
coq = Qed.Engine.F_subst("(offset %1)");
} "offset"
let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
diff --git a/src/plugins/wp/Plang.ml b/src/plugins/wp/Plang.ml
index 57124006229..f67bbaa3564 100644
--- a/src/plugins/wp/Plang.ml
+++ b/src/plugins/wp/Plang.ml
@@ -75,7 +75,7 @@ class engine =
object(self)
inherit E.engine as super
inherit Lang.idprinting
- method infoprover w = w.altergo
+ method infoprover w = w.why3
(* --- Types --- *)
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
deleted file mode 100644
index e78bb4bb0f7..00000000000
--- a/src/plugins/wp/ProverErgo.ml
+++ /dev/null
@@ -1,513 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Prover Alt-Ergo Interface --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Cil_types
-open Qed
-open Lang
-open Definitions
-
-let dkey = Wp_parameters.register_category "prover"
-let dkey_cluster = Wp_parameters.register_category "cluster"
-
-let option_file = LogicBuiltins.create_option
- (fun ~driver_dir x -> Filename.concat driver_dir x)
- "altergo" "file"
-
-(* -------------------------------------------------------------------------- *)
-(* --- Making Goal File --- *)
-(* -------------------------------------------------------------------------- *)
-
-let altergo_gui =
- lazy
- begin
- let name = Wp_parameters.AltGrErgo.get () in
- let x = Command.command name [| "-version" |] in
- match x with
- | Unix.WEXITED 0 -> true
- | Unix.WEXITED 127 -> Wp_parameters.error ~current:false "AltGr-Ergo command '%s' not found." name; false
- | Unix.WEXITED r -> Wp_parameters.error ~current:false "AltGr-Ergo command '%s' exits with status [%d]" name r ; false
- | _ -> Wp_parameters.error ~current:false "AltGr-Ergo command '%s' does not work." name; false
- end
-
-let append_file out file =
- let lines = ref 0 in
- Command.read_lines file
- begin fun line ->
- output_string out line ;
- output_string out "\n" ;
- incr lines ;
- end ;
- !lines
-
-let rec locate_error files file line =
- match files with
- | [] -> ProverTask.location file line
- | (f,n)::files ->
- if line <= n then ProverTask.location f line
- else locate_error files file (line-n)
-
-let cluster_file c =
- let dir = WpContext.directory () in
- let base = cluster_id c in
- Format.sprintf "%s/%s.ergo" (dir :> string) base
-
-(* -------------------------------------------------------------------------- *)
-(* --- Exporting Formulae to Alt-Ergo --- *)
-(* -------------------------------------------------------------------------- *)
-
-type depend =
- | D_file of string
- | D_cluster of cluster
-
-[@@@warning "-32"]
-let pp_depend fmt = function
- | D_file file -> Format.fprintf fmt "File %s" file
- | D_cluster cluster -> Format.fprintf fmt "Cluster %a"
- Definitions.pp_cluster cluster
-[@@@warning "+32"]
-
-module TYPES = WpContext.Index
- (struct
- type key = adt
- type data = tau
- let name = "ProverErgo.TYPES"
- let compare = ADT.compare
- let pretty = ADT.pretty
- end)
-
-let engine =
- let module E = Qed.Export_altergo.Make(Lang.F.QED) in
- object(self)
- inherit E.engine as super
- inherit Lang.idprinting
-
- method infoprover p = p.altergo
- method set_typedef = TYPES.define
- method get_typedef = TYPES.get
-
- val mutable share = true
- method! shareable e = share && super#shareable e
- method! declare_axiom fmt a xs tgs phi =
- try share <- false ; super#declare_axiom fmt a xs tgs phi ; share <- true
- with err -> share <- true ; raise err
-
- val mutable goal = false
- method set_goal g = goal <- g
-
- method private is_vlist polarity a b =
- goal && self#mode = polarity &&
- (Vlist.check_term a || Vlist.check_term b)
-
- method! pp_equal fmt a b =
- if self#is_vlist Qed.Engine.Mpositive a b
- then Qed.Plib.pp_call_var "vlist_eq" self#pp_term fmt [a;b]
- else super#pp_equal fmt a b
-
- method! pp_noteq fmt a b =
- if self#is_vlist Qed.Engine.Mnegative a b
- then
- begin
- Format.fprintf fmt "@[<hov 2>not@,(" ;
- Qed.Plib.pp_call_var "vlist_eq" self#pp_term fmt [a;b] ;
- Format.fprintf fmt ")@]" ;
- end
- else super#pp_noteq fmt a b
-
- method! pp_fun cmode fct ts =
- if fct == Vlist.f_concat
- then Vlist.export self ts
- else super#pp_fun cmode fct ts
-
- end
-
-class visitor fmt c =
- object(self)
-
- inherit Definitions.visitor c
- inherit ProverTask.printer fmt (cluster_title c)
-
- val mutable deps = []
-
- (* --- Managing Formatter --- *)
-
- method flush =
- begin
- Format.pp_print_newline fmt () ;
- List.rev deps
- end
-
- (* --- Files, Theories and Clusters --- *)
-
- method add_dfile f =
- let df = D_file f in
- if not (List.mem df deps) then deps <- df :: deps
-
- method add_shared f = self#add_dfile ((Wp_parameters.Share.get_file ~mode:`Must_exist f) :> string)
- method add_library f = self#add_dfile f
-
- method on_cluster c = deps <- (D_cluster c) :: deps
-
- method on_library thy =
- let iter file = self#add_library file in
- List.iter iter
- (LogicBuiltins.get_option option_file ~library:thy)
-
- method on_type lt def =
- begin
- self#lines ;
- engine#declare_type fmt (Lang.adt lt) (List.length lt.lt_params) def ;
- end
-
- method private gen_on_comp kind c fts =
- begin
- self#lines ;
- let adt = match kind with
- | KValue -> Lang.comp c
- | KInit -> Lang.comp_init c
- in
- let t = match fts with
- | None -> Qed.Engine.Tabs
- | Some fts -> Qed.Engine.Trec fts
- in
- engine#declare_type fmt adt 0 t ;
- end
-
- method on_comp = self#gen_on_comp KValue
- method on_icomp = self#gen_on_comp KInit
-
- method on_dlemma l =
- begin
- self#paragraph ;
- engine#declare_axiom fmt
- (Lang.lemma_id l.l_name)
- l.l_forall l.l_triggers
- (F.e_prop l.l_lemma)
- end
-
- method on_dfun d =
- begin
- self#paragraph ;
- match d.d_definition with
- | Logic t ->
- engine#declare_signature fmt
- d.d_lfun (List.map F.tau_of_var d.d_params) t ;
- | Function(t,_,v) ->
- engine#declare_definition fmt
- d.d_lfun d.d_params t v
- | Predicate(_,p) ->
- engine#declare_definition fmt
- d.d_lfun d.d_params Logic.Prop (F.e_prop p)
- | Inductive ds ->
- engine#declare_signature fmt
- d.d_lfun (List.map F.tau_of_var d.d_params) Logic.Prop;
- List.iter self#on_dlemma ds
- end
-
- end
-
-let write_cluster c job =
- let f = cluster_file c in
- Wp_parameters.debug ~dkey "Generate '%s'" f ;
- let output = Command.print_file f
- begin fun fmt ->
- let v = new visitor fmt c in
- engine#set_goal false ;
- job v ;
- v#flush
- end
- in
- if Wp_parameters.has_dkey dkey_cluster then
- Log.print_on_output
- begin fun fmt ->
- Format.fprintf fmt "---------------------------------------------@\n" ;
- Format.fprintf fmt "--- File '%s/%s.ergo' @\n"
- (WpContext.get_context () |> WpContext.S.id) (cluster_id c) ;
- Format.fprintf fmt "---------------------------------------------@\n" ;
- Command.pp_from_file fmt f ;
- end ;
- output
-
-(* -------------------------------------------------------------------------- *)
-(* --- File Assembly --- *)
-(* -------------------------------------------------------------------------- *)
-
-module CLUSTERS = WpContext.Index
- (struct
- type key = cluster
- type data = int * depend list
- let name = "ProverErgo.CLUSTERS"
- let compare = cluster_compare
- let pretty = pp_cluster
- end)
-
-type export = {
- out : out_channel ;
- mutable files : (string * int) list ;
-}
-
-let rec assemble export = function
- | D_file file -> assemble_file export file
- | D_cluster c -> assemble_cluster export c
-
-and assemble_file export file =
- if List.for_all (fun (f,_) -> f <> file) export.files
- then
- let lines = append_file export.out file in
- export.files <- (file,lines) :: export.files
-
-and assemble_cluster export c =
- let (age,deps) = try CLUSTERS.find c with Not_found -> (-1,[]) in
- let deps =
- if age < cluster_age c then
- let deps = write_cluster c (fun v -> v#vself) in
- CLUSTERS.update c (cluster_age c , deps) ; deps
- else deps
- in
- List.iter (assemble export) deps ;
- let file = cluster_file c in
- assemble_file export file
-
-and assemble_lib export lib =
- assemble_file export (LogicBuiltins.find_lib lib)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Assembling Goal --- *)
-(* -------------------------------------------------------------------------- *)
-
-let assemble_goal ~file ~id ~title ~axioms prop =
- let goal = cluster ~id ~title () in
- let deps = write_cluster goal
- begin fun v ->
- v#on_library "qed";
- v#vgoal axioms prop ;
- v#paragraph ;
- try
- let qlet = List.mem "qlet" (Wp_parameters.AltErgoFlags.get ()) in
- engine#set_quantify_let qlet ;
- engine#set_goal true ;
- engine#global
- begin fun () ->
- v#printf "@[<hv 2>goal %s:@ %a@]@." id
- engine#pp_goal (F.e_prop prop) ;
- end ;
- engine#set_quantify_let false ;
- engine#set_goal false ;
- with error ->
- engine#set_quantify_let false ;
- engine#set_goal false ;
- raise error
- end in
- Command.write_file file
- begin fun out ->
- let export = { files = [] ; out = out } in
- List.iter (assemble export) deps ;
- let libs = Wp_parameters.AltErgoLibs.get () in
- List.iter (assemble_lib export) libs ;
- assemble_file export (cluster_file goal) ;
- List.rev export.files
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Running AltErgo --- *)
-(* -------------------------------------------------------------------------- *)
-
-open ProverTask
-
-(*bug in Alt-Ergo: sometimes error messages are repeated. *)
-(*let p_loc = "^File " ... *)
-
-let p_loc = "^File " ^ p_string ^ ", line " ^ p_int ^ ", [^:]+:"
-let p_valid = p_loc ^ "Valid (" ^ p_float ^ ") (" ^ p_int ^ "\\( +steps\\)?)"
-let p_unsat = p_loc ^ "I don't know"
-let p_limit = "^Steps limit reached: " ^ p_int
-
-let re_error = Str.regexp p_loc
-let re_valid = Str.regexp p_valid
-let re_limit = Str.regexp p_limit
-let re_unsat = Str.regexp p_unsat
-
-class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
- object(ergo)
-
- inherit ProverTask.command (Wp_parameters.AltErgo.get ())
-
- val mutable files = []
- val mutable error = None
- val mutable valid = false
- val mutable limit = false
- val mutable unsat = false
- val mutable timer = 0.0
- val mutable steps = 0
-
- method private time t = timer <- t
-
- method private error (a : pattern) =
- let lpos = locate_error files (a#get_string 1) (a#get_int 2) in
- let message = a#get_after ~offset:1 2 in
- error <- Some ( lpos , message )
-
- method private valid (a : pattern) =
- begin
- valid <- true ;
- timer <- a#get_float 3 ;
- steps <- a#get_int 4 ;
- end
-
- method private limit (a : pattern) =
- begin
- limit <- true ;
- steps <- pred (a#get_int 1) ;
- end
-
- method private unsat (_ : pattern) =
- begin
- unsat <- true ;
- end
-
- method result r =
- if r = 127 then
- let cmd = Wp_parameters.AltErgo.get () in
- VCS.kfailed "Command '%s' not found" cmd
- else
- match error with
- | Some(pos,message) when unsat || limit || not valid ->
- let source = Cil_datatype.Position.of_lexing_pos pos in
- Wp_parameters.error ~source "Alt-Ergo error:@\n%s" message ;
- VCS.failed ~pos message
- | _ ->
- try
- let verdict =
- if unsat then VCS.Unknown else
- if valid then VCS.Valid else
- if limit then VCS.Stepout else
- raise Not_found in
- VCS.result
- ~time:(if gui then 0.0 else timer)
- ~steps verdict
- with Not_found ->
- begin
- let message std =
- Format.asprintf
- "Alt-Ergo (%s) for goal %a"
- std WpPropId.pretty pid
- in
- if Wp_parameters.verbose_atleast 1 then begin
- ProverTask.pp_file ~message:(message "stdout") ~file:logout ;
- ProverTask.pp_file ~message:(message "stderr") ~file:logerr ;
- end;
- if r = 0 then VCS.failed "Unexpected Alt-Ergo output"
- else VCS.kfailed "Alt-Ergo exits with status [%d]." r
- end
-
- method prove =
- files <- lines ;
- if gui then ergo#set_command (Wp_parameters.AltGrErgo.get ()) ;
- ergo#add_parameter ~name:"-proof" Wp_parameters.ProofTrace.get ;
- ergo#add_parameter ~name:"-model" Wp_parameters.ProofTrace.get ;
- let flags = List.filter
- (fun p -> p <> "qlet")
- (Wp_parameters.AltErgoFlags.get ()) in
- ergo#add flags ;
- ergo#add [ file ] ;
- if not gui then begin
- ergo#add_positive
- ~name:"-steps-bound" ~value:(VCS.get_stepout config) ;
- let smoke = WpPropId.is_smoke_test pid in
- ergo#timeout (VCS.get_timeout ~smoke config) ;
- end ;
- ergo#validate_time ergo#time ;
- ergo#validate_pattern ~logs:`ERR re_error ergo#error ;
- ergo#validate_pattern ~logs:`OUT re_valid ergo#valid ;
- ergo#validate_pattern ~logs:`OUT re_limit ergo#limit ;
- ergo#validate_pattern ~logs:`OUT re_unsat ergo#unsat ;
- ergo#run ~logout ~logerr ()
-
- end
-
-open VCS
-open Wpo
-open Task
-
-let try_prove ~config ~pid ~gui ~file ~lines ~logout ~logerr =
- let ergo = new altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr in
- ergo#prove >>> function
- | Task.Timeout t -> Task.return (VCS.timeout t)
- | Task.Result r -> Task.call ergo#result r
- | st -> Task.status (Task.map (fun _ -> assert false) st)
-
-let prove_file ~config ~pid ~mode ~file ~lines ~logout ~logerr =
- let gui = match mode with
- | Edit -> Lazy.force altergo_gui
- | Batch | Update | Fix | FixUpdate -> false in
- try_prove ~config ~pid ~gui ~file ~lines ~logout ~logerr >>= function
- | { verdict=(VCS.Unknown|VCS.Timeout|VCS.Stepout) }
- when (mode = Fix || mode = FixUpdate) && Lazy.force altergo_gui ->
- try_prove ~config ~pid ~gui:true ~file ~lines ~logout ~logerr
- | r -> Task.return r
-
-let prove_prop ~config ~pid ~mode ~context ~axioms ~prop =
- let prover = NativeAltErgo in
- let model = fst context in
- let file = DISK.file_goal ~pid ~model ~prover in
- let logout = DISK.file_logout ~pid ~model ~prover in
- let logerr = DISK.file_logerr ~pid ~model ~prover in
- let id = WpPropId.get_propid pid in
- let title = Pretty_utils.to_string WpPropId.pretty pid in
- let lines = WpContext.on_context context
- (assemble_goal ~file ~id ~title ~axioms) prop in
- if Wp_parameters.has_print_generated () then
- WpContext.on_context context (fun () ->
- let goal = cluster ~id ~title () in
- Wp_parameters.print_generated (cluster_file goal)
- ) () ;
- if Wp_parameters.Generate.get ()
- then Task.return VCS.no_result
- else prove_file ~config ~pid ~mode ~file ~lines ~logout ~logerr
-
-let prove_annot context pid vcq ~config ~mode =
- Task.todo
- begin fun () ->
- let axioms = vcq.VC_Annot.axioms in
- let prop = GOAL.compute_proof ~pid vcq.VC_Annot.goal in
- prove_prop ~pid ~config ~mode ~context ~axioms ~prop
- end
-
-let prove_lemma context pid vca ~config ~mode =
- Task.todo
- begin fun () ->
- let lemma = vca.Wpo.VC_Lemma.lemma in
- let depends = vca.Wpo.VC_Lemma.depends in
- let prop = F.p_forall lemma.l_forall lemma.l_lemma in
- let axioms = Some(lemma.l_cluster,depends) in
- prove_prop ~pid ~config ~mode ~context ~axioms ~prop
- end
-
-let prove ~config ~mode wpo =
- let pid = wpo.Wpo.po_pid in
- let context = Wpo.get_context wpo in
- match wpo.Wpo.po_formula with
- | Wpo.GoalAnnot vcq -> prove_annot context pid vcq ~config ~mode
- | Wpo.GoalLemma vca -> prove_lemma context pid vca ~config ~mode
diff --git a/src/plugins/wp/ProverErgo.mli b/src/plugins/wp/ProverErgo.mli
deleted file mode 100644
index 6355a6e1b81..00000000000
--- a/src/plugins/wp/ProverErgo.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Task
-open VCS
-
-(* -------------------------------------------------------------------------- *)
-(* --- Alt-Ergo Theorem Prover --- *)
-(* -------------------------------------------------------------------------- *)
-
-val dkey_cluster: Wp_parameters.category
-
-val prove : config:config -> mode:mode -> Wpo.t -> result task
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 46f3ae3cf80..ffdbeed2d2d 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -36,7 +36,7 @@ struct
let stage = function
| Prover( Qed , { verdict = Valid } ) -> 0
- | Prover( (NativeAltErgo | Why3 _) , { verdict = Valid } ) -> 1
+ | Prover( Why3 _ , { verdict = Valid } ) -> 1
| Prover( NativeCoq , { verdict = Valid } ) -> 2
| Tactic _ -> 3
| Prover _ -> 4
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 05aacf11a7c..9adac2908d3 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -28,7 +28,6 @@ let dkey_shell = Wp_parameters.register_category "shell"
type prover =
| Why3 of Why3Provers.t (* Prover via WHY *)
- | NativeAltErgo (* Direct Alt-Ergo *)
| NativeCoq (* Direct Coq and Coqide *)
| Qed (* Qed Solver *)
| Tactical (* Interactive Prover *)
@@ -43,12 +42,6 @@ type mode =
let parse_prover = function
| "" | "none" -> None
| "qed" | "Qed" -> Some Qed
- | "native-alt-ergo" (* for wp-reports *)
- | "native:alt-ergo" | "native:altgr-ergo"
- ->
- Wp_parameters.warning ~once:true ~current:false
- "native support for alt-ergo is deprecated, use why3 instead" ;
- Some NativeAltErgo
| "native-coq" (* for wp-reports *)
| "native:coq" | "native:coqide" | "native:coqedit"
->
@@ -90,7 +83,6 @@ let parse_mode m =
let name_of_prover = function
| Why3 s -> Why3Provers.print_wp s
- | NativeAltErgo -> "native:alt-ergo"
| NativeCoq -> "native:coq"
| Qed -> "qed"
| Tactical -> "script"
@@ -100,7 +92,6 @@ let title_of_prover = function
if Wp_parameters.has_dkey dkey_shell
then Why3Provers.name s
else Why3Provers.title s
- | NativeAltErgo -> "Alt-Ergo (native)"
| NativeCoq -> "Coq (native)"
| Qed -> "Qed"
| Tactical -> "Script"
@@ -128,13 +119,12 @@ let sanitize_why3 s =
let filename_for_prover = function
| Why3 s -> sanitize_why3 (Why3Provers.print_wp s)
- | NativeAltErgo -> "Alt-Ergo"
| NativeCoq -> "Coq"
| Qed -> "Qed"
| Tactical -> "Tactical"
let is_auto = function
- | Qed | NativeAltErgo -> true
+ | Qed -> true
| Tactical | NativeCoq -> false
| Why3 p ->
match p.prover_name with
@@ -152,9 +142,6 @@ let cmp_prover p q =
| Qed , Qed -> 0
| Qed , _ -> (-1)
| _ , Qed -> 1
- | NativeAltErgo , NativeAltErgo -> 0
- | NativeAltErgo , _ -> (-1)
- | _ , NativeAltErgo -> 1
| Tactical , Tactical -> 0
| Tactical , _ -> (-1)
| _ , Tactical -> 1
@@ -344,7 +331,7 @@ let pp_result fmt r =
let is_qualified prover result =
match prover with
| Qed | Tactical -> true
- | NativeAltErgo | NativeCoq -> result.verdict <> Timeout
+ | NativeCoq -> result.verdict <> Timeout
| Why3 _ -> result.cached || result.prover_time < Rformat.epsilon
let pp_cache_miss fmt st updating prover result =
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index f45575f2b6d..544d259d47e 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -28,7 +28,6 @@
type prover =
| Why3 of Why3Provers.t (** Prover via WHY *)
- | NativeAltErgo (** Direct Alt-Ergo *)
| NativeCoq (** Direct Coq and Coqide *)
| Qed (** Qed Solver *)
| Tactical (** Interactive Prover *)
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index a748662b125..204b5adac9c 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -41,12 +41,10 @@ let t_list = "\\list"
let l_list = Lang.infoprover "list"
let l_concat = Lang.infoprover (E.F_right "concat")
let l_elt = Lang.(E.({
- altergo = F_subst "cons(%1,nil)" ;
why3 = F_call "elt" ;
coq = F_subst "(cons %1 nil)" ;
}))
let l_repeat = Lang.(E.({
- altergo = F_call "repeat_box" ;
why3 = F_call "repeat" ;
coq = F_call "repeat" ;
}))
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index 8404774fb29..3f297a4ddd5 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -289,11 +289,10 @@ and bal = parse
| RECLINK l ->
skip input ;
begin try
- {Lang.altergo = conv_bal def (List.assoc "altergo" l);
- why3 = conv_bal def (List.assoc "why3" l);
+ {Lang.why3 = conv_bal def (List.assoc "why3" l);
coq = conv_bal def (List.assoc "coq" l) }
with Not_found ->
- failwith "a link must contain an entry for 'altergo', 'why3' and 'coq'"
+ failwith "a link must contain an entry for 'why3' and 'coq'"
end
| _ -> failwith "Missing link symbol"
@@ -304,11 +303,10 @@ and bal = parse
| `RecString l ->
skip input ;
begin try
- {Lang.altergo = List.assoc "altergo" l;
- why3 = List.assoc "why3" l;
+ {Lang.why3 = List.assoc "why3" l;
coq = List.assoc "coq" l }
with Not_found ->
- failwith "a link must contain an entry for 'altergo', 'why3' and 'coq'"
+ failwith "a link must contain an entry for 'why3' and 'coq'"
end
| _ -> failwith "Missing link symbol"
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index addb11faabb..7ba0c5f0a55 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -33,7 +33,6 @@ let dispatch ?(config=VCS.default) mode prover wpo =
begin
match prover with
| Qed | Tactical -> Task.return VCS.no_result
- | NativeAltErgo -> ProverErgo.prove ~config ~mode wpo
| NativeCoq -> ProverCoq.prove mode wpo
| Why3 prover ->
let smoke = Wpo.is_smoke_test wpo in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 699646cfaa8..91b006ef291 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -106,7 +106,6 @@ struct
let file_goal ~pid ~model ~prover =
let ext = match prover with
| Qed -> "qed"
- | NativeAltErgo -> "mlw"
| Why3 _ -> "why"
| NativeCoq -> "v"
| Tactical -> "tac"
@@ -117,7 +116,6 @@ struct
let file_kf ~kf ~model ~prover =
let ext = match prover with
| Qed -> "qed"
- | NativeAltErgo -> "mlw"
| Why3 _ -> "why"
| NativeCoq -> "v"
| Tactical -> "tac"
@@ -470,7 +468,7 @@ module ProverType =
type t = prover
include Datatype.Undefined
let name = "Wpo.prover"
- let reprs = [ NativeAltErgo; NativeCoq; Qed ]
+ let reprs = [ NativeCoq; Qed ]
end)
(* to get a "reasonable" API doc: *)
let () = Type.set_ml_name ProverType.ty (Some "Wpo.prover")
--
GitLab