From 4e61acde4a9174d6a1d1584a29fcffa5bc14244a Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Mon, 30 Dec 2019 18:41:09 +0100
Subject: [PATCH] examples
---
examples/klee_hybrid_test.rs | 4 +++-
examples/register_test.rs | 26 +++++++++++++-------------
examples/vcell_test.rs | 16 +---------------
3 files changed, 17 insertions(+), 29 deletions(-)
diff --git a/examples/klee_hybrid_test.rs b/examples/klee_hybrid_test.rs
index 11ea854..7c22c43 100644
--- a/examples/klee_hybrid_test.rs
+++ b/examples/klee_hybrid_test.rs
@@ -24,10 +24,12 @@ use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
fn main() {
let mut a = 0;
klee_make_symbolic!(&mut a, "a");
+ // Rust panic on a == 200;
+ let _ = 100 / (a - 200);
match a {
0 => klee_abort!(),
1 => klee_abort!(),
- 2 => panic!(),
+ 2 => klee_abort!(),
3 => panic!("3"), // just one instance of panic! will be spotted
4 => klee_assert!(false),
5 => klee_assert_eq!(false, true),
diff --git a/examples/register_test.rs b/examples/register_test.rs
index a8acc1b..7398740 100644
--- a/examples/register_test.rs
+++ b/examples/register_test.rs
@@ -7,7 +7,7 @@
// will still be treated as a new symbol. That might be overly pessimistic
// but is a safe approximation for the worst case behavior of the hardware.
//
-// > cargo klee --bin register --release
+// > cargo klee --example register_test --release
// ...
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.2/src/lib.rs:49: abort failure
// KLEE: NOTE: now ignoring this error at this location
@@ -16,17 +16,17 @@
// KLEE: done: completed paths = 3
// KLEE: done: generated tests = 3
//
-// > ls target/release/deps/klee-last/
+// > ls target/release/examples/klee-last/
// assembly.ll info messages.txt run.istats run.stats test000001.ktest test000002.ktest test000003.abort.err test000003.kquery test000003.ktest warnings.txt
//
-// We see that KLEE spoted the test3 hits unreachable (and thus panics)
+// We see that KLEE spotted the test3 hits unreachable (and thus panics)
//
// Let's look at the test cases separately:
//
// test1 passed:
-// ktest-tool target/release/deps/klee-last/test000001.ktest
-// ktest file : 'target/release/deps/klee-last/test000001.ktest'
-// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
+// ktest-tool target/release/examples/klee-last/test000001.ktest
+// ktest file : 'target/release/examples/klee-last/test000001.ktest'
+// args : ['...']
// num objects: 1
// object 0: name: 'vcell'
// object 0: size: 4
@@ -38,9 +38,9 @@
// If the first read of the register is not 1 then we are ok.
//
// The second test also passed.
-// ktest-tool target/release/deps/klee-last/test000002.ktest
-// ktest file : 'target/release/deps/klee-last/test000002.ktest'
-// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
+// ktest-tool target/release/examples/klee-last/test000002.ktest
+// ktest file : 'target/release/examples/klee-last/test000002.ktest'
+// args : ['...']
// num objects: 2
// object 0: name: 'vcell'
// object 0: size: 4
@@ -60,9 +60,9 @@
// returning 2.
//
// The third test gives the error.
-// ktest-tool target/release/deps/klee-last/test000003.ktest
-// ktest file : 'target/release/deps/klee-last/test000003.ktest'
-// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
+// ktest-tool target/release/examples/klee-last/test000003.ktest
+// ktest file : 'target/release/examples/klee-last/test000003.ktest'
+// args : ['...']
// num objects: 2
// object 0: name: 'vcell'
// object 0: size: 4
@@ -85,7 +85,6 @@
#![no_main]
use panic_klee as _;
-
use volatile_register::RW;
#[no_mangle]
@@ -99,6 +98,7 @@ fn main() {
unsafe { rw.write(0) };
// this read is still treated as a new symbolic value of type u32
if rw.read() == 2 {
+ // will generate a panic!() if reached.
unreachable!();
}
}
diff --git a/examples/vcell_test.rs b/examples/vcell_test.rs
index a362802..236e748 100644
--- a/examples/vcell_test.rs
+++ b/examples/vcell_test.rs
@@ -1,24 +1,10 @@
#![no_std]
#![no_main]
-#[cfg(feature = "klee-analysis")]
use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-
-#[cfg(feature = "klee-analysis")]
use panic_klee as _;
-
-#[cfg(not(feature = "klee-analysis"))]
-use panic_halt as _;
-
-#[cfg(not(feature = "klee-analysis"))]
-#[no_mangle]
-fn main() {
- let mut a = 0;
- panic!();
-}
-
use vcell;
-#[cfg(feature = "klee-analysis")]
+
#[no_mangle]
fn main() {
let mut vc = vcell::VolatileCell::new(0u32);
--
GitLab