From 3a8a27fa3360bd9926b8e1c2771b9f982d8a0992 Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Sat, 28 Dec 2019 17:37:31 +0100
Subject: [PATCH] works
---
examples/kabort.rs | 28 ----------------------------
examples/klee_test.rs | 33 +++++++++++++++++++++++++++++++++
2 files changed, 33 insertions(+), 28 deletions(-)
delete mode 100644 examples/kabort.rs
create mode 100644 examples/klee_test.rs
diff --git a/examples/kabort.rs b/examples/kabort.rs
deleted file mode 100644
index 3375985..0000000
--- a/examples/kabort.rs
+++ /dev/null
@@ -1,28 +0,0 @@
-#![no_std]
-#![no_main]
-
-#[cfg(feature = "klee-analysis")]
-use klee_sys::{klee_abort, klee_make_symbolic};
-
-#[cfg(not(feature = "klee-analysis"))]
-use panic_halt as _;
-
-#[cfg(not(feature = "klee-analysis"))]
-#[no_mangle]
-fn main() {
- let mut a = 0;
- panic!();
-}
-
-#[cfg(feature = "klee-analysis")]
-#[no_mangle]
-fn main() {
- let mut a = 0;
- klee_make_symbolic(&mut a, "a");
- match a {
- 0 => klee_abort(),
- 2 => klee_abort(),
- _ => (),
- };
- panic();
-}
diff --git a/examples/klee_test.rs b/examples/klee_test.rs
new file mode 100644
index 0000000..2dc2836
--- /dev/null
+++ b/examples/klee_test.rs
@@ -0,0 +1,33 @@
+#![no_std]
+#![no_main]
+
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+
+#[cfg(not(feature = "klee-analysis"))]
+use panic_halt as _;
+
+#[cfg(not(feature = "klee-analysis"))]
+#[no_mangle]
+fn main() {
+ let mut a = 0;
+ panic!();
+}
+
+#[cfg(feature = "klee-analysis")]
+#[no_mangle]
+fn main() {
+ let mut a = 0;
+ klee_make_symbolic!(&mut a, "a");
+ match a {
+ 0 => klee_abort!(),
+ 1 => klee_abort!(),
+ 2 => panic!(),
+ 3 => panic!("3"), // just one instance of panic! will be spotted
+ 4 => klee_assert!(false),
+ 5 => klee_assert_eq!(false, true),
+ 6 => klee_assert_eq!(false, true),
+ _ => (),
+ };
+ panic!("at end"); // just one instane of panic! will be spotted
+}
--
GitLab