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 83189039 authored by Mário Pereira's avatar Mário Pereira

Extraction: test if a [val] declaration is assigned in the driver

parent bb137664
......@@ -716,7 +716,6 @@ module Translate = struct
let args = params cty.cty_args in
let res = mlty_of_ity cty.cty_mask cty.cty_result in
[Mltree.Dlet (Mltree.Lany (rs, res, args))]
(* raise (ExtractionVal _rs) *)
| PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
[]
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
......
......@@ -259,6 +259,14 @@ module Print = struct
| Eapp (s, []) -> rs_equal s rs_false
| _ -> false
exception ExtractionVal of rsymbol
let val_in_drv info rs = (* we suppose [rs] refers to a [val] declaration *)
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name with
| None, None -> raise (ExtractionVal rs)
| _ -> ()
let rec print_apply_args info fmt = function
| expr :: exprl, pv :: pvl ->
if is_optional ~labels:(pv_name pv).id_label then
......@@ -381,7 +389,7 @@ module Print = struct
(print_list arrow (print_ty_arg info)) args
(print_ty info) res;
forget_vars args
| Lany _ -> () (* FIXME: test driver here and fail if no driver *)
| Lany (rs, _, _) -> val_in_drv info rs
and print_enode ?(paren=false) info fmt = function
| Econst c ->
......@@ -602,6 +610,11 @@ module Print = struct
fprintf fmt "@." end in
List.iter decide_print decl_name
let () = Exn_printer.register (fun fmt e -> match e with
| ExtractionVal rs -> Format.fprintf fmt
"Function %a cannot be extracted" Expr.print_rs rs
| _ -> raise e)
end
let print_decl =
......
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