Skip to content

Commit 3467030

Browse files
adpaco-awstedinski
authored andcommitted
Use RMC prelude in all tests (rust-lang#232)
1 parent bd21736 commit 3467030

File tree

66 files changed

+89
-211
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

66 files changed

+89
-211
lines changed

src/test/cbmc/ArithEqualOperators/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let mut a: u32 = __nondet();

src/test/cbmc/ArithOperators/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a: u32 = __nondet();

src/test/cbmc/BinOp_Offset/main_fail.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unreachable!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
pub fn test_offset_in_double_array() {
86
//let table: Vec<Vec<u64>> = Vec::with_capacity(1);

src/test/cbmc/BitwiseArithOperators/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
assert!(3 | 5 == 7);

src/test/cbmc/BitwiseEqualOperators/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let mut x = 0;

src/test/cbmc/Bool-BoolOperators/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
assert!(true);

src/test/cbmc/Cast/from_be_bytes.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use std::convert::TryInto;
4-
fn __nondet<T>() -> T {
5-
unimplemented!()
6-
}
4+
include!("../../rmc-prelude.rs");
75
fn main() {
86
let input: &[u8] = &vec![
97
__nondet(),

src/test/cbmc/EQ-NE/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let x: u32 = __nondet();

src/test/cbmc/FloatingPoint/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
macro_rules! test_floats {
86
($ty:ty) => {

src/test/cbmc/FunctionCall_Ret-NoParam/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a = return_u32();

src/test/cbmc/FunctionCall_Ret-Param/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@
33

44
// cbmc-flags: --unwind 10
55

6-
fn __nondet<T>() -> T {
7-
unimplemented!()
8-
}
6+
include!("../../rmc-prelude.rs");
97

108
fn main() {
119
let x: u32 = __nondet();

src/test/cbmc/IfElseifElse_NonReturning/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a: u32 = __nondet();

src/test/cbmc/IfElseifElse_Returning/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a: u32 = __nondet();

src/test/cbmc/LT-GT-LE-GE/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a: u32 = __nondet();

src/test/cbmc/LoopLoop_NonReturning/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@
33

44
// cbmc-flags: --unwind 10 --unwinding-assertions
55

6-
fn __nondet<T>() -> T {
7-
unimplemented!()
8-
}
6+
include!("../../rmc-prelude.rs");
97

108
fn main() {
119
let mut a: u32 = __nondet();

src/test/cbmc/LoopWhile_NonReturning/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@
33

44
// cbmc-flags: --unwind 11 --unwinding-assertions
55

6-
fn __nondet<T>() -> T {
7-
unimplemented!()
8-
}
6+
include!("../../rmc-prelude.rs");
97

108
fn main() {
119
let mut a: u32 = __nondet();

src/test/cbmc/NondetVectors/bytes.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use std::convert::TryInto;
44

5-
fn __nondet<T>() -> T {
6-
unimplemented!()
7-
}
5+
include!("../../rmc-prelude.rs");
86

97
fn main() {
108
let input: &[u8] = &vec![

src/test/cbmc/NondetVectors/fixme_main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
const FIFO_SIZE: usize = 2;
4-
fn __nondet<T>() -> T {
5-
unimplemented!()
6-
}
4+
include!("../../rmc-prelude.rs");
75

86
fn main() {
97
let len: usize = __nondet();

src/test/cbmc/Pointers_OtherTypes/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let mut x = 1;

src/test/cbmc/SaturatingIntrinsics/fixme_128.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,7 @@
55
#![feature(core_intrinsics)]
66
use std::intrinsics;
77

8-
fn __nondet<T>() -> T {
9-
unimplemented!()
10-
}
8+
include!("../../rmc-prelude.rs");
119

1210
fn main() {
1311
let v: u128 = __nondet();

src/test/cbmc/SaturatingIntrinsics/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@
33
#![feature(core_intrinsics)]
44
use std::intrinsics;
55

6-
fn __nondet<T>() -> T {
7-
unimplemented!()
8-
}
6+
include!("../../rmc-prelude.rs");
97

108
macro_rules! test_saturating_intrinsics {
119
($ty:ty) => {

src/test/cbmc/Scopes_NonReturning/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a: u32 = __nondet();

src/test/cbmc/Scopes_Returning/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let x = { 5 };

src/test/cbmc/Slice/slice_from_raw_fail.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use std::slice;
44

5-
fn __nondet<T>() -> T {
6-
unimplemented!()
7-
}
5+
include!("../../rmc-prelude.rs");
86

97
// From Listing 19-7: Creating a slice from an arbitrary memory location. https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html
108
fn main() {

src/test/cbmc/i32-Unary-/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let a: i32 = __nondet();

src/test/expected/closure/expected

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
resume instruction: SUCCESS
2-
line 22 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
3-
line 22 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
4-
line 22 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
5-
line 27 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
6-
line 27 assertion failed: original_num + 12 == num: SUCCESS
7-
line 27 arithmetic overflow on signed + in var_18 + 12: SUCCESS
2+
line 20 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
3+
line 20 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
4+
line 20 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
5+
line 25 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
6+
line 25 assertion failed: original_num + 12 == num: SUCCESS
7+
line 25 arithmetic overflow on signed + in var_18 + 12: SUCCESS

src/test/expected/closure/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,7 @@ fn call_with_one<F>(mut some_closure: F) -> ()
88
some_closure(1, 1);
99
}
1010

11-
fn __nondet<T>() -> T {
12-
unimplemented!()
13-
}
11+
include!("../../rmc-prelude.rs");
1412

1513
pub fn main() {
1614
let mut num: i32 = __nondet();

src/test/expected/closure3/expected

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
line 18 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
2-
line 19 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS
3-
line 19 assertion failed: num + 10 == y: SUCCESS
1+
line 16 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
2+
line 17 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS
3+
line 17 assertion failed: num + 10 == y: SUCCESS

src/test/expected/closure3/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,7 @@ fn call_with_one<F, T>(f: F) -> T
77
f(10)
88
}
99

10-
fn __nondet<T>() -> T {
11-
unimplemented!()
12-
}
10+
include!("../../rmc-prelude.rs");
1311

1412
pub fn main() {
1513
let num: i64 = __nondet();

src/test/expected/comp/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,7 @@ fn eq2(a: i32, b: i32) {
1212
assert!(a - b < a);
1313
}
1414

15-
fn __nondet<T>() -> T {
16-
unimplemented!()
17-
}
15+
include!("../../rmc-prelude.rs");
1816

1917
fn main() {
2018
let a = __nondet();

src/test/expected/dynamic-error-trait/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use std::io::{self, Read, Write};
44

5-
fn __nondet<T>() -> T {
6-
unimplemented!()
7-
}
5+
include!("../../rmc-prelude.rs");
86

97
type Result<T> = std::result::Result<T, io::Error>;
108

src/test/expected/nondet/expected

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
line 11 attempt to compute `move _12 * move _13`, which would overflow: SUCCESS
2-
line 11 attempt to compute `const 2_i32 * move _16`, which would overflow: SUCCESS
3-
line 11 attempt to compute `move _11 - move _15`, which would overflow: SUCCESS
4-
line 11 attempt to compute `move _10 + const 1_i32`, which would overflow: SUCCESS
5-
line 11 assertion failed: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS
1+
line 9 attempt to compute `move _12 * move _13`, which would overflow: SUCCESS
2+
line 9 attempt to compute `const 2_i32 * move _16`, which would overflow: SUCCESS
3+
line 9 attempt to compute `move _11 - move _15`, which would overflow: SUCCESS
4+
line 9 attempt to compute `move _10 + const 1_i32`, which would overflow: SUCCESS
5+
line 9 assertion failed: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS

src/test/expected/nondet/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
fn __nondet<T>() -> T {
4-
unimplemented!()
5-
}
3+
include!("../../rmc-prelude.rs");
64

75
fn main() {
86
let x: i32 = __nondet();
Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
line 28 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
2-
line 28 arithmetic overflow on unsigned + in self->len + 1: SUCCESS
3-
line 58 assertion failed: a.is_some(): FAILURE
4-
line 59 assertion failed: a.is_none(): FAILURE
5-
line 61 assertion failed: b.is_some(): SUCCESS
6-
line 62 assertion failed: b.is_none(): FAILURE
1+
line 26 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
2+
line 26 arithmetic overflow on unsigned + in self->len + 1: SUCCESS
3+
line 56 assertion failed: a.is_some(): FAILURE
4+
line 57 assertion failed: a.is_none(): FAILURE
5+
line 59 assertion failed: b.is_some(): SUCCESS
6+
line 60 assertion failed: b.is_none(): FAILURE

src/test/expected/replace-hashmap/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,7 @@ use std::collections::HashMap;
55
use std::hash::Hash;
66
use std::collections::hash_map::RandomState;
77
use std::borrow::Borrow;
8-
fn __nondet<T>() -> T {
9-
unimplemented!()
10-
}
8+
include!("../../rmc-prelude.rs");
119

1210
use std::marker::PhantomData;
1311
struct CbmcHashMap<K,V, S=RandomState> {len: usize, _k : PhantomData<K>, _s : PhantomData<S>, last : Option<V>}
Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
line 24 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
2-
line 34 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS
3-
line 53 assertion failed: v.len() == 1: SUCCESS
4-
line 54 assertion failed: v.len() == 11: FAILURE
5-
line 56 assertion failed: p != None: SUCCESS
6-
line 57 assertion failed: p == None: FAILURE
7-
line 58 assertion failed: p == Some(to_push): SUCCESS
8-
line 59 assertion failed: p == Some(not_pushed): FAILURE
1+
line 22 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
2+
line 32 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS
3+
line 51 assertion failed: v.len() == 1: SUCCESS
4+
line 52 assertion failed: v.len() == 11: FAILURE
5+
line 54 assertion failed: p != None: SUCCESS
6+
line 55 assertion failed: p == None: FAILURE
7+
line 56 assertion failed: p == Some(to_push): SUCCESS
8+
line 57 assertion failed: p == Some(not_pushed): FAILURE

src/test/expected/replace-vec/main.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
#![feature(allocator_api)]
44

5-
fn __nondet<T>() -> T {
6-
unimplemented!()
7-
}
5+
include!("../../rmc-prelude.rs");
86

97
use std::marker::PhantomData;
108
use std::alloc::Allocator;

0 commit comments

Comments
 (0)