File tree Expand file tree Collapse file tree 1 file changed +5
-5
lines changed
Expand file tree Collapse file tree 1 file changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -36,11 +36,11 @@ Let Thrust verify that the program is correct. Here, we use `cargo run` in the T
3636``` console
3737$ cargo run -- -Adead_code -C debug-assertions=false gcd.rs && echo ' safe'
3838 Compiling thrust v0.1.0 (/home/coord_e/rust-refinement/thrust)
39- Finished `dev` profile [unoptimized + debuginfo] target(s) in 6.23s
40- Running `target/debug/thrust-rustc -C debug-assertions=false -Adead_code gcd.rs`
39+ Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.08s
40+ Running `target/debug/thrust-rustc -Adead_code - C debug-assertions=false gcd.rs`
4141error: verification error: Unsat
4242
43- error: aborting due to 1 previous error; 2 warnings emitted
43+ error: aborting due to 1 previous error
4444```
4545
4646Thrust says the program is not safe (possible to panic). In fact, we have a bug in our ` gcd ` function:
@@ -59,8 +59,8 @@ Now Thrust verifies the program is actually safe.
5959
6060``` console
6161$ cargo run -- -Adead_code -C debug-assertions=false gcd_fixed.rs && echo ' safe'
62- Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.04s
63- Running `target/debug/thrust-rustc -C debug-assertions=false -Adead_code gcd_fixed .rs`
62+ Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.08s
63+ Running `target/debug/thrust-rustc -Adead_code - C debug-assertions=false gcd .rs`
6464safe
6565```
6666
You can’t perform that action at this time.
0 commit comments