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 db2a9f42 authored by Martin Clochard's avatar Martin Clochard
parents 7994c06b 981dfbea
...@@ -53,7 +53,7 @@ module M ...@@ -53,7 +53,7 @@ module M
(*** In all cases, records are decomposed using match eval ***) (*** In all cases, records are decomposed using match eval ***)
type r = {f "field_f" :int; g:bool} type r = {f "model_trace:field_f" :int; g:bool}
(* Projection functions *) (* Projection functions *)
function projf_r_f "model_trace:.f" (x : r) : int function projf_r_f "model_trace:.f" (x : r) : int
......
...@@ -52,12 +52,12 @@ let is_model_trace_label label = ...@@ -52,12 +52,12 @@ let is_model_trace_label label =
true true
with Not_found -> false with Not_found -> false
let get_model_trace_label labels = let get_model_trace_label ~labels =
Slab.choose (Slab.filter is_model_trace_label labels) Slab.choose (Slab.filter is_model_trace_label labels)
let transform_model_trace_label labels trans_fun = let transform_model_trace_label labels trans_fun =
try try
let trace_label = get_model_trace_label labels in let trace_label = get_model_trace_label ~labels in
let labels_without_trace = Slab.remove trace_label labels in let labels_without_trace = Slab.remove trace_label labels in
let new_trace_label = create_label (trans_fun trace_label.lab_string) in let new_trace_label = create_label (trans_fun trace_label.lab_string) in
Slab.add new_trace_label labels_without_trace Slab.add new_trace_label labels_without_trace
...@@ -76,7 +76,7 @@ let append_to_model_trace_label ~labels ~to_append = ...@@ -76,7 +76,7 @@ let append_to_model_trace_label ~labels ~to_append =
transform_model_trace_label labels trans transform_model_trace_label labels trans
let get_model_element_name ~labels = let get_model_element_name ~labels =
let trace_label = get_model_trace_label labels in let trace_label = get_model_trace_label ~labels in
let splitted1 = Str.bounded_split (Str.regexp_string ":") trace_label.lab_string 2 in let splitted1 = Str.bounded_split (Str.regexp_string ":") trace_label.lab_string 2 in
match splitted1 with match splitted1 with
| [_; content] -> | [_; content] ->
...@@ -140,6 +140,9 @@ let id_fresh ?(label = Slab.empty) ?loc nm = ...@@ -140,6 +140,9 @@ let id_fresh ?(label = Slab.empty) ?loc nm =
let id_user ?(label = Slab.empty) nm loc = let id_user ?(label = Slab.empty) nm loc =
create_ident nm label (Some loc) create_ident nm label (Some loc)
let id_lab label id =
create_ident id.id_string label id.id_loc
let id_clone ?(label = Slab.empty) id = let id_clone ?(label = Slab.empty) id =
let ll = Slab.union label id.id_label in let ll = Slab.union label id.id_label in
create_ident id.id_string ll id.id_loc create_ident id.id_string ll id.id_loc
......
...@@ -49,6 +49,10 @@ val get_model_element_name : labels : Slab.t -> string ...@@ -49,6 +49,10 @@ val get_model_element_name : labels : Slab.t -> string
Throws Not_found if there is no element name (there is no Throws Not_found if there is no element name (there is no
label of the form "model_trace:+". *) label of the form "model_trace:+". *)
val get_model_trace_label : labels : Slab.t -> Slab.elt
(** Return label of the for "model_trace:*".
Throws Not_found if there is no such label.*)
(** {2 Identifiers} *) (** {2 Identifiers} *)
type ident = private { type ident = private {
...@@ -83,6 +87,9 @@ val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid ...@@ -83,6 +87,9 @@ val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
(* create a localized pre-ident *) (* create a localized pre-ident *)
val id_user : ?label:Slab.t -> string -> Loc.position -> preid val id_user : ?label:Slab.t -> string -> Loc.position -> preid
(* create a duplicate pre-ident with given labels *)
val id_lab : Slab.t -> ident -> preid
(* create a duplicate pre-ident *) (* create a duplicate pre-ident *)
val id_clone : ?label:Slab.t -> ident -> preid val id_clone : ?label:Slab.t -> ident -> preid
......
...@@ -69,10 +69,10 @@ let rec print_indices fmt indices = ...@@ -69,10 +69,10 @@ let rec print_indices fmt indices =
print_indices fmt tail print_indices fmt tail
and and
print_array fmt arr = print_array fmt arr =
fprintf fmt "[others -> "; fprintf fmt "(others => ";
print_model_value fmt arr.arr_others; print_model_value fmt arr.arr_others;
print_indices fmt arr.arr_indices; print_indices fmt arr.arr_indices;
fprintf fmt "]" fprintf fmt ")"
and and
print_model_value_sanit sanit_print fmt value = print_model_value_sanit sanit_print fmt value =
(* Prints model value. *) (* Prints model value. *)
......
...@@ -603,4 +603,3 @@ let () = Exn_printer.register ...@@ -603,4 +603,3 @@ let () = Exn_printer.register
fprintf fmt "Cannot prove the termination of %a" print_ls ls fprintf fmt "Cannot prove the termination of %a" print_ls ls
| _ -> raise exn | _ -> raise exn
end end
...@@ -64,4 +64,3 @@ val print_task : formatter -> task -> unit ...@@ -64,4 +64,3 @@ val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit val print_theory : formatter -> theory -> unit
val print_namespace : formatter -> string -> theory -> unit val print_namespace : formatter -> string -> theory -> unit
...@@ -61,10 +61,25 @@ let rec add_quant kn (vl,tl,f) v = ...@@ -61,10 +61,25 @@ let rec add_quant kn (vl,tl,f) v =
| _ -> [] | _ -> []
in in
match cl with match cl with
| [ls,_] -> | [ls,pjl] ->
(* there is only one constructor *)
let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in let mk_v ty pj =
let nvl = List.map mk_v ls.ls_args in (* The name of the field corresponding to the variable that is created *)
let field_name = begin match pj with
| Some pj_ls ->
begin
try
Ident.get_model_element_name ~labels:pj_ls.ls_name.id_label
with Not_found -> pj_ls.ls_name.id_string
end
| _ -> ""
end in
let label = Ident.append_to_model_element_name
~labels:v.vs_name.id_label ~to_append:("." ^ field_name) in
create_vsymbol (id_lab label v.vs_name) (ty_inst s ty) in
let nvl = List.map2 mk_v ls.ls_args pjl in
let t = fs_app ls (List.map t_var nvl) ty in let t = fs_app ls (List.map t_var nvl) ty in
let f = t_let_close_simp v t f in let f = t_let_close_simp v t f in
let tl = tr_map (t_subst_single v t) tl in let tl = tr_map (t_subst_single v t) tl in
...@@ -114,7 +129,7 @@ let eval_match ~inline kn t = ...@@ -114,7 +129,7 @@ let eval_match ~inline kn t =
let rec eval stop env t = let rec eval stop env t =
let stop = stop || Slab.mem Split_goal.stop_split t.t_label in let stop = stop || Slab.mem Split_goal.stop_split t.t_label in
let eval = eval stop in let eval = eval stop in
t_label_copy t (match t.t_node with let t_eval_matched = (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ -> | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
cs_equ kn env (eval env t1) (eval env t2) cs_equ kn env (eval env t1) (eval env t2)
| Tapp (ls, [t1]) when is_projection kn ls -> | Tapp (ls, [t1]) when is_projection kn ls ->
...@@ -142,7 +157,18 @@ let eval_match ~inline kn t = ...@@ -142,7 +157,18 @@ let eval_match ~inline kn t =
else List.fold_left (add_quant kn) ([],tl,f) vl in else List.fold_left (add_quant kn) ([],tl,f) vl in
t_quant_simp q (close (List.rev vl) tl (eval env f)) t_quant_simp q (close (List.rev vl) tl (eval env f))
| _ -> | _ ->
t_map_simp (eval env) t) t_map_simp (eval env) t) in
(* Copy all labels of t to t_eval_matched except for "model_trace:*" label.
This label is not copied if both t and t_eval_matched contain it. *)
let t =
(try
let _ = Ident.get_model_trace_label ~labels:t_eval_matched.t_label in
let original_mt_label = Ident.get_model_trace_label ~labels:t.t_label in
(* If both t_eval_matched and t contain model_trace label, remove it *)
t_label_remove original_mt_label t
with Not_found -> t) in
t_label_copy t t_eval_matched
in in
eval false Mvs.empty t eval false Mvs.empty t
......
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