From 2b874b2ceb829652bf11472522b47d4fffe6606b Mon Sep 17 00:00:00 2001 From: Vladislav Zavialov Date: Sun, 16 Jun 2024 11:52:19 +0200 Subject: [PATCH] motoko-san: Generate fields New features: * dynamically generated prelude fields * arrays with tuples and options as elements New test cases: * test/viper/array-of-tuples.vpr --- src/pipeline/pipeline.ml | 2 +- src/viper/common.ml | 14 ++- src/viper/prelude.ml | 20 ++-- src/viper/prelude.mli | 1 + src/viper/pretty.ml | 7 +- src/viper/trans.ml | 60 ++++++----- test/repl/ok/viper.stdout.ok | 8 -- test/viper/array-of-tuples.mo | 26 +++++ test/viper/ok/array-of-tuples.silicon.ok | 2 + test/viper/ok/array-of-tuples.vpr.ok | 101 ++++++++++++++++++ test/viper/ok/array.silicon.ok | 2 +- test/viper/ok/array.vpr.ok | 8 +- test/viper/ok/assertions.silicon.ok | 4 +- test/viper/ok/assertions.vpr.ok | 8 -- test/viper/ok/async.silicon.ok | 2 +- test/viper/ok/async.vpr.ok | 8 -- test/viper/ok/claim-broken.silicon.ok | 2 +- test/viper/ok/claim-broken.vpr.ok | 8 -- test/viper/ok/claim-reward-naive.vpr.ok | 8 -- test/viper/ok/claim-simple.silicon.ok | 2 +- test/viper/ok/claim-simple.vpr.ok | 8 -- test/viper/ok/claim.vpr.ok | 8 -- test/viper/ok/counter.silicon.ok | 2 +- test/viper/ok/counter.vpr.ok | 8 -- test/viper/ok/invariant.silicon.ok | 2 +- test/viper/ok/invariant.vpr.ok | 8 -- test/viper/ok/label-break-continue.silicon.ok | 4 +- test/viper/ok/label-break-continue.vpr.ok | 8 -- test/viper/ok/lits.silicon.ok | 4 +- test/viper/ok/lits.vpr.ok | 8 -- test/viper/ok/loop-invariant.silicon.ok | 4 +- test/viper/ok/loop-invariant.vpr.ok | 8 -- test/viper/ok/method-call.silicon.ok | 2 +- test/viper/ok/method-call.vpr.ok | 8 -- test/viper/ok/nats.silicon.ok | 2 +- test/viper/ok/nats.vpr.ok | 8 -- test/viper/ok/odd-even.silicon.ok | 4 +- test/viper/ok/odd-even.vpr.ok | 8 -- test/viper/ok/option.silicon.ok | 2 +- test/viper/ok/option.vpr.ok | 8 -- test/viper/ok/polymono.silicon.ok | 4 +- test/viper/ok/polymono.vpr.ok | 8 -- test/viper/ok/private.vpr.ok | 8 -- test/viper/ok/reverse.silicon.ok | 2 +- test/viper/ok/reverse.vpr.ok | 7 -- test/viper/ok/simple-funs.silicon.ok | 4 +- test/viper/ok/simple-funs.vpr.ok | 8 -- test/viper/ok/text.silicon.ok | 2 +- test/viper/ok/text.vpr.ok | 19 ++-- test/viper/ok/tuple.silicon.ok | 2 +- test/viper/ok/tuple.vpr.ok | 8 -- test/viper/ok/variants.silicon.ok | 4 +- test/viper/ok/variants.vpr.ok | 8 -- 53 files changed, 226 insertions(+), 265 deletions(-) create mode 100644 src/viper/prelude.mli create mode 100644 test/viper/array-of-tuples.mo create mode 100644 test/viper/ok/array-of-tuples.silicon.ok create mode 100644 test/viper/ok/array-of-tuples.vpr.ok diff --git a/src/pipeline/pipeline.ml b/src/pipeline/pipeline.ml index 59f3babed4c..5dbbcb241f2 100644 --- a/src/pipeline/pipeline.ml +++ b/src/pipeline/pipeline.ml @@ -511,7 +511,7 @@ let viper_files' parsefn files : viper_result = let u = CompUnit.comp_unit_of_prog false prog in let reqs = Viper.Common.init_reqs () in let* v = Viper.Trans.unit reqs (Viper.Prep.prep_unit u) in - let s = Viper.Pretty.prog_mapped "" reqs v in + let s = Viper.Pretty.prog_mapped "" (Viper.Prelude.prelude reqs) v in Diag.return s let viper_files files : viper_result = diff --git a/src/viper/common.ml b/src/viper/common.ml index da14f2c76f5..dd6328ce379 100644 --- a/src/viper/common.ml +++ b/src/viper/common.ml @@ -20,9 +20,17 @@ module IntSet = Set.Make(struct let compare = compare end) +module StrMap = Map.Make(String) + (* Requirements arising from the translated code. In trans.ml we collect those requirements, in prelude.ml we generate definitons to satisfy them. *) -type reqs = { tuple_arities : IntSet.t ref } - -let init_reqs () = { tuple_arities = ref IntSet.empty } +type reqs = + { tuple_arities : IntSet.t ref + ; typed_fields : Syntax.typ StrMap.t ref + } + +let init_reqs () = + { tuple_arities = ref IntSet.empty + ; typed_fields = ref StrMap.empty + } diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml index f5e500b0021..eb0c119ca70 100644 --- a/src/viper/prelude.ml +++ b/src/viper/prelude.ml @@ -51,15 +51,15 @@ adt Option[T] { let prelude_text_encoding : string = {prelude|/* Text encoding */ function $concat(a: Int, b: Int): Int|prelude} -let prelude_typed_references : string = {prelude|/* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array]|prelude} +let pp_typed_field (name, typ) = + Format.asprintf "@[<2>field %s:@ %a@]" + name + Pretty.pp_typ typ + +let prelude_typed_references typed_fields : string = + String.concat "\n" + ("/* Typed references */" :: + List.map pp_typed_field (StrMap.bindings typed_fields)) let prelude reqs: string = String.concat "\n" @@ -69,6 +69,6 @@ let prelude reqs: string = prelude_tuple_encoding !(reqs.tuple_arities); prelude_option_encoding; prelude_text_encoding; - prelude_typed_references; + prelude_typed_references !(reqs.typed_fields); "/* END PRELUDE */" ] diff --git a/src/viper/prelude.mli b/src/viper/prelude.mli new file mode 100644 index 00000000000..3fca5507558 --- /dev/null +++ b/src/viper/prelude.mli @@ -0,0 +1 @@ +val prelude : Common.reqs -> string \ No newline at end of file diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml index cbf0431a2d6..3535177c7e9 100644 --- a/src/viper/pretty.ml +++ b/src/viper/pretty.ml @@ -1,6 +1,5 @@ open Source open Syntax -open Prelude open Format @@ -258,11 +257,11 @@ and pp_loop_inv ppf inv = marks := inv.at :: !marks; fprintf ppf "\017invariant %a\019" pp_exp inv -let prog_mapped file tuple_arities p = +let prog_mapped file prelude p = marks := []; let b = Buffer.create 16 in let ppf = Format.formatter_of_buffer b in - Format.fprintf ppf "@[%s@]@.@.@[%a@]" (prelude tuple_arities) pp_prog p; + Format.fprintf ppf "@[%s@]@.@.@[%a@]" prelude pp_prog p; Format.pp_print_flush ppf (); let in_file { left; right } = let left, right = { left with file }, { right with file } in @@ -299,4 +298,4 @@ let prog_mapped file tuple_arities p = List.fold_left tighten None mapping in Buffer.contents b, lookup -let prog tuple_arities p = fst (prog_mapped "" tuple_arities p) +let prog prelude p = fst (prog_mapped "" prelude p) diff --git a/src/viper/trans.ml b/src/viper/trans.ml index 6b1df95989d..7ce9c818047 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -187,6 +187,11 @@ let rec strip_par_p (p : M.pat) : M.pat = | M.ParP p' -> strip_par_p p' | _ -> p +let rec strip_mut_t (t : T.typ) : T.typ = + match t with + | T.Mut t' -> strip_mut_t t' + | _ -> t + let rec unit reqs (u : M.comp_unit) : prog Diag.result = Diag.( reset_stamps(); @@ -406,7 +411,7 @@ and dec_field' ctxt d = let lhs = fun ctxt' -> !!! Source.no_region (FldAcc (fldacc ctxt')) in let perms ctxt' at = conjoin ([ accE at (self ctxt' at, id x) ] - @ (access_pred (lhs ctxt') t |: []) + @ (access_pred ctxt' (lhs ctxt') t |: []) @ static_invariants at (lhs ctxt') e) at in { ctxt with ids = Env.add x.it (Field, t) ctxt.ids }, Some perms, (* perm *) @@ -437,9 +442,9 @@ and arg p = match p.it with | _ -> unsupported p.at (Arrange.pat p)) | _ -> unsupported p.at (Arrange.pat p) -and access_pred lhs t = +and access_pred ctxt lhs t = match T.normalize t with - | T.Array elem_t -> Some (array_acc Source.no_region lhs elem_t) + | T.Array elem_t -> Some (array_acc Source.no_region ctxt lhs elem_t) | _ -> None (* Get access predicates for all local variables in current scope *) @@ -448,7 +453,7 @@ and local_access_preds ctxt = let preds = Env.fold (fun id info preds -> match info with | (Local, t) -> - let pred = access_pred !!(LocalVar (!!id, tr_typ ctxt t)) t in + let pred = access_pred ctxt !!(LocalVar (!!id, tr_typ ctxt t)) t in pred |: preds | _ -> preds) ctxt.ids [] @@ -750,9 +755,9 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' = fld_via_tmp_var ctxt lval t (fun x -> let lhs = !!(LocalVar (x, tr_typ ctxt t)) in [], [ !!(AssertS !!(GeCmpE (exp ctxt e1, intLitE at 0))) - ; !!(InhaleS (array_acc at lhs (array_elem_t t))) + ; !!(InhaleS (array_acc at ctxt lhs (array_elem_t t))) ; !!(InhaleS (array_size_inv at lhs (exp ctxt e1))) - ; !!(InhaleS (array_init_const at lhs (array_elem_t t) (exp ctxt e2))) ] + ; !!(InhaleS (array_init_const at ctxt lhs (array_elem_t t) (exp ctxt e2))) ] ) | _ -> unsupported args.at (Arrange.exp args) end @@ -921,7 +926,7 @@ and rets ctxt t_opt = | T.Tup [] -> [], [] | T.Async (T.Fut, _, _) -> [], [] | typ -> - let pred = access_pred !!(LocalVar (!!"$Res", tr_typ ctxt typ)) typ in + let pred = access_pred ctxt !!(LocalVar (!!"$Res", tr_typ ctxt typ)) typ in pred |: [], [(!!"$Res", tr_typ ctxt typ)] ) @@ -978,22 +983,29 @@ and tuple_elem_ts t = | t -> failwith "tuple_elem_ts: expected tuple type" (* name of field of typed reference *) -and typed_field t = - match T.normalize t with - | T.Mut elem_t -> typed_field elem_t - | T.Prim T.Int -> "$int" - | T.Prim T.Nat -> "$int" (* Viper has no native support for Nat, so translate to Int *) - | T.Prim T.Bool -> "$bool" - | T.Prim T.Text -> "$text" - | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t) +and typed_field ctxt t = + let t' = tr_typ ctxt (strip_mut_t t) in + let name = type_field_name t' in + ctxt.reqs.typed_fields := StrMap.add name t' !(ctxt.reqs.typed_fields); + name + +and type_field_name t = + match t.it with + | IntT -> "$int" + | BoolT -> "$bool" + | RefT -> "$ref" + | ArrayT -> "$array" + | TupleT ts -> "$tuple" ^ string_of_int (List.length ts) ^ String.concat "" (List.map type_field_name ts) + | OptionT t' -> "$option" ^ type_field_name t' + | ConT (con, ts) -> "$c_" ^ con.it ^ String.concat "" (List.map type_field_name ts) and array_size_inv at lhs n = !!! at (EqCmpE (sizeE at lhs, n)) -and array_acc at lhs t = +and array_acc at ctxt lhs t = match T.normalize t with - | T.Mut _-> arrayAccE at lhs (typed_field t) FullP - | _ -> arrayAccE at lhs (typed_field t) WildcardP + | T.Mut _-> arrayAccE at lhs (typed_field ctxt t) FullP + | _ -> arrayAccE at lhs (typed_field ctxt t) WildcardP (* Allocate array on the LHS expression. Note: array_alloc assumes that the array is uninitialized. Assignment to @@ -1001,24 +1013,24 @@ and array_acc at lhs t = and array_alloc at ctxt lhs t es : stmt list = let (!!) p = !!! at p in let init_array = List.mapi (fun i e -> - FieldAssignS (locE at lhs (intLitE at i) (typed_field t), exp ctxt e)) es in + FieldAssignS (locE at lhs (intLitE at i) (typed_field ctxt t), exp ctxt e)) es in (* InhaleS (!! (FldAcc (locE at lhs (intLitE at i) (typed_field t))) === e)) es in *) let reset_perm = (match T.normalize t with | T.Mut _ -> [] - | _ -> [ExhaleS (array_acc at lhs t); InhaleS (array_acc at lhs t)])in - let stmts = [ InhaleS (array_acc at lhs (T.Mut t)) + | _ -> [ExhaleS (array_acc at ctxt lhs t); InhaleS (array_acc at ctxt lhs t)])in + let stmts = [ InhaleS (array_acc at ctxt lhs (T.Mut t)) ; InhaleS (array_size_inv at lhs (intLitE at (List.length es)))] @ init_array @ reset_perm in List.map (!!) stmts -and array_init_const at lhs t x = +and array_init_const at ctxt lhs t x = let (!!) p = !!! at p in - !! (CallE ("$array_init", [lhs; !!(FldE (typed_field t)); x])) + !! (CallE ("$array_init", [lhs; !!(FldE (typed_field ctxt t)); x])) and array_loc ctxt at e1 e2 t = - locE at (exp ctxt e1) (exp ctxt e2) (typed_field t) + locE at (exp ctxt e1) (exp ctxt e2) (typed_field ctxt t) and label_expr_alloc ~label_id ~label_type ~label_rhs ~label_note at ctxt lhs : seqn' = let ctxt = diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok index 9379885c3cf..f162e54e90f 100644 --- a/test/repl/ok/viper.stdout.ok +++ b/test/repl/ok/viper.stdout.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ field $message_async: Int diff --git a/test/viper/array-of-tuples.mo b/test/viper/array-of-tuples.mo new file mode 100644 index 00000000000..d3893d76092 --- /dev/null +++ b/test/viper/array-of-tuples.mo @@ -0,0 +1,26 @@ +// @verify +// import Array "mo:base/Array"; + +actor ArrayOfTuples { + + public func get_tup_arr(): async [(Int, Bool)] { + let x1 = (42, true); + let x2 = (0, false); + return [x1, x2]; + }; + + private func set_nested_mut_arr(arr: [var ?(?Int, (Bool, Bool))]) { + assert arr.size() >= 2; + assert:return arr.size() >= 2 and + arr[0] == (old (arr[0])) and + arr[1] == ?(?42, (true, true)); + arr[1] := ?(?42, (true, true)); + }; + + public func check_arr(): async () { + let arr : [var ?(?Int, (Bool, Bool))] = [var null, null]; + set_nested_mut_arr(arr); + assert:system arr[0] == null; + assert:system arr[1] == ?(?42, (true, true)); + } +} diff --git a/test/viper/ok/array-of-tuples.silicon.ok b/test/viper/ok/array-of-tuples.silicon.ok new file mode 100644 index 00000000000..814169d5441 --- /dev/null +++ b/test/viper/ok/array-of-tuples.silicon.ok @@ -0,0 +1,2 @@ +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (array-of-tuples.vpr@29.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array-of-tuples.vpr@30.1) diff --git a/test/viper/ok/array-of-tuples.vpr.ok b/test/viper/ok/array-of-tuples.vpr.ok new file mode 100644 index 00000000000..fbe02e0b835 --- /dev/null +++ b/test/viper/ok/array-of-tuples.vpr.ok @@ -0,0 +1,101 @@ +/* BEGIN PRELUDE */ +/* Array encoding */ +domain Array { + function $loc(a: Array, i: Int): Ref + function $size(a: Array): Int + function $loc_inv1(r: Ref): Array + function $loc_inv2(r: Ref): Int + axiom $all_diff_array { forall a: Array, i: Int :: {$loc(a, i)} $loc_inv1($loc(a, i)) == a && $loc_inv2($loc(a, i)) == i } + axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } +} +define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) +define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x +/* Tuple encoding */ +adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) } +/* Option encoding */ +adt Option[T] { + None() + Some(some$0: T) +} +/* Text encoding */ +function $concat(a: Int, b: Int): Int +/* Typed references */ +field $option$tuple2$option$int$tuple2$bool$bool: + Option[Tuple$2[Option[Int], Tuple$2[Bool, Bool]]] +field $tuple2$int$bool: Tuple$2[Int, Bool] +/* END PRELUDE */ + +define $Perm($Self) (true) +define $Inv($Self) (true) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + + } +method get_tup_arr($Self: Ref) + returns ($Res: Array) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $array_acc($Res, $tuple2$int$bool, wildcard) + ensures $Inv($Self) + { var x1: Tuple$2[Int, Bool] + var x2: Tuple$2[Int, Bool] + x1 := Tup$2(42, true); + x2 := Tup$2(0, false); + inhale $array_acc($Res, $tuple2$int$bool, write); + inhale ($size($Res) == 2); + ($loc($Res, 0)).$tuple2$int$bool := x1; + ($loc($Res, 1)).$tuple2$int$bool := x2; + exhale $array_acc($Res, $tuple2$int$bool, wildcard); + inhale $array_acc($Res, $tuple2$int$bool, wildcard); + goto $Ret; + label $Ret; + } +method set_nested_mut_arr($Self: Ref, arr: Array) + + requires $Perm($Self) + requires $array_acc(arr, $option$tuple2$option$int$tuple2$bool$bool, + write) + ensures $Perm($Self) + ensures $array_acc(arr, $option$tuple2$option$int$tuple2$bool$bool, + write) + ensures ((($size(arr) >= 2) && (($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool == + old(($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool))) && ( + ($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool == Some( + Tup$2( + Some(42), + Tup$2(true, + true))))) + { + assume ($size(arr) >= 2); + ($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool := Some( + Tup$2( + Some(42), + Tup$2(true, + true))); + label $Ret; + } +method check_arr($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { var arr: Array + inhale $array_acc(arr, $option$tuple2$option$int$tuple2$bool$bool, + write); + inhale ($size(arr) == 2); + ($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool := None(); + ($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool := None(); + set_nested_mut_arr($Self, arr); + assert (($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool == + None()); + assert (($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool == + Some(Tup$2(Some(42), Tup$2(true, true)))); + label $Ret; + } diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok index 283caf9977d..197d08f2d36 100644 --- a/test/viper/ok/array.silicon.ok +++ b/test/viper/ok/array.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@42.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@36.1) diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok index de41aca78ed..0437f0a92c7 100644 --- a/test/viper/ok/array.vpr.ok +++ b/test/viper/ok/array.vpr.ok @@ -20,14 +20,8 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] +field $int: Int /* END PRELUDE */ define $Perm($Self) (((((true && (acc(($Self).immut_arr,write) && ($array_acc( diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok index 3ef74e608d1..553e00f5c5c 100644 --- a/test/viper/ok/assertions.silicon.ok +++ b/test/viper/ok/assertions.silicon.ok @@ -1,2 +1,2 @@ - [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@42.13--42.24) - [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@60.15--60.44) + [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@34.13--34.24) + [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@52.15--52.44) diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok index d1d85fdd48f..e6477bfa8e5 100644 --- a/test/viper/ok/assertions.vpr.ok +++ b/test/viper/ok/assertions.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ field $message_async: Int diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok index 4132895445d..0bc658a1ac5 100644 --- a/test/viper/ok/async.silicon.ok +++ b/test/viper/ok/async.silicon.ok @@ -1 +1 @@ - [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@65.15--65.42) + [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@57.15--57.42) diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok index abfde21c192..95fbb7fff8d 100644 --- a/test/viper/ok/async.vpr.ok +++ b/test/viper/ok/async.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ field $message_async_4: Int diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok index 13af7bf74b0..6083507e3fa 100644 --- a/test/viper/ok/claim-broken.silicon.ok +++ b/test/viper/ok/claim-broken.silicon.ok @@ -1 +1 @@ - [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@63.20--63.47) + [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@55.20--55.47) diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok index 10dacb2c038..ddf3cfb8539 100644 --- a/test/viper/ok/claim-broken.vpr.ok +++ b/test/viper/ok/claim-broken.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ field $message_async: Int diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok index bfa3dd26762..af15146bb49 100644 --- a/test/viper/ok/claim-reward-naive.vpr.ok +++ b/test/viper/ok/claim-reward-naive.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write))) diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok index eef64e2e302..e45f21bcc4b 100644 --- a/test/viper/ok/claim-simple.silicon.ok +++ b/test/viper/ok/claim-simple.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (claim-simple.vpr@34.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (claim-simple.vpr@26.1) diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok index f14a36dca1a..9bb67fb702e 100644 --- a/test/viper/ok/claim-simple.vpr.ok +++ b/test/viper/ok/claim-simple.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write))) diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok index c1fde4d31b4..64336db61cd 100644 --- a/test/viper/ok/claim.vpr.ok +++ b/test/viper/ok/claim.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ field $message_async: Int diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok index 25cbd81e574..c54fa2ba30b 100644 --- a/test/viper/ok/counter.silicon.ok +++ b/test/viper/ok/counter.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@34.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@26.1) diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok index f31d5da3294..af536420704 100644 --- a/test/viper/ok/counter.vpr.ok +++ b/test/viper/ok/counter.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) ((true && acc(($Self).count,write))) diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok index 9d22ac740ab..33261606336 100644 --- a/test/viper/ok/invariant.silicon.ok +++ b/test/viper/ok/invariant.silicon.ok @@ -1 +1 @@ - [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@39.13--39.24) + [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@31.13--31.24) diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok index 7e70f568d78..fe43fae9625 100644 --- a/test/viper/ok/invariant.vpr.ok +++ b/test/viper/ok/invariant.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write))) diff --git a/test/viper/ok/label-break-continue.silicon.ok b/test/viper/ok/label-break-continue.silicon.ok index a01f038ad0a..65a001834d6 100644 --- a/test/viper/ok/label-break-continue.silicon.ok +++ b/test/viper/ok/label-break-continue.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (label-break-continue.vpr@35.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (label-break-continue.vpr@36.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (label-break-continue.vpr@27.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (label-break-continue.vpr@28.1) diff --git a/test/viper/ok/label-break-continue.vpr.ok b/test/viper/ok/label-break-continue.vpr.ok index 3f4c45054cf..73e3ca29213 100644 --- a/test/viper/ok/label-break-continue.vpr.ok +++ b/test/viper/ok/label-break-continue.vpr.ok @@ -22,14 +22,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true) diff --git a/test/viper/ok/lits.silicon.ok b/test/viper/ok/lits.silicon.ok index c78e9d4f25c..28c575f027b 100644 --- a/test/viper/ok/lits.silicon.ok +++ b/test/viper/ok/lits.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (lits.vpr@33.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (lits.vpr@34.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (lits.vpr@25.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (lits.vpr@26.1) diff --git a/test/viper/ok/lits.vpr.ok b/test/viper/ok/lits.vpr.ok index d8182ea500d..74a85bd7e90 100644 --- a/test/viper/ok/lits.vpr.ok +++ b/test/viper/ok/lits.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true) diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok index 83b68ad826e..b2405dd8f09 100644 --- a/test/viper/ok/loop-invariant.silicon.ok +++ b/test/viper/ok/loop-invariant.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (loop-invariant.vpr@33.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (loop-invariant.vpr@34.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (loop-invariant.vpr@25.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (loop-invariant.vpr@26.1) diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok index 13967df69b9..8f2e3fd58eb 100644 --- a/test/viper/ok/loop-invariant.vpr.ok +++ b/test/viper/ok/loop-invariant.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true) diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok index 73b9e5cc757..1f0439b0749 100644 --- a/test/viper/ok/method-call.silicon.ok +++ b/test/viper/ok/method-call.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (method-call.vpr@34.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (method-call.vpr@26.1) diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok index ff1a6c5e01f..04a82c80f2f 100644 --- a/test/viper/ok/method-call.vpr.ok +++ b/test/viper/ok/method-call.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) ((true && acc(($Self).boolFld,write))) diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok index f0e971fad6b..7fd1f0023d5 100644 --- a/test/viper/ok/nats.silicon.ok +++ b/test/viper/ok/nats.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@34.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@26.1) diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok index 3409f8c3549..19039b4b400 100644 --- a/test/viper/ok/nats.vpr.ok +++ b/test/viper/ok/nats.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) ((true && acc(($Self).x,write))) diff --git a/test/viper/ok/odd-even.silicon.ok b/test/viper/ok/odd-even.silicon.ok index 8ff9203ce20..557a3a1d5a6 100644 --- a/test/viper/ok/odd-even.silicon.ok +++ b/test/viper/ok/odd-even.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (odd-even.vpr@33.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (odd-even.vpr@34.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (odd-even.vpr@25.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (odd-even.vpr@26.1) diff --git a/test/viper/ok/odd-even.vpr.ok b/test/viper/ok/odd-even.vpr.ok index e3985b7cc3c..9c2f401dec4 100644 --- a/test/viper/ok/odd-even.vpr.ok +++ b/test/viper/ok/odd-even.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true) diff --git a/test/viper/ok/option.silicon.ok b/test/viper/ok/option.silicon.ok index 06f7bb55f45..597ebacdb40 100644 --- a/test/viper/ok/option.silicon.ok +++ b/test/viper/ok/option.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (option.vpr@34.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (option.vpr@26.1) diff --git a/test/viper/ok/option.vpr.ok b/test/viper/ok/option.vpr.ok index 823b20cdf3a..c91a72d9209 100644 --- a/test/viper/ok/option.vpr.ok +++ b/test/viper/ok/option.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write))) diff --git a/test/viper/ok/polymono.silicon.ok b/test/viper/ok/polymono.silicon.ok index 94592a8ba3d..14f6ae0e596 100644 --- a/test/viper/ok/polymono.silicon.ok +++ b/test/viper/ok/polymono.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (polymono.vpr@33.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (polymono.vpr@34.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (polymono.vpr@25.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (polymono.vpr@26.1) diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok index 686a90c4c5b..49f4d496952 100644 --- a/test/viper/ok/polymono.vpr.ok +++ b/test/viper/ok/polymono.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true) diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok index 1ffb7653123..0dfe28e119c 100644 --- a/test/viper/ok/private.vpr.ok +++ b/test/viper/ok/private.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write))) diff --git a/test/viper/ok/reverse.silicon.ok b/test/viper/ok/reverse.silicon.ok index 91ec44fa1b0..68016479b83 100644 --- a/test/viper/ok/reverse.silicon.ok +++ b/test/viper/ok/reverse.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (reverse.vpr@37.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (reverse.vpr@30.1) diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok index 744becfd334..f58275916ba 100644 --- a/test/viper/ok/reverse.vpr.ok +++ b/test/viper/ok/reverse.vpr.ok @@ -21,13 +21,6 @@ adt Option[T] { function $concat(a: Int, b: Int): Int /* Typed references */ field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) ((true && (acc(($Self).xarray,write) && ($array_acc( diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok index 79eb777979e..2ddee151b59 100644 --- a/test/viper/ok/simple-funs.silicon.ok +++ b/test/viper/ok/simple-funs.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (simple-funs.vpr@33.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@34.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (simple-funs.vpr@25.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@26.1) diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok index d79fba5dff3..39901ba9537 100644 --- a/test/viper/ok/simple-funs.vpr.ok +++ b/test/viper/ok/simple-funs.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true) diff --git a/test/viper/ok/text.silicon.ok b/test/viper/ok/text.silicon.ok index 636bc465cdc..0cae47913c0 100644 --- a/test/viper/ok/text.silicon.ok +++ b/test/viper/ok/text.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (text.vpr@35.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (text.vpr@28.1) diff --git a/test/viper/ok/text.vpr.ok b/test/viper/ok/text.vpr.ok index 0b54cb5b5e8..a8642086106 100644 --- a/test/viper/ok/text.vpr.ok +++ b/test/viper/ok/text.vpr.ok @@ -22,13 +22,6 @@ adt Option[T] { function $concat(a: Int, b: Int): Int /* Typed references */ field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write))) @@ -62,13 +55,13 @@ method array_text($Self: Ref) requires $Perm($Self) ensures $Perm($Self) { var arr: Array - inhale $array_acc(arr, $text, write); + inhale $array_acc(arr, $int, write); inhale ($size(arr) == 2); - ($loc(arr, 0)).$text := 2; - ($loc(arr, 1)).$text := 2; - ($loc(arr, 0)).$text := 0; - ($loc(arr, 1)).$text := 1; - assert ((($loc(arr, 0)).$text == 0) && (($loc(arr, 1)).$text == 1)); + ($loc(arr, 0)).$int := 2; + ($loc(arr, 1)).$int := 2; + ($loc(arr, 0)).$int := 0; + ($loc(arr, 1)).$int := 1; + assert ((($loc(arr, 0)).$int == 0) && (($loc(arr, 1)).$int == 1)); label $Ret; } method tuple_text($Self: Ref) diff --git a/test/viper/ok/tuple.silicon.ok b/test/viper/ok/tuple.silicon.ok index 5662a29c2d5..da7cd2acc23 100644 --- a/test/viper/ok/tuple.silicon.ok +++ b/test/viper/ok/tuple.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (tuple.vpr@39.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (tuple.vpr@31.1) diff --git a/test/viper/ok/tuple.vpr.ok b/test/viper/ok/tuple.vpr.ok index 8b3a614c418..4f0152fc9a5 100644 --- a/test/viper/ok/tuple.vpr.ok +++ b/test/viper/ok/tuple.vpr.ok @@ -25,14 +25,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write))) diff --git a/test/viper/ok/variants.silicon.ok b/test/viper/ok/variants.silicon.ok index 0d0474b877d..4666b19dbe7 100644 --- a/test/viper/ok/variants.silicon.ok +++ b/test/viper/ok/variants.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (variants.vpr@33.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (variants.vpr@34.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (variants.vpr@25.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (variants.vpr@26.1) diff --git a/test/viper/ok/variants.vpr.ok b/test/viper/ok/variants.vpr.ok index 403b2e27117..e1510ef6fd8 100644 --- a/test/viper/ok/variants.vpr.ok +++ b/test/viper/ok/variants.vpr.ok @@ -20,14 +20,6 @@ adt Option[T] { /* Text encoding */ function $concat(a: Int, b: Int): Int /* Typed references */ -field $int: Int -field $bool: Bool -field $text: Int -field $ref: Ref -field $array: Array -field $option_int: Option[Int] -field $option_bool: Option[Bool] -field $option_array: Option[Array] /* END PRELUDE */ define $Perm($Self) (true)