Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rmc-docs/src/install-guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ Create a test file:

```rust
// File: test.rs
pub fn main() {
fn main() {
assert!(1 == 2);
}
```
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/allocation/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ fn foo() -> Option<i32> {
None
}

pub fn main() {
fn main() {
assert!(foo() == None);
let x = foo();
let y: Option<i32> = None;
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/array/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ fn foo(x: [i32; 5]) -> [i32; 2] {
[x[0], x[1]]
}

pub fn main() {
fn main() {
let x = [1, 2, 3, 4, 5];
let y = foo(x);
let z = 2;
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/assert-eq/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
/// "library/std/src/macros.rs line 17 a panicking function core::panicking::panic_fmt is invoked: SUCCESS"
/// https://github.com/model-checking/rmc/issues/13

pub fn main() {
fn main() {
let x = 1;
let y = 2;
assert_eq!(x + 1, y);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/binop/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ fn ibxor_test(a: i32, b: i32, correct: i32, wrong: i32) {
assert!(a ^ b == wrong);
}

pub fn main() {
fn main() {
iadd_test(1, 2, 3, 4);
isub_test(3, 4, -1, 0);
imul_test(5, 6, 30, 60);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/closure/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ where
some_closure(1, 1);
}

pub fn main() {
fn main() {
let mut num: i32 = rmc::nondet();
let y = 2;
if num <= std::i32::MAX - 100 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/closure2/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let x = 2;
let f = |y| x + y;
let z = f(100);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/closure3/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ where
f(10)
}

pub fn main() {
fn main() {
let num: i64 = rmc::nondet();
if num <= std::i64::MAX - 100 {
// avoid overflow
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/comp/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ fn eq2(a: i32, b: i32) {
assert!(a - b < a);
}

pub fn main() {
fn main() {
let a = rmc::nondet();
let b = rmc::nondet();
if a > -400 && a < 100 && b < 200 && b > 0 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/copy/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
use std::ptr;

pub fn main() {
fn main() {
// TODO: make an overlapping set of locations, and check that it does the right thing for the overlapping region too.
// https://github.com/model-checking/rmc/issues/12
let expected_val = 42;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,4 @@
// `--dry-run` causes RMC to print out commands instead of running them
// In `expected` you will find substrings of these commands because the
// concrete paths depend on your working directory.
pub fn main() {}
fn main() {}
2 changes: 1 addition & 1 deletion src/test/expected/dry-run-flag-conflict/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,4 @@
// `--dry-run` causes RMC to print out commands instead of running them
// In `expected` you will find substrings of these commands because the
// concrete paths depend on your working directory.
pub fn main() {}
fn main() {}
2 changes: 1 addition & 1 deletion src/test/expected/dry-run/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
// `--dry-run` causes RMC to print out commands instead of running them
// In `expected` you will find substrings of these commands because the
// concrete paths depend on your working directory.
pub fn main() {}
fn main() {}
2 changes: 1 addition & 1 deletion src/test/expected/dynamic-error-trait/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ impl MemoryMapping {
}
}

pub fn main() {
fn main() {
let mm = MemoryMapping::new(2);
if mm.is_ok() {
let mm = mm.expect("foo");
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/dynamic-trait-static-dispatch/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ impl Foo for Bar {
}

// this example works with static dispatch, so should work also while dynamic dispatch is not yet resolved
pub fn main() {
fn main() {
let bar = Bar {};
assert!(bar.a() == 3);
assert!(bar.b() == 5);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/dynamic-trait/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ fn impl_area(a: impl Shape) -> u32 {
a.area()
}

pub fn main() {
fn main() {
let rec = Rectangle { w: 10, h: 5 };
assert!(rec.vol(3) == 150);
assert!(impl_area(rec.clone()) == 50);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/enum/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ fn b() -> Foo {
Foo::B { x: 30, y: 60.0 }
}

pub fn main() {
fn main() {
let x = a();
match x {
Foo::A(x) => assert!(x == 10),
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/float-nan/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut f: f32 = 2.0;
while f != 0.0 {
f -= 1.0;
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/generics/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ fn wrapped<T>(x: T) -> Foo<T> {
Foo { data: ident(x), i: 0 }
}

pub fn main() {
fn main() {
let x = 10;
let y = wrapped(x);
let z = 20.0;
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/iterator/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut z = 1;
for i in 1..4 {
z *= i;
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/niche/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ fn get_some<'a>(a: &'a i8) -> T<'a> {
Option2::Some((*a, a))
}

pub fn main() {
fn main() {
let x = get_opt();
match x {
Option2::None => {}
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/niche2/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ fn get_b() -> Option<Foo> {
Some(Foo::B([]))
}

pub fn main() {
fn main() {
match get_none() {
None => {}
Some(_) => assert!(false),
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/nondet/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let x: i32 = rmc::nondet();
if (x > -500 && x < 500) {
// x * x - 2 * x + 1 == 4 -> x == -1 || x == 3
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/references/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ impl Foo {
}
}

pub fn main() {
fn main() {
let foo = Foo { a: 2, _b: 3.0 };
let z = foo.get_a();
assert!(z == 2);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/slice/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ fn bar(x: &[i32; 5]) -> &[i32] {
&x[1..4]
}

pub fn main() {
fn main() {
let x = [1, 2, 3, 4, 5];
let y = foo(&x);
let z = bar(&x);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/static-mutable-struct/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ fn mutate_the_thing(nx: i64, ny: i32) {
}
}

pub fn main() {
fn main() {
assert!(foo().x == 12);
assert!(foo().y == 12);
assert!(foo().x == 14);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/static-mutable/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ fn mutate_the_thing(new: i32) {
}
}

pub fn main() {
fn main() {
assert!(10 == foo());
assert!(12 == foo());
mutate_the_thing(10);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/static/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ fn foo() -> i32 {
X
}

pub fn main() {
fn main() {
assert!(10 == foo());
assert!(12 == foo());
}
2 changes: 1 addition & 1 deletion src/test/expected/test1/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut a: i32 = 0;
let mut i: i32 = 10;
while i != 0 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/test2/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut a: i32 = 4;
let mut i = 0;
while a != 1 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/test3/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut a: f32 = 0.0;
let mut i = 10;

Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/test4/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut a = 4;
let mut i = 0;
while a != 1 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/test5/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
// should succeed
assert!(div(4, 2) == 2);
// should fail
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/test6/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ fn add2(a: i32, b: i32) -> f32 {
add(a, b as f32)
}

pub fn main() {
fn main() {
// should succeed: 1 + 1 = 2
assert!(add2(1, 1) == 2.0);
// should fail: 2 + 1 = 3
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/transmute/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let bitpattern = unsafe { std::mem::transmute::<f32, u32>(1.0) };
assert!(bitpattern == 0x3F800000);

Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/unwind_tip/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
//
// In this test, we check that RMC warns the user about unwinding failures
// and makes a recommendation to fix the issue.
pub fn main() {
fn main() {
let mut a: u32 = rmc::nondet();

if a < 1024 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/vec/main.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut x: Vec<i32> = Vec::new();
x.push(10);
assert!(x[0] == 10);
Expand Down
2 changes: 1 addition & 1 deletion src/test/expected/vecdq/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
use std::collections::VecDeque;

pub fn main() {
fn main() {
let x = rmc::nondet();
let y = rmc::nondet();
let mut q: VecDeque<i32> = VecDeque::new();
Expand Down
2 changes: 1 addition & 1 deletion src/test/firecracker/virtio-block-parse/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -322,7 +322,7 @@ fn is_nonzero_pow2(x: u16) -> bool {
unsafe { (x != 0) && ((x & (x - 1)) == 0) }
}

pub fn main() {
fn main() {
let mem = GuestMemoryMmap {};
let queue_size: u16 = rmc::nondet();
if !is_nonzero_pow2(queue_size) {
Expand Down
2 changes: 1 addition & 1 deletion src/test/prusti/100_doors.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut door_open = [false; 10];
for pass in 1..11 {
let mut door = pass;
Expand Down
2 changes: 1 addition & 1 deletion src/test/prusti/Ackermann_function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ fn ack(m: u64, n: u64) -> u64 {
}
}

pub fn main() {
fn main() {
let a = ack(2, 4);
assert!(a == 11);
}
2 changes: 1 addition & 1 deletion src/test/prusti/Binary_search.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ fn get() -> [i32; 11] {
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]
}

pub fn main() {
fn main() {
let x = get();
let y = rmc::nondet();
if 1 <= y && y <= 11 {
Expand Down
2 changes: 1 addition & 1 deletion src/test/prusti/Fibonacci_sequence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ impl Iterator for Fib {
}
}

pub fn main() {
fn main() {
let mut fib = Fib::new();
assert!(fib.nth(10).unwrap() == 55);
}
2 changes: 1 addition & 1 deletion src/test/prusti/Heapsort.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
pub fn main() {
fn main() {
let mut v = [3, 0, 1, 2];
create_heap(&mut v, |x, y| x < y);
assert!(v == [3, 2, 1, 0]);
Expand Down
2 changes: 1 addition & 1 deletion src/test/prusti/Selection_sort.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ fn selection_sort(array: &mut [i32]) {
}
}

pub fn main() {
fn main() {
let mut array = [9, 4, 8, 3];
selection_sort(&mut array);
assert!(array == [3, 4, 8, 9]);
Expand Down
2 changes: 1 addition & 1 deletion src/test/prusti/Tower_of_Hanoi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,6 @@ fn move_(n: i32, from: i32, to: i32, via: i32) {
}
}

pub fn main() {
fn main() {
move_(4, 1, 2, 3);
}
2 changes: 1 addition & 1 deletion src/test/prusti/borrow_first.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ fn foo(vec: &mut Vec<i32>) -> &i32 {
&vec[last]
}

pub fn main() {
fn main() {
let mut v = vec![-1, 2, 3];
let r = foo(&mut v);
assert!(*r > 0);
Expand Down
Loading