-
Notifications
You must be signed in to change notification settings - Fork 3.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
b2781bf
commit 2c9bf73
Showing
7 changed files
with
161 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
115 changes: 115 additions & 0 deletions
115
third_party/move/move-prover/tests/sources/functional/abort_in_fun.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,115 @@ | ||
| module 0x42::TestAbortInFunction { | ||
|
|
||
| fun aborts_with(x: u64, y: u64): u64 { | ||
| if (x == 1) { | ||
| abort 2 | ||
| } else if (y == 2) { | ||
| abort 3 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
| spec aborts_with { | ||
| aborts_if x == 1 with 2; | ||
| aborts_if y == 2 with 3; | ||
| ensures result == x; | ||
| } | ||
|
|
||
| fun call_aborts_with(): u64 { | ||
| aborts_with(2, 3) | ||
| } | ||
|
|
||
| spec call_aborts_with { | ||
| ensures result == aborts_with(2, 3); | ||
| } | ||
|
|
||
| fun abort_generic<Element: copy + drop>(x: Element, y: Element): Element { | ||
| if (x == y) { | ||
| abort 0 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
|
|
||
| fun call_aborts_generic(): u64 { | ||
| abort_generic(2, 3) | ||
| } | ||
|
|
||
| spec call_aborts_generic { | ||
| ensures result == abort_generic(2, 3); | ||
| } | ||
|
|
||
| struct S<Element: copy + drop> has copy, drop { | ||
| value: Element | ||
| } | ||
|
|
||
| fun abort_generic_struct<Element: copy + drop>(x: S<Element>, y: S<Element>): S<Element> { | ||
| if (x == y) { | ||
| abort 0 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
|
|
||
| fun spec_abort_generic_struct<Element: copy + drop>(x: S<Element>, y: S<Element>): S<Element> { | ||
| if (x == y) { | ||
| abort 0 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
|
|
||
| fun call_abort_generic_struct<Element: copy + drop>(x: Element, y: Element): Element { | ||
| let sx = S { | ||
| value: x | ||
| }; | ||
| let sy = S { | ||
| value: y | ||
| }; | ||
| abort_generic_struct(sx, sy).value | ||
| } | ||
|
|
||
| spec call_abort_generic_struct { | ||
| aborts_if x == y; | ||
| ensures result == call_abort_generic_struct(x, y); | ||
| } | ||
|
|
||
| struct T has copy, drop { | ||
| v: u64 | ||
| } | ||
|
|
||
| fun call_abort_generic_struct_concrete(x: u64, y: u64): T { | ||
| let sx = S { | ||
| value: T { | ||
| v: x | ||
| } | ||
| }; | ||
| let sy = S { | ||
| value: T { | ||
| v: y | ||
| } | ||
| }; | ||
| 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); | ||
| ensures result == spec_call_abort_generic_struct_concrete(x, y); | ||
| } | ||
|
|
||
| spec fun spec_call_abort_generic_struct_concrete(x: u64, y: u64): T { | ||
| let sx = S { | ||
| value: T { | ||
| v: x | ||
| } | ||
| }; | ||
| let sy = S { | ||
| value: T { | ||
| v: y | ||
| } | ||
| }; | ||
| spec_abort_generic_struct(sx, sy).value | ||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters