Skip to content
Permalink

Comparing changes

This is a direct comparison between two commits made in this repository or its related repositories. View the default comparison for this range or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: aptos-labs/aptos-core
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: c06c4080e434ef41ebf0e1c9fa20f4b82faef8f3
Choose a base ref
..
head repository: aptos-labs/aptos-core
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 6142f77448d6b2763b6d3025bfca2eea522439a6
Choose a head ref
Showing with 4 additions and 2 deletions.
  1. +4 −2 third_party/move/move-prover/tests/sources/functional/abort_in_fun.move
Original file line number Diff line number Diff line change
@@ -82,7 +82,7 @@ module 0x42::TestAbortInFunction {
pragma bv=b"0";
}

fun call_abort_generic_struct_concrete(x: u64, y: u64): T {
fun call_abort_generic_struct_concrete(x: u64, y: u64, test_assert1: bool): T {
let sx = S {
value: T {
v: x
@@ -93,12 +93,14 @@ module 0x42::TestAbortInFunction {
v: y
}
};
assert!(test_assert1, 0);
abort_generic_struct(sx, sy).value
}

spec call_abort_generic_struct_concrete {
aborts_if x == y;
ensures result == call_abort_generic_struct_concrete(x, y);
aborts_if !test_assert1;
ensures result == call_abort_generic_struct_concrete(x, y, test_assert1);
ensures result == spec_call_abort_generic_struct_concrete(x, y);
}