From cb59b442ee14c53cf75d23e75f801a153d9ef825 Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Thu, 10 Oct 2024 00:30:22 -0700 Subject: [PATCH] check use of variable in spec by default in live analysis --- .../pipeline/livevar_analysis_processor.rs | 20 +-- .../tests/file-format-generator/bug_14762.exp | 114 ++++++++++++++++++ .../file-format-generator/bug_14762.move | 54 +++++++++ .../file-format-generator/bug_14762.opt.exp | 100 +++++++++++++++ .../tests/no-v1-comparison/bug_14762.exp | 1 + .../tests/no-v1-comparison/bug_14762.move | 79 ++++++++++++ .../functional/ModifiesErrorTest.v2_exp | 60 --------- .../sources/functional/ModifiesTest.v2_exp | 11 -- .../tests/sources/functional/bitset.v2_exp | 11 -- .../functional/bitwise_features.v2_exp | 5 - .../tests/sources/functional/bug_14762.exp | 9 ++ .../tests/sources/functional/bug_14762.move | 69 +++++++++++ .../sources/functional/inline-lambda.v2_exp | 12 -- .../functional/inline_fun_simple.v2_exp | 24 ---- .../functional/loops_with_memory_ops.v2_exp | 1 - .../sources/functional/specs_in_fun.v2_exp | 24 ---- .../functional/specs_in_fun_ref.v2_exp | 29 ----- .../functional/verify_custom_table.v2_exp | 12 -- .../tests/sources/regression/bug_828.v2_exp | 5 - 19 files changed, 439 insertions(+), 201 deletions(-) create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move delete mode 100644 third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp delete mode 100644 third_party/move/move-prover/tests/sources/functional/bitset.v2_exp delete mode 100644 third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp create mode 100644 third_party/move/move-prover/tests/sources/functional/bug_14762.exp create mode 100644 third_party/move/move-prover/tests/sources/functional/bug_14762.move delete mode 100644 third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp delete mode 100644 third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp diff --git a/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs b/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs index 36e22429ee40a..c888d9e67bec2 100644 --- a/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs +++ b/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs @@ -198,9 +198,7 @@ impl FunctionTargetProcessor for LiveVarAnalysisProcessor { impl LiveVarAnalysisProcessor { /// Create a new instance of live variable analysis. /// `track_all_usages` determines whether both primary and secondary usages of a variable are - /// tracked (when true), or only the primary usages (when false). Also, if set, all usages - /// of temporaries in specifications are tracked, which are considered as secondary because - /// they are not part of the execution semantics. + /// tracked (when true), or only the primary usages (when false). /// Unless all usages are needed, it is recommended to set `track_all_usages` to false. pub fn new(track_all_usages: bool) -> Self { Self { track_all_usages } @@ -373,14 +371,22 @@ impl<'a> TransferFunctions for LiveVarAnalysis<'a> { Branch(id, _, _, src) => { state.insert_or_update(*src, self.livevar_info(id, offset), self.track_all_usages); }, - Prop(id, _, exp) if self.track_all_usages => { + Prop(id, _, exp) => { for idx in exp.used_temporaries() { - state.insert_or_update(idx, self.livevar_info(id, offset), true); + state.insert_or_update( + idx, + self.livevar_info(id, offset), + self.track_all_usages, + ); } }, - SpecBlock(id, spec) if self.track_all_usages => { + SpecBlock(id, spec) => { for idx in spec.used_temporaries() { - state.insert_or_update(idx, self.livevar_info(id, offset), true); + state.insert_or_update( + idx, + self.livevar_info(id, offset), + self.track_all_usages, + ); } }, _ => {}, diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp new file mode 100644 index 0000000000000..9d0f6f655fbc9 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp @@ -0,0 +1,114 @@ + +============ disassembled file-format ================== +// Move bytecode v7 +module c0ffee.m { +use 0000000000000000000000000000000000000000000000000000000000000001::option; +use 0000000000000000000000000000000000000000000000000000000000000001::vector; + + +struct T has copy, drop, store { + issuer: vector, + version: u64 +} +struct J has copy, drop, store { + variant: u64 +} +struct S has copy, drop, store { + entries: vector +} + +test(Arg0: &mut S, Arg1: vector): Option /* def_idx: 0 */ { +L2: loc0: &vector +L3: loc1: bool +L4: loc2: u64 +L5: loc3: u64 +L6: loc4: u64 +L7: loc5: &T +L8: loc6: &T +L9: loc7: u64 +L10: loc8: bool +L11: loc9: u64 +L12: loc10: Option +L13: loc11: Option +B0: + 0: CopyLoc[0](Arg0: &mut S) + 1: ImmBorrowField[0](S.entries: vector) + 2: StLoc[2](loc0: &vector) + 3: LdFalse + 4: StLoc[3](loc1: bool) + 5: LdU64(0) + 6: StLoc[4](loc2: u64) + 7: LdU64(0) + 8: CopyLoc[2](loc0: &vector) + 9: VecLen(2) + 10: StLoc[5](loc3: u64) + 11: StLoc[6](loc4: u64) +B1: + 12: CopyLoc[6](loc4: u64) + 13: CopyLoc[5](loc3: u64) + 14: Lt + 15: BrFalse(41) +B2: + 16: CopyLoc[2](loc0: &vector) + 17: CopyLoc[6](loc4: u64) + 18: VecImmBorrow(2) + 19: StLoc[7](loc5: &T) + 20: MoveLoc[7](loc5: &T) + 21: StLoc[8](loc6: &T) + 22: MoveLoc[8](loc6: &T) + 23: ImmBorrowField[1](T.issuer: vector) + 24: ReadRef + 25: CopyLoc[1](Arg1: vector) + 26: Eq + 27: BrFalse(34) +B3: + 28: LdTrue + 29: StLoc[3](loc1: bool) + 30: MoveLoc[6](loc4: u64) + 31: StLoc[4](loc2: u64) + 32: Branch(43) +B4: + 33: Branch(34) +B5: + 34: LdU64(1) + 35: StLoc[9](loc7: u64) + 36: MoveLoc[6](loc4: u64) + 37: MoveLoc[9](loc7: u64) + 38: Add + 39: StLoc[6](loc4: u64) + 40: Branch(42) +B6: + 41: Branch(43) +B7: + 42: Branch(12) +B8: + 43: Nop + 44: MoveLoc[2](loc0: &vector) + 45: Pop + 46: MoveLoc[3](loc1: bool) + 47: StLoc[10](loc8: bool) + 48: MoveLoc[4](loc2: u64) + 49: StLoc[11](loc9: u64) + 50: MoveLoc[10](loc8: bool) + 51: BrFalse(59) +B9: + 52: MoveLoc[0](Arg0: &mut S) + 53: MutBorrowField[0](S.entries: vector) + 54: MoveLoc[11](loc9: u64) + 55: Call vector::remove(&mut vector, u64): T + 56: Call option::some(T): Option + 57: StLoc[12](loc10: Option) + 58: Branch(63) +B10: + 59: MoveLoc[0](Arg0: &mut S) + 60: Pop + 61: Call option::none(): Option + 62: StLoc[12](loc10: Option) +B11: + 63: MoveLoc[12](loc10: Option) + 64: StLoc[13](loc11: Option) + 65: MoveLoc[13](loc11: Option) + 66: Ret +} +} +============ bytecode verification succeeded ======== diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move new file mode 100644 index 0000000000000..687c39ecd04be --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move @@ -0,0 +1,54 @@ +module 0xc0ffee::m { + use std::vector; + use std::option; + use std::option::Option; + + struct J has copy, drop, store { + variant: u64, + } + + + struct T has copy, drop, store { + issuer: vector, + version: u64, + } + + struct S has copy, drop, store { + entries: vector, + } + + public inline fun find(v: &vector, f: |&Element|bool): (bool, u64) { + let find = false; + let found_index = 0; + let i = 0; + let len = vector::length(v); + while (i < len) { + if (f(vector::borrow(v, i))) { + find = true; + found_index = i; + break + }; + i = i + 1; + }; + spec { + assert find ==> f(v[found_index]); + }; + (find, found_index) + } + + fun test(s: &mut S, issuer: vector): Option { + let (found, index) = find(&s.entries, |obj| { + let set: &T = obj; + set.issuer == issuer + }); + + let ret = if (found) { + option::some(vector::remove(&mut s.entries, index)) + } else { + option::none() + }; + + ret + } + +} diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp new file mode 100644 index 0000000000000..cce956293c50f --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp @@ -0,0 +1,100 @@ + +============ disassembled file-format ================== +// Move bytecode v7 +module c0ffee.m { +use 0000000000000000000000000000000000000000000000000000000000000001::option; +use 0000000000000000000000000000000000000000000000000000000000000001::vector; + + +struct T has copy, drop, store { + issuer: vector, + version: u64 +} +struct J has copy, drop, store { + variant: u64 +} +struct S has copy, drop, store { + entries: vector +} + +test(Arg0: &mut S, Arg1: vector): Option /* def_idx: 0 */ { +L2: loc0: &vector +L3: loc1: bool +L4: loc2: u64 +L5: loc3: u64 +L6: loc4: u64 +L7: loc5: bool +L8: loc6: u64 +L9: loc7: Option +L10: loc8: Option +B0: + 0: CopyLoc[0](Arg0: &mut S) + 1: ImmBorrowField[0](S.entries: vector) + 2: StLoc[2](loc0: &vector) + 3: LdFalse + 4: StLoc[3](loc1: bool) + 5: LdU64(0) + 6: StLoc[4](loc2: u64) + 7: LdU64(0) + 8: StLoc[5](loc3: u64) + 9: CopyLoc[2](loc0: &vector) + 10: VecLen(2) + 11: StLoc[6](loc4: u64) +B1: + 12: CopyLoc[5](loc3: u64) + 13: CopyLoc[6](loc4: u64) + 14: Lt + 15: BrFalse(28) +B2: + 16: CopyLoc[2](loc0: &vector) + 17: CopyLoc[5](loc3: u64) + 18: VecImmBorrow(2) + 19: ImmBorrowField[1](T.issuer: vector) + 20: ReadRef + 21: CopyLoc[1](Arg1: vector) + 22: Eq + 23: BrFalse(52) +B3: + 24: LdTrue + 25: StLoc[3](loc1: bool) + 26: MoveLoc[5](loc3: u64) + 27: StLoc[4](loc2: u64) +B4: + 28: Nop + 29: MoveLoc[2](loc0: &vector) + 30: Pop + 31: MoveLoc[3](loc1: bool) + 32: StLoc[7](loc5: bool) + 33: MoveLoc[4](loc2: u64) + 34: StLoc[8](loc6: u64) + 35: MoveLoc[7](loc5: bool) + 36: BrFalse(47) +B5: + 37: MoveLoc[0](Arg0: &mut S) + 38: MutBorrowField[0](S.entries: vector) + 39: MoveLoc[8](loc6: u64) + 40: Call vector::remove(&mut vector, u64): T + 41: Call option::some(T): Option + 42: StLoc[9](loc7: Option) +B6: + 43: MoveLoc[9](loc7: Option) + 44: StLoc[10](loc8: Option) + 45: MoveLoc[10](loc8: Option) + 46: Ret +B7: + 47: MoveLoc[0](Arg0: &mut S) + 48: Pop + 49: Call option::none(): Option + 50: StLoc[9](loc7: Option) + 51: Branch(43) +B8: + 52: LdU64(1) + 53: StLoc[8](loc6: u64) + 54: MoveLoc[5](loc3: u64) + 55: MoveLoc[8](loc6: u64) + 56: Add + 57: StLoc[5](loc3: u64) + 58: Branch(12) +} +} +============ bytecode verification succeeded ======== diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp new file mode 100644 index 0000000000000..5d92c423f3fd8 --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp @@ -0,0 +1 @@ +processed 2 tasks diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move new file mode 100644 index 0000000000000..eede6c62f227f --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move @@ -0,0 +1,79 @@ +//# publish +module 0x42::m { + use std::vector; + use std::option; + use std::option::Option; + + struct J has copy, drop, store { + variant: u64, + } + + struct T has copy, drop, store { + issuer: vector, + version: u64, + } + + struct S has copy, drop, store { + entries: vector, + } + + public inline fun find(v: &vector, f: |&Element|bool): (bool, u64) { + let find = false; + let found_index = 0; + let i = 0; + let len = vector::length(v); + while (i < len) { + if (f(vector::borrow(v, i))) { + find = true; + found_index = i; + break + }; + i = i + 1; + }; + spec { + assert find ==> f(v[found_index]); + }; + (find, found_index) + } + + fun test(s: &mut S, issuer: vector): Option { + let (found, index) = find(&s.entries, |obj| { + let set: &T = obj; + set.issuer == issuer + }); + + let ret = if (found) { + option::some(vector::remove(&mut s.entries, index)) + } else { + option::none() + }; + + ret + } + + fun test1() { + let t0 = T { + issuer: vector[1], + version: 1 + }; + let t1 = T { + issuer: vector[2], + version: 0 + }; + let s = S { + entries: vector[t0, t1] + }; + let opt_t = test(&mut s, vector[0]); + assert!(option::is_none(&opt_t), 0); + let opt_t = test(&mut s, vector[1]); + assert!(option::is_some(&opt_t), 0); + assert!(option::borrow(&opt_t).issuer == vector[1], 0); + let opt_t = test(&mut s, vector[2]); + assert!(option::is_some(&opt_t), 0); + assert!(option::borrow(&opt_t).issuer == vector[2], 0); + + } + +} + +//# run 0x42::m::test1 diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp index a4c827857f788..620e4ee6a4e64 100644 --- a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp @@ -1,64 +1,4 @@ Move prover returns: exiting with verification errors -warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0` - ┌─ tests/sources/functional/ModifiesErrorTest.move:37:18 - │ -37 │ let x0 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1` - ┌─ tests/sources/functional/ModifiesErrorTest.move:40:18 - │ -40 │ let x1 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0` - ┌─ tests/sources/functional/ModifiesErrorTest.move:51:18 - │ -51 │ let x0 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1` - ┌─ tests/sources/functional/ModifiesErrorTest.move:53:18 - │ -53 │ let x1 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0` - ┌─ tests/sources/functional/ModifiesErrorTest.move:64:18 - │ -64 │ let x0 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1` - ┌─ tests/sources/functional/ModifiesErrorTest.move:66:18 - │ -66 │ let x1 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0` - ┌─ tests/sources/functional/ModifiesErrorTest.move:78:18 - │ -78 │ let x0 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1` - ┌─ tests/sources/functional/ModifiesErrorTest.move:80:18 - │ -80 │ let x1 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0` - ┌─ tests/sources/functional/ModifiesErrorTest.move:91:18 - │ -91 │ let x0 = A::read_at(addr); - │ ^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1` - ┌─ tests/sources/functional/ModifiesErrorTest.move:93:18 - │ -93 │ let x1 = A::read_at(addr); - │ ^^^^^^^^^^^^^^^^ - error: caller does not have permission to modify `B::T` at given address ┌─ tests/sources/functional/ModifiesErrorTest.move:38:17 │ diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp deleted file mode 100644 index 66abe10c08bf4..0000000000000 --- a/third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp +++ /dev/null @@ -1,11 +0,0 @@ -warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0` - ┌─ tests/sources/functional/ModifiesTest.move:67:18 - │ -67 │ let x0 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1` - ┌─ tests/sources/functional/ModifiesTest.move:69:18 - │ -69 │ let x1 = A::read_at(addr2); - │ ^^^^^^^^^^^^^^^^^ diff --git a/third_party/move/move-prover/tests/sources/functional/bitset.v2_exp b/third_party/move/move-prover/tests/sources/functional/bitset.v2_exp deleted file mode 100644 index e50ba75b20d2e..0000000000000 --- a/third_party/move/move-prover/tests/sources/functional/bitset.v2_exp +++ /dev/null @@ -1,11 +0,0 @@ -warning: Unused assignment to `s2`. Consider removing or prefixing with an underscore: `_s2` - ┌─ tests/sources/functional/bitset.move:59:18 - │ -59 │ let s2 = intersect(s, s); - │ ^^^^^^^^^^^^^^^ - -warning: Unused assignment to `s3`. Consider removing or prefixing with an underscore: `_s3` - ┌─ tests/sources/functional/bitset.move:60:18 - │ -60 │ let s3 = union(s, s); - │ ^^^^^^^^^^^ diff --git a/third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp b/third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp deleted file mode 100644 index 7c523ceea6767..0000000000000 --- a/third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp +++ /dev/null @@ -1,5 +0,0 @@ -warning: Unused assignment to `old_features`. Consider removing or prefixing with an underscore: `_old_features` - ┌─ tests/sources/functional/bitwise_features.move:50:28 - │ -50 │ let old_features = *features; // ghost var - │ ^^^^^^^^^ diff --git a/third_party/move/move-prover/tests/sources/functional/bug_14762.exp b/third_party/move/move-prover/tests/sources/functional/bug_14762.exp new file mode 100644 index 0000000000000..4b2683e417420 --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/bug_14762.exp @@ -0,0 +1,9 @@ +Move prover returns: exiting with model building errors +error: invalid transfer of references + ┌─ tests/sources/functional/bug_14762.move:45:26 + │ +39 │ let (found, index) = find(&s.entries, |obj| { + │ ---------- It is still being borrowed by this reference + · +45 │ option::some(vector::remove(&mut s.entries, index)) + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Invalid usage of reference as function argument. Cannot transfer a mutable reference that is being borrowed diff --git a/third_party/move/move-prover/tests/sources/functional/bug_14762.move b/third_party/move/move-prover/tests/sources/functional/bug_14762.move new file mode 100644 index 0000000000000..b1e1587553120 --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/bug_14762.move @@ -0,0 +1,69 @@ +module 0x42::m { + use std::vector; + use std::option; + use std::option::Option; + + struct J has copy, drop, store { + variant: u64, + } + + struct T has copy, drop, store { + issuer: vector, + version: u64, + } + + struct S has copy, drop, store { + entries: vector, + } + + public inline fun find(v: &vector, f: |&Element|bool): (bool, u64) { + let find = false; + let found_index = 0; + let i = 0; + let len = vector::length(v); + while (i < len) { + if (f(vector::borrow(v, i))) { + find = true; + found_index = i; + break + }; + i = i + 1; + }; + spec { + assert find ==> f(v[found_index]); + }; + (find, found_index) + } + + fun test(s: &mut S, issuer: vector): Option { + let (found, index) = find(&s.entries, |obj| { + let set: &T = obj; + set.issuer == issuer + }); + + let ret = if (found) { + option::some(vector::remove(&mut s.entries, index)) + } else { + option::none() + }; + + ret + } + + fun test1() { + let t0 = T { + issuer: vector[1], + version: 1 + }; + let t1 = T { + issuer: vector[2], + version: 0 + }; + let s = S { + entries: vector[t0, t1] + }; + let _opt_t = test(&mut s, vector[0]); + + } + +} diff --git a/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp b/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp index a939ef7f0c9c6..4d220149d9a54 100644 --- a/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp @@ -1,16 +1,4 @@ Move prover returns: exiting with verification errors -warning: Unused assignment to `r1`. Consider removing or prefixing with an underscore: `_r1` - ┌─ tests/sources/functional/inline-lambda.move:11:31 - │ -11 │ let r1 = apply(0, |v| v >= 0); - │ ^^^^^^ - -warning: Unused assignment to `r2`. Consider removing or prefixing with an underscore: `_r2` - ┌─ tests/sources/functional/inline-lambda.move:16:31 - │ -16 │ let r2 = apply(0, |v| v != a1 + a2); - │ ^^^^^^^^^^^^ - error: unknown assertion failed ┌─ tests/sources/functional/inline-lambda.move:5:13 │ diff --git a/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp b/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp index a71d8eee327fb..00f90006edacb 100644 --- a/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp @@ -1,28 +1,4 @@ Move prover returns: exiting with verification errors -warning: Unused assignment to `r1`. Consider removing or prefixing with an underscore: `_r1` - ┌─ tests/sources/functional/inline_fun_simple.move:10:32 - │ -10 │ let r1 = apply(42, |v| v >= 1); - │ ^^^^^^ - -warning: Unused assignment to `r2`. Consider removing or prefixing with an underscore: `_r2` - ┌─ tests/sources/functional/inline_fun_simple.move:15:32 - │ -15 │ let r2 = apply(43, |v| v <= 2); - │ ^^^^^^ - -warning: Unused assignment to `r1`. Consider removing or prefixing with an underscore: `_r1` - ┌─ tests/sources/functional/inline_fun_simple.move:22:32 - │ -22 │ let r1 = apply(42, |v| v >= 1); - │ ^^^^^^ - -warning: Unused assignment to `r2`. Consider removing or prefixing with an underscore: `_r2` - ┌─ tests/sources/functional/inline_fun_simple.move:27:31 - │ -27 │ let r2 = apply(3, |v| v <= 2); - │ ^^^^^^ - error: unknown assertion failed ┌─ tests/sources/functional/inline_fun_simple.move:4:13 │ diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp index 00ce62137346b..4da1a9c4977ce 100644 --- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp @@ -42,7 +42,6 @@ error: induction case of the loop invariant does not hold = at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = a = - = b = = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2 = = diff --git a/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp b/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp index a41ce4e659842..4dc5d49a730b3 100644 --- a/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp @@ -1,28 +1,4 @@ Move prover returns: exiting with verification errors -warning: Unused assignment to `y`. Consider removing or prefixing with an underscore: `_y` - ┌─ tests/sources/functional/specs_in_fun.move:18:9 - │ -18 │ y = x + 1; - │ ^^^^^^^^^ - -warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z` - ┌─ tests/sources/functional/specs_in_fun.move:33:9 - │ -33 │ z = x + y; - │ ^^^^^^^^^ - -warning: Unused assignment to `y`. Consider removing or prefixing with an underscore: `_y` - ┌─ tests/sources/functional/specs_in_fun.move:51:9 - │ -51 │ y = x + 1; - │ ^^^^^^^^^ - -warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z` - ┌─ tests/sources/functional/specs_in_fun.move:66:9 - │ -66 │ z = x + y; - │ ^^^^^^^^^ - error: unknown assertion failed ┌─ tests/sources/functional/specs_in_fun.move:45:13 │ diff --git a/third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp b/third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp deleted file mode 100644 index a7c557355adc9..0000000000000 --- a/third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp +++ /dev/null @@ -1,29 +0,0 @@ -warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z` - ┌─ tests/sources/functional/specs_in_fun_ref.move:11:9 - │ -11 │ z = x + y; - │ ^^^^^^^^^ - -warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z` - ┌─ tests/sources/functional/specs_in_fun_ref.move:44:9 - │ -44 │ z = *x + *y; - │ ^^^^^^^^^^^ - -warning: Unused assignment to `vx`. Consider removing or prefixing with an underscore: `_vx` - ┌─ tests/sources/functional/specs_in_fun_ref.move:45:18 - │ -45 │ let vx = *x; - │ ^^ - -warning: Unused assignment to `vy`. Consider removing or prefixing with an underscore: `_vy` - ┌─ tests/sources/functional/specs_in_fun_ref.move:46:18 - │ -46 │ let vy = *y; - │ ^^ - -warning: Unused assignment to `fx`. Consider removing or prefixing with an underscore: `_fx` - ┌─ tests/sources/functional/specs_in_fun_ref.move:47:18 - │ -47 │ let fx = freeze(x); - │ ^^^^^^^^^ diff --git a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp index 53156854c8c86..a859dc99038f4 100644 --- a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp @@ -1,16 +1,4 @@ Move prover returns: exiting with verification errors -warning: Unused assignment to `k`. Consider removing or prefixing with an underscore: `_k` - ┌─ tests/sources/functional/verify_custom_table.move:115:22 - │ -115 │ let (k, v) = table::remove_return_key(&mut t, 2); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: Unused assignment to `v`. Consider removing or prefixing with an underscore: `_v` - ┌─ tests/sources/functional/verify_custom_table.move:115:22 - │ -115 │ let (k, v) = table::remove_return_key(&mut t, 2); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - error: post-condition does not hold ┌─ tests/sources/functional/verify_custom_table.move:76:9 │ diff --git a/third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp b/third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp deleted file mode 100644 index 1632a07cecacd..0000000000000 --- a/third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp +++ /dev/null @@ -1,5 +0,0 @@ -warning: Unused assignment to `old_i`. Consider removing or prefixing with an underscore: `_old_i` - ┌─ tests/sources/regression/bug_828.move:4:21 - │ -4 │ let old_i = i; - │ ^