Skip to content

Commit 0f5bf06

Browse files
makes JS compile (but is going to need follow-up work)
1 parent e465a44 commit 0f5bf06

File tree

2 files changed

+5
-4
lines changed

2 files changed

+5
-4
lines changed

src/js/astjs.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -146,7 +146,7 @@ module Make (Cfg : Config) = struct
146146
| Named (n, t) -> to_js_object "Name" [| js_string n; typ_js t |]
147147
| Weak t -> to_js_object "Weak" [| typ_js t |]
148148

149-
and field_js { Type.lab; typ = t; src = s } =
149+
and field_js { Type.lab; typ = t; src = s; _ } =
150150
to_js_object lab (typ_js t :: src s |> Array.of_list)
151151

152152
and src ({ Type.depr; track_region; region = r } : Type.src) :
@@ -500,7 +500,7 @@ module Make (Cfg : Config) = struct
500500
and typ_field'_js =
501501
let open Syntax in
502502
function
503-
| ValF (lab, t, m) ->
503+
| ValF (lab, _, t, m) ->
504504
to_js_object "ValF" [| id lab; syntax_typ_js t; mut_js m |]
505505
| TypF (lab, tbs, t) ->
506506
to_js_object "TypF"
@@ -578,6 +578,7 @@ module Make (Cfg : Config) = struct
578578
function
579579
| WildP -> js_string "WildP"
580580
| VarP x -> to_js_object "VarP" [| id x |]
581+
| ImplicitP { id = x; _ } -> to_js_object "VarP" [| id x |]
581582
| TupP ps -> to_js_object "TupP" (List.map pat_js ps |> Array.of_list)
582583
| ObjP ps -> to_js_object "ObjP" (List.map pat_field_js ps |> Array.of_list)
583584
| AnnotP (p, t) -> to_js_object "AnnotP" [| pat_js p; syntax_typ_js t |]

test/viper/ok/label-break-continue.vpr.ok

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,8 @@ method label_expressions($Self: Ref)
5050
label $lbl$simple;
5151
assert (simple_label == 42);
5252
implicit_leave := 42;
53-
goto $lbl$implicit;
54-
label $lbl$implicit;
53+
goto $lbl$implicit_;
54+
label $lbl$implicit_;
5555
assert (implicit_leave == 42);
5656
if (true)
5757
{

0 commit comments

Comments
 (0)