forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Get rid of skip monomorphizer hack (rust-lang#485) (rust-lang#624)
Remove the hack we added to monomorphizer to skip functions that we were not able to handle. The latest fixes that we added to RMC was enough to allow us to run the monomorphizer as is.
- Loading branch information
Showing
11 changed files
with
75 additions
and
22 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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -8,4 +8,4 @@ | |
mod hooks; | ||
|
||
pub use hooks::{fn_hooks, skip_monomorphize, GotocHooks}; | ||
pub use hooks::{fn_hooks, GotocHooks}; |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
use std::mem; | ||
|
||
pub fn main() { | ||
let mut var1 = rmc::nondet::<i32>(); | ||
let mut var2 = rmc::nondet::<i32>(); | ||
let old_var1 = var1; | ||
unsafe { | ||
assert_eq!(mem::replace(&mut var1, var2), old_var1); | ||
} | ||
assert_eq!(var1, var2); | ||
} |
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,16 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
use std::mem; | ||
|
||
pub fn main() { | ||
let mut var1 = rmc::nondet::<i32>(); | ||
let mut var2 = rmc::nondet::<i32>(); | ||
let old_var1 = var1; | ||
let old_var2 = var2; | ||
unsafe { | ||
mem::swap(&mut var1, &mut var2); | ||
} | ||
assert_eq!(var1, old_var2); | ||
assert_eq!(var2, old_var1); | ||
} |
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,11 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
use std::ptr::read; | ||
|
||
pub fn main() { | ||
let var = 1; | ||
unsafe { | ||
assert_eq!(read(&var), var); | ||
} | ||
} |
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,12 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
use std::ptr::write; | ||
|
||
pub fn main() { | ||
let mut var = 1; | ||
unsafe { | ||
write(&mut var, 10); | ||
} | ||
assert_eq!(var, 10); | ||
} |
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,18 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
#![feature(never_type)] | ||
|
||
/// Test using the never type | ||
pub fn err() -> ! { | ||
panic!("EXPECTED FAIL: Function should always fail"); | ||
} | ||
|
||
// Give an empty main to make rustc happy. | ||
#[no_mangle] | ||
pub fn main() { | ||
let var = rmc::nondet::<i32>(); | ||
if var > 0 { | ||
err(); | ||
} | ||
} |