Skip to content

Commit

Permalink
test: solution for prover tests
Browse files Browse the repository at this point in the history 
- all `move-prover` test issues are fixed which were caused by changing
 the stdlib/sources location.
  • Loading branch information
@Rqnsom
Rqnsom committed May 21, 2024
1 parent d33762e commit c9db823
Show file tree
Hide file tree
Showing 10 changed files with 58 additions and 57 deletions.
1 change: 1 addition & 0 deletions language/move-prover/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ toml = "0.5.8"

[dev-dependencies]
datatest-stable = "0.1.1"
move-stdlib = { path = "../move-stdlib", features = ["stdlib-bytecode"] }
move-prover-test-utils = { path = "test-utils" }
shell-words = "1.0.0"
walkdir = "2.3.1"
Expand Down
24 changes: 12 additions & 12 deletions language/move-prover/tests/sources/functional/fixed_point_arithm.cvc4_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,11 @@ error: post-condition does not hold
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:102: mul_div_incorrect
= at ../move-stdlib/sources/FixedPoint32.move:150: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:150: get_raw_value
= num = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:151: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:151: get_raw_value
= result = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:152: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:152: get_raw_value
= y_raw_val = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:103: mul_div_incorrect
= z = <redacted>
Expand All @@ -63,11 +63,11 @@ error: post-condition does not hold
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:102: mul_div_incorrect
= at ../move-stdlib/sources/FixedPoint32.move:150: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:150: get_raw_value
= num = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:151: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:151: get_raw_value
= result = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:152: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:152: get_raw_value
= y_raw_val = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:103: mul_div_incorrect
= z = <redacted>
Expand Down Expand Up @@ -129,9 +129,9 @@ error: post-condition does not hold
= at tests/sources/functional/fixed_point_arithm.move:70: multiply_x_1
= x = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:71: multiply_x_1
= at ../move-stdlib/sources/FixedPoint32.move:126
= at ../move-stdlib/sources/FixedPoint32.move:127
= at ../move-stdlib/sources/FixedPoint32.move:128
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:126
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:127
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:128
= at tests/sources/functional/fixed_point_arithm.move:71: multiply_x_1
= result = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:72: multiply_x_1
Expand All @@ -147,9 +147,9 @@ error: post-condition does not hold
= at tests/sources/functional/fixed_point_arithm.move:78: multiply_x_1_incorrect
= x = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:79: multiply_x_1_incorrect
= at ../move-stdlib/sources/FixedPoint32.move:126
= at ../move-stdlib/sources/FixedPoint32.move:127
= at ../move-stdlib/sources/FixedPoint32.move:128
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:126
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:127
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:128
= at tests/sources/functional/fixed_point_arithm.move:79: multiply_x_1_incorrect
= result = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:80: multiply_x_1_incorrect
Expand Down
18 changes: 9 additions & 9 deletions language/move-prover/tests/sources/functional/fixed_point_arithm.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,11 @@ error: post-condition does not hold
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:105: mul_div_incorrect
= at ../move-stdlib/sources/fixed_point32.move:148: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:148: get_raw_value
= num = <redacted>
= at ../move-stdlib/sources/fixed_point32.move:149: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:149: get_raw_value
= result = <redacted>
= at ../move-stdlib/sources/fixed_point32.move:150: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:150: get_raw_value
= y_raw_val = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:106: mul_div_incorrect
= at tests/sources/functional/fixed_point_arithm.move:107: mul_div_incorrect
Expand All @@ -62,11 +62,11 @@ error: post-condition does not hold
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:105: mul_div_incorrect
= at ../move-stdlib/sources/fixed_point32.move:148: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:148: get_raw_value
= num = <redacted>
= at ../move-stdlib/sources/fixed_point32.move:149: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:149: get_raw_value
= result = <redacted>
= at ../move-stdlib/sources/fixed_point32.move:150: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:150: get_raw_value
= y_raw_val = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:106: mul_div_incorrect
= at tests/sources/functional/fixed_point_arithm.move:107: mul_div_incorrect
Expand Down Expand Up @@ -126,9 +126,9 @@ error: post-condition does not hold
= at tests/sources/functional/fixed_point_arithm.move:81: multiply_x_1_incorrect
= x = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:82: multiply_x_1_incorrect
= at ../move-stdlib/sources/fixed_point32.move:124
= at ../move-stdlib/sources/fixed_point32.move:125
= at ../move-stdlib/sources/fixed_point32.move:126
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:124
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:125
= at ../move-stdlib/MoveStdlib/sources/fixed_point32.move:126
= at tests/sources/functional/fixed_point_arithm.move:82: multiply_x_1_incorrect
= result = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:83: multiply_x_1_incorrect
Expand Down
12 changes: 6 additions & 6 deletions language/move-prover/tests/sources/functional/fixed_point_arithm.simplify_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,11 @@ error: post-condition does not hold
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:105: mul_div_incorrect
= at ../move-stdlib/sources/FixedPoint32.move:150: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:150: get_raw_value
= num = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:151: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:151: get_raw_value
= result = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:152: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:152: get_raw_value
= y_raw_val = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:106: mul_div_incorrect
= z = <redacted>
Expand All @@ -63,11 +63,11 @@ error: post-condition does not hold
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:105: mul_div_incorrect
= at ../move-stdlib/sources/FixedPoint32.move:150: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:150: get_raw_value
= num = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:151: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:151: get_raw_value
= result = <redacted>
= at ../move-stdlib/sources/FixedPoint32.move:152: get_raw_value
= at ../move-stdlib/MoveStdlib/sources/FixedPoint32.move:152: get_raw_value
= y_raw_val = <redacted>
= at tests/sources/functional/fixed_point_arithm.move:106: mul_div_incorrect
= z = <redacted>
Expand Down
24 changes: 12 additions & 12 deletions language/move-prover/tests/sources/functional/global_invariants.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,18 +21,18 @@ error: global memory invariant does not hold
= at tests/sources/functional/global_invariants.move:62: remove_R_invalid
= account = <redacted>
= at tests/sources/functional/global_invariants.move:64: remove_R_invalid
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/global_invariants.move:64: remove_R_invalid
= at tests/sources/functional/global_invariants.move:65: remove_R_invalid
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/global_invariants.move:62: remove_R_invalid
= at tests/sources/functional/global_invariants.move:65: remove_R_invalid
= at tests/sources/functional/global_invariants.move:18
Expand All @@ -47,16 +47,16 @@ error: global memory invariant does not hold
= at tests/sources/functional/global_invariants.move:53: remove_S_invalid
= account = <redacted>
= at tests/sources/functional/global_invariants.move:55: remove_S_invalid
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/global_invariants.move:55: remove_S_invalid
= at tests/sources/functional/global_invariants.move:56: remove_S_invalid
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/global_invariants.move:18
6 changes: 3 additions & 3 deletions language/move-prover/tests/sources/functional/is_txn_signer.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,11 @@ error: unknown assertion failed
= at tests/sources/functional/is_txn_signer.move:29: f4_incorrect
= account = <redacted>
= at tests/sources/functional/is_txn_signer.move:30: f4_incorrect
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/is_txn_signer.move:30: f4_incorrect
= at tests/sources/functional/is_txn_signer.move:31: f4_incorrect

Expand Down
6 changes: 3 additions & 3 deletions language/move-prover/tests/sources/functional/resources.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ error: post-condition does not hold
= at tests/sources/functional/resources.move:32: create_resource_incorrect
= account = <redacted>
= at tests/sources/functional/resources.move:33: create_resource_incorrect
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/resources.move:36: create_resource_incorrect
= at tests/sources/functional/resources.move:38: create_resource_incorrect (spec)
= at tests/sources/functional/resources.move:39: create_resource_incorrect (spec)
6 changes: 3 additions & 3 deletions language/move-prover/tests/sources/functional/script_incorrect.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,11 @@ error: abort not covered by any of the `aborts_if` clauses
= at tests/sources/functional/script_provider.move:8: register
= account = <redacted>
= at tests/sources/functional/script_provider.move:9: register
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= at tests/sources/functional/script_provider.move:9: register
= at tests/sources/functional/script_provider.move:10: register
= ABORTED
12 changes: 6 additions & 6 deletions language/move-prover/tests/sources/functional/type_dependent_code.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,11 @@ error: post-condition does not hold
= x = <redacted>
= at tests/sources/functional/type_dependent_code.move:45: test1
= at tests/sources/functional/type_dependent_code.move:46: test1
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= r = <redacted>
= at tests/sources/functional/type_dependent_code.move:47: test1
= at tests/sources/functional/type_dependent_code.move:48: test1
Expand All @@ -77,11 +77,11 @@ error: post-condition does not hold
= t2 = <redacted>
= at tests/sources/functional/type_dependent_code.move:61: test2
= at tests/sources/functional/type_dependent_code.move:62: test2
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= r = <redacted>
= at tests/sources/functional/type_dependent_code.move:63: test2
= at tests/sources/functional/type_dependent_code.move:64: test2
Expand Down
6 changes: 3 additions & 3 deletions language/move-prover/tests/sources/regression/type_param_bug_121721.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ error: global memory invariant does not hold
= ballot_account = <redacted>
= proposal = <redacted>
= at tests/sources/regression/type_param_bug_121721.move:84: create_ballot
= at ../move-stdlib/sources/signer.move:12: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/signer.move:13: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at ../move-stdlib/MoveStdlib/sources/signer.move:14: address_of
= ballot_address = <redacted>
= at tests/sources/regression/type_param_bug_121721.move:86: create_ballot
= at tests/sources/regression/type_param_bug_121721.move:88: create_ballot
Expand Down

0 comments on commit c9db823

Please sign in to comment.