Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 2a794b99 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Mlw: partially revert cda6d915: labels do not define exceptions

It is confusing to use the keyword "label" to define an exception.
Also, the "label L in ..." binds too far and the break point is
not clearly defined.

We do need some syntactic sugar for
  exception X t in try <expr> with X r -> r
(at the very least "break" and "continue"), but labels are not it.
parent 28ad4e77
......@@ -240,6 +240,7 @@ module NaturalMergesort
variant { n - !first_run }
label L in
let lo = ref 0 in
exception Break in try
while !lo < n - 1 do
invariant { 0 <= !lo <= n }
invariant { !first_run at L <= !first_run <= n }
......@@ -248,7 +249,7 @@ module NaturalMergesort
invariant { permut_all (a at L) a }
variant { n - !lo }
let mid = find_run a !lo in
if mid = n then begin if !lo = 0 then return; raise L end;
if mid = n then begin if !lo = 0 then return; raise Break end;
let hi = find_run a mid in
label M in
merge_using tmp a !lo mid hi;
......@@ -257,6 +258,7 @@ module NaturalMergesort
ghost if !lo = 0 then first_run := hi;
lo := hi;
done
with Break -> () end
done
......
......@@ -438,7 +438,7 @@ and dexpr_node =
| DEtrue
| DEfalse
| DEcast of dexpr * dity
| DEmark of preid * dity * dexpr
| DEmark of preid * dexpr
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
......@@ -797,10 +797,10 @@ let dexpr ?loc node =
| DEtrue
| DEfalse ->
dvty_bool
| DEcast (de,dity)
| DEmark (_,dity,de) ->
| DEcast (de,dity) ->
dexpr_expected_type de dity;
de.de_dvty
| DEmark (_,de)
| DEuloc (de,_)
| DElabel (de,_) ->
de.de_dvty in
......@@ -1254,7 +1254,7 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
| DEexn (id,dity,mask,de) ->
let xs = create_xsymbol id ~mask (ity_of_dity dity) in
cexp uloc (add_xsymbol env xs) de (LD (LX xs) :: lpl)
| DEmark (id,_,de) ->
| DEmark (id,de) ->
let env, old = add_label env id.pre_name in
cexp uloc env de (LD (LL old) :: lpl)
| DEsym _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _
......@@ -1398,18 +1398,10 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DEexn (id,dity,mask,de) ->
let xs = create_xsymbol id ~mask (ity_of_dity dity) in
e_exn xs (expr uloc (add_xsymbol env xs) de)
| DEmark (id,dity,de) ->
let xs = create_xsymbol id (ity_of_dity dity) in
| DEmark (id,de) ->
let env, old = add_label env id.pre_name in
let e = expr uloc (add_xsymbol env xs) de in
let e = if Sxs.mem xs e.e_effect.eff_raises then
let v = create_pvsymbol (id_fresh "result") xs.xs_ity in
(* FIXME? We assume that the generated exception will not
be catched inside e. Otherwise, it will not appear in
the effect and we will not declare the exception here. *)
e_exn xs (e_try e (Mxs.singleton xs ([v], e_var v))) else e in
let put _ (ld,_) e = e_let ld e in
Hpv.fold put old e
Hpv.fold put old (expr uloc env de)
| DEcast _ | DEuloc _ | DElabel _ ->
assert false (* already stripped *)
......
......@@ -128,7 +128,7 @@ and dexpr_node =
| DEtrue
| DEfalse
| DEcast of dexpr * dity
| DEmark of preid * dity * dexpr
| DEmark of preid * dexpr
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
......
......@@ -781,10 +781,8 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Eassert (ak, f) ->
DEassert (ak, dassert muc f)
| Ptree.Emark (id, e1) ->
let dity = dity_fresh () in
let id = create_user_id id in
let denv = denv_add_exn denv id dity in
DEmark (id, dity, dexpr muc denv e1)
DEmark (id, dexpr muc denv e1)
| Ptree.Escope (q, e1) ->
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
......
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