From 436f05fe3559e87a233b655047d46864b56ffeca Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Sun, 2 Oct 2022 18:33:52 +0200
Subject: [PATCH] examples
---
klee-examples/.vscode/settings.json | 5 ++++-
klee-examples/Cargo.toml | 3 +--
klee-examples/examples/get_sign.rs | 3 ++-
klee-examples/src/main.rs | 31 +++++++++++++++++++++++++++++
4 files changed, 38 insertions(+), 4 deletions(-)
create mode 100644 klee-examples/src/main.rs
diff --git a/klee-examples/.vscode/settings.json b/klee-examples/.vscode/settings.json
index 1635b45..a8a3dd8 100644
--- a/klee-examples/.vscode/settings.json
+++ b/klee-examples/.vscode/settings.json
@@ -1,6 +1,9 @@
{
"cSpell.ignoreWords": [
+ "eabihf",
"istats",
- "ktest"
+ "klee_make_symbolic",
+ "ktest",
+ "thumbv"
]
}
\ No newline at end of file
diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index 801094d..619b90b 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -2,7 +2,7 @@
name = "cargo_klee_examples"
version = "0.3.0"
authors = ["pln <Per Lindgren>"]
-edition = "2018"
+edition = "2021"
[dependencies.klee-sys]
git = "https://gitlab.henriktjader.com/pln/klee-sys.git"
@@ -27,4 +27,3 @@ debug = true # better debugging
incremental = false # better optimization
lto = true # better optimization
codegen-units = 1 # better optimization
-
diff --git a/klee-examples/examples/get_sign.rs b/klee-examples/examples/get_sign.rs
index 418f7b4..717a16e 100644
--- a/klee-examples/examples/get_sign.rs
+++ b/klee-examples/examples/get_sign.rs
@@ -32,13 +32,14 @@ fn main() {
// Compile a Rust program for KLEE test case generation.
//
-// > cargo klee --examples get_sign
+// > cargo klee --example get_sign
// ...
//
// KLEE: Using Z3 solver backend
//
// KLEE: done: total instructions = 89
// KLEE: done: completed paths = 3
+// KLEE: done: partially completed paths = 0
// KLEE: done: generated tests = 3
//
// To view the generated tests:
diff --git a/klee-examples/src/main.rs b/klee-examples/src/main.rs
new file mode 100644
index 0000000..1a6b075
--- /dev/null
+++ b/klee-examples/src/main.rs
@@ -0,0 +1,31 @@
+// Testing a small Rust function.
+// Inspired by `get_sign` https://klee.github.io/tutorials/testing-function/
+
+// Here, we do not want to analyse the Rust run-time, thus `no_std`.
+#![no_std]
+#![no_main]
+
+// Low level binding(s) to the KLEE API.
+use klee_sys::klee_make_symbolic;
+
+// Binding of Rust `panic` to KLEE `abort`.
+use panic_klee as _;
+
+fn get_sign(x: i32) -> i32 {
+ if x == 0 {
+ return 0;
+ }
+ if x < 0 {
+ return -1;
+ } else {
+ return 1;
+ }
+}
+
+// KLEE needs the non mangled `main` symbol.
+#[no_mangle]
+fn main() {
+ let mut a: i32 = 0;
+ klee_make_symbolic!(&mut a, "a");
+ get_sign(a);
+}
--
GitLab