Commit cd56dae7 authored by Mário Pereira's avatar Mário Pereira
Browse files
parents e33ac290 5fe2e452
...@@ -39,10 +39,17 @@ and pdecl_node = ...@@ -39,10 +39,17 @@ and pdecl_node =
let pd_equal : pdecl -> pdecl -> bool = (==) let pd_equal : pdecl -> pdecl -> bool = (==)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let ity_mark = ity_pur ts_mark []
let pv_old = create_pvsymbol ~ghost:true (id_fresh "%old") ity_mark
let mk_decl = let mk_decl =
let r = ref 0 in let r = ref 0 in
fun node syms news -> fun node syms news ->
incr r; incr r;
let syms = Sid.remove pv_old.pv_vs.vs_name syms in
{ pd_node = node; pd_syms = syms; pd_news = news; pd_tag = !r; } { pd_node = node; pd_syms = syms; pd_news = news; pd_tag = !r; }
let news_id s id = Sid.add_new (Decl.ClashIdent id) id s let news_id s id = Sid.add_new (Decl.ClashIdent id) id s
......
...@@ -41,6 +41,13 @@ and pdecl_node = private ...@@ -41,6 +41,13 @@ and pdecl_node = private
| PDrec of fun_defn list | PDrec of fun_defn list
| PDexn of xsymbol | PDexn of xsymbol
(** {2 Marks} *)
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val ity_mark : ity
val pv_old : pvsymbol
(** {2 Declaration constructors} *) (** {2 Declaration constructors} *)
type pre_field = preid option * field type pre_field = preid option * field
......
...@@ -937,7 +937,7 @@ let check_user_effect ?ps e spec args dsp = ...@@ -937,7 +937,7 @@ let check_user_effect ?ps e spec args dsp =
Loc.errorm ?loc:(e_find_loc (fun e -> has_write reg e.e_effect) e) Loc.errorm ?loc:(e_find_loc (fun e -> has_write reg e.e_effect) e)
"this@ expression@ produces@ an@ unlisted@ write@ effect" in "this@ expression@ produces@ an@ unlisted@ write@ effect" in
if dsp.ds_checkrw then begin if dsp.ds_checkrw then begin
let reads = Spv.remove Mlw_wp.pv_old e.e_syms.syms_pv in let reads = Spv.remove Mlw_decl.pv_old e.e_syms.syms_pv in
let reads = Spv.diff reads (spec_pvset Spv.empty spec) in let reads = Spv.diff reads (spec_pvset Spv.empty spec) in
Spv.iter check_read (Spv.diff reads args); Spv.iter check_read (Spv.diff reads args);
Sreg.iter check_write eeff.eff_writes; Sreg.iter check_write eeff.eff_writes;
......
...@@ -1346,7 +1346,7 @@ let eval_global_expr env mkm tkm _writes e = ...@@ -1346,7 +1346,7 @@ let eval_global_expr env mkm tkm _writes e =
let add_glob _ d ((venv,renv) as acc) = let add_glob _ d ((venv,renv) as acc) =
match d.Mlw_decl.pd_node with match d.Mlw_decl.pd_node with
| Mlw_decl.PDval (Mlw_expr.LetV pvs) | Mlw_decl.PDval (Mlw_expr.LetV pvs)
when not (pv_equal pvs Mlw_wp.pv_old) -> when not (pv_equal pvs Mlw_decl.pv_old) ->
let ity = pvs.pv_ity in let ity = pvs.pv_ity in
let v = any_value_of_type env (ty_of_ity ity) in let v = any_value_of_type env (ty_of_ity ity) in
let renv,v = to_program_value env renv (VTvalue ity) v in let renv,v = to_program_value env renv (VTvalue ity) v in
......
...@@ -400,10 +400,7 @@ let xs_exit = create_xsymbol (id_fresh "%Exit") ity_unit ...@@ -400,10 +400,7 @@ let xs_exit = create_xsymbol (id_fresh "%Exit") ity_unit
let mod_prelude = let mod_prelude =
let pd_exit = create_exn_decl xs_exit in let pd_exit = create_exn_decl xs_exit in
let pd_old = create_val_decl (LetV Mlw_wp.pv_old) in
let uc = empty_module None (id_fresh "Prelude") ["why3";"Prelude"] in let uc = empty_module None (id_fresh "Prelude") ["why3";"Prelude"] in
let uc = use_export_theory uc Mlw_wp.mark_theory in
let uc = add_pdecl ~wp:false uc pd_old in
let uc = add_pdecl ~wp:false uc pd_exit in let uc = add_pdecl ~wp:false uc pd_exit in
close_module uc close_module uc
...@@ -536,7 +533,7 @@ let clone_export uc m minst inst = ...@@ -536,7 +533,7 @@ let clone_export uc m minst inst =
| VTarrow a -> VTarrow (conv_aty mv a) | VTarrow a -> VTarrow (conv_aty mv a)
| VTvalue v -> VTvalue (conv_ity v) in | VTvalue v -> VTvalue (conv_ity v) in
vty_arrow args ~spec vty in vty_arrow args ~spec vty in
let mvs = ref (Mvs.singleton Mlw_wp.pv_old.pv_vs Mlw_wp.pv_old.pv_vs) in let mvs = ref (Mvs.singleton pv_old.pv_vs pv_old.pv_vs) in
let add_pdecl uc d = { uc with let add_pdecl uc d = { uc with
muc_decls = d :: uc.muc_decls; muc_decls = d :: uc.muc_decls;
muc_known = known_add_decl (Theory.get_known nth) uc.muc_known d; muc_known = known_add_decl (Theory.get_known nth) uc.muc_known d;
......
...@@ -447,8 +447,6 @@ module Translate = struct ...@@ -447,8 +447,6 @@ module Translate = struct
| None -> ML.Tapp (ts.ts_name, List.map (ity info) tl) | None -> ML.Tapp (ts.ts_name, List.map (ity info) tl)
end end
let ity_mark = ity_pur Mlw_wp.ts_mark []
let is_underscore pv = let is_underscore pv =
pv.pv_vs.vs_name.id_string = "_" && ity_equal pv.pv_ity ity_unit pv.pv_vs.vs_name.id_string = "_" && ity_equal pv.pv_ity ity_unit
...@@ -631,7 +629,7 @@ module Translate = struct ...@@ -631,7 +629,7 @@ module Translate = struct
let pdecl info pd = let pdecl info pd =
match pd.pd_node with match pd.pd_node with
| PDval (LetV pv) when pv_equal pv Mlw_wp.pv_old -> | PDval (LetV pv) when pv_equal pv Mlw_decl.pv_old ->
[] []
| PDval _ -> | PDval _ ->
[] []
......
...@@ -18,6 +18,7 @@ open Theory ...@@ -18,6 +18,7 @@ open Theory
open Mlw_ty open Mlw_ty
open Mlw_ty.T open Mlw_ty.T
open Mlw_expr open Mlw_expr
open Mlw_decl
let debug = Debug.register_info_flag "whyml_wp" let debug = Debug.register_info_flag "whyml_wp"
~desc:"Print@ details@ of@ verification@ conditions@ generation." ~desc:"Print@ details@ of@ verification@ conditions@ generation."
...@@ -32,11 +33,6 @@ let lemma_label = Ident.create_label "why3:lemma" ...@@ -32,11 +33,6 @@ let lemma_label = Ident.create_label "why3:lemma"
(** Marks *) (** Marks *)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let ity_mark = ity_pur ts_mark []
let fresh_mark () = create_vsymbol (id_fresh "'mark") ty_mark let fresh_mark () = create_vsymbol (id_fresh "'mark") ty_mark
let fs_at = let fs_at =
...@@ -70,7 +66,6 @@ let e_now = e_ghost (e_lapp fs_now [] (ity_pur ts_mark [])) ...@@ -70,7 +66,6 @@ let e_now = e_ghost (e_lapp fs_now [] (ity_pur ts_mark []))
(* [vs_old] appears in the postconditions given to the core API, (* [vs_old] appears in the postconditions given to the core API,
which expects every vsymbol to be a pure part of a pvsymbol *) which expects every vsymbol to be a pure part of a pvsymbol *)
let pv_old = create_pvsymbol ~ghost:true (id_fresh "%old") ity_mark
let vs_old = pv_old.pv_vs let vs_old = pv_old.pv_vs
let t_old = t_var vs_old let t_old = t_var vs_old
......
...@@ -12,7 +12,6 @@ ...@@ -12,7 +12,6 @@
(** {1 Weakest preconditions} *) (** {1 Weakest preconditions} *)
open Theory open Theory
open Mlw_ty
open Mlw_ty.T open Mlw_ty.T
open Mlw_decl open Mlw_decl
open Mlw_expr open Mlw_expr
...@@ -21,9 +20,6 @@ open Mlw_expr ...@@ -21,9 +20,6 @@ open Mlw_expr
val lemma_label : Ident.label val lemma_label : Ident.label
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val fs_at : Term.lsymbol val fs_at : Term.lsymbol
val fs_old : Term.lsymbol val fs_old : Term.lsymbol
...@@ -36,7 +32,6 @@ val th_mark_old : Theory.theory ...@@ -36,7 +32,6 @@ val th_mark_old : Theory.theory
val fs_now : Term.lsymbol val fs_now : Term.lsymbol
val e_now : expr val e_now : expr
val pv_old : pvsymbol
val remove_old : Term.term -> Term.term val remove_old : Term.term -> Term.term
val full_invariant : val full_invariant :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment