Skip to content

Commit 9416fda

Browse files
adpaco-awstedinski
authored andcommitted
Add a test for breakpoint (rust-lang#1022)
* Add a test for `breakpoint` * Convert into an `expected` test * Update comment on test
1 parent 212c5da commit 9416fda

File tree

2 files changed

+14
-0
lines changed

2 files changed

+14
-0
lines changed
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
SUCCESS\
2+
assertion failed: true
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Check that `breakpoint` is supported (generates a `SKIP` statement)
5+
// and that the assertion after `breakpoint` continues to be reachable
6+
#![feature(core_intrinsics)]
7+
8+
#[kani::proof]
9+
fn main() {
10+
unsafe { std::intrinsics::breakpoint() };
11+
assert!(true);
12+
}

0 commit comments

Comments
 (0)