Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit cac6f913 authored by Mário Pereira's avatar Mário Pereira

Refinement

Somes experiments around the generation of type invariants implication.
parent 562e6ef1
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
......@@ -920,9 +920,9 @@ module Transform = struct
let e, spv = expr info subst e in
let e_bl, spv_bl = mk_list_eb bl (xbranch info subst) in
mk (Etry (e, e_bl)), Spv.union spv spv_bl
| Eassign al ->
| Eassign al -> (* FIXME : produced superfolous let *)
let assign e (_, _, pv) = mk_let subst pv e in
List.fold_left assign e al, Spv.empty
(* e *) List.fold_left assign e al, Spv.empty
| Econst _ | Eabsurd | Ehole -> e, Spv.empty
| Eignore e ->
let e, spv = expr info subst e in
......
......@@ -608,11 +608,25 @@ let clone_type_record cl s d s' d' =
List.iter match_pj d.itd_fields;
cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
let _self_inv itd s =
let u = create_vsymbol (id_fresh "self")
(ty_app s.its_ts (List.map ty_var s.its_ts.ts_args)) in
let t = [t_var u] in
let get_ld s (ldd,sbs) = match s.rs_logic, s.rs_field with
| RLls s, Some v ->
create_param_decl s :: ldd,
Mvs.add v.pv_vs (t_app_infer s t) sbs
| _ -> assert false in
let fl = itd.itd_fields in
let _proj, sbs = List.fold_right get_ld fl ([],Mvs.empty) in
let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
t_forall_close [u] [] inv
let clone_type_decl inst cl tdl kn =
let def =
List.fold_left (fun m d -> Mits.add d.itd_its d m) Mits.empty tdl in
let htd = Hits.create 5 in
let vcs = ref ([] : (itysymbol * term) list) in
let vcs = ref ([] : (itysymbol * its_defn * term) list) in
let rec visit alg ({its_ts = {ts_name = id} as ts} as s) d =
if not (Hits.mem htd s) then
let alg = Sits.add s alg in
......@@ -644,7 +658,6 @@ let clone_type_decl inst cl tdl kn =
| Some s' ->
if not (List.length ts.ts_args = List.length s'.its_ts.ts_args) then
raise (BadInstance id);
(* if not (its_pure s && its_pure s') then raise (BadInstance id); *)
let pd' = Mid.find s'.its_ts.ts_name kn in
let d' = begin match pd'.pd_node with
| PDtype [d'] -> d'
......@@ -653,9 +666,15 @@ let clone_type_decl inst cl tdl kn =
raise (BadInstance id)
| PDlet _ | PDexn _ | PDpure -> raise (BadInstance id)
end in
clone_type_record cl s d s' d'
clone_type_record cl s d s' d'; (* clone record fields *)
(* if d.itd_invariant <> [] && d'.itd_invariant <> [] then begin *)
(* let d_inv = self_inv d s in *)
(* let d'_inv = self_inv d' s' in *)
(* let inv = t_implies_simp d'_inv d_inv in *)
(* Format.eprintf "inv:%a@." Pretty.print_term inv; *)
(* vcs := (d.itd_its, d, inv) :: !vcs (\* add VC for invariant *\) end *)
| None -> begin match Mts.find_opt ts inst.mi_ty with
| Some ity ->
| Some ity -> (* creative indentation *)
let stv = Stv.of_list ts.ts_args in
if not (Stv.subset (ity_freevars Stv.empty ity) stv &&
its_pure s && ity_immutable ity) then raise (BadInstance id);
......@@ -924,12 +943,18 @@ and clone_let_defn cl sm ld = match ld with
sm_save_rs cl sm d.rec_sym d'.rec_sym) sm rdl rdl' in
sm, ld
let add_vc uc (its, f) =
let add_vc uc (its, td, f) =
let {id_string = nm; id_loc = loc} = its.its_ts.ts_name in
let label = Slab.singleton (Ident.create_label ("expl:VC for " ^ nm)) in
let pr = create_prsymbol (id_fresh ~label ?loc ("VC " ^ nm)) in
(* let td = create_alias_decl (id_fresh nm) [] its in *)
let td = create_type_decl [td] in (* FIXME *)
let uc = add_pdecl_raw ~warn:false uc td in
let d = create_pure_decl (create_prop_decl Pgoal pr f) in
add_pdecl ~warn:false ~vc:false uc d
Format.eprintf "ici@.";
let res = add_pdecl ~warn:false ~vc:false uc d in
Format.eprintf "ici2@.";
res
let clone_pdecl inst cl uc d = match d.pd_node with
| PDtype tdl ->
......
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