From 2df40c9d99971743eb3d604ad34962c874cfe73c Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 8 Dec 2020 11:30:47 +0100
Subject: [PATCH] rust wip (inccomlpete)
---
CHANGELOG.md | 2 +-
Cargo.toml | 33 +++++++++++++++++++++++++++++++++
examples/get_sign.rs | 27 +++++++++++++++++++++++++++
3 files changed, 61 insertions(+), 1 deletion(-)
create mode 100644 Cargo.toml
create mode 100644 examples/get_sign.rs
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b84b8bf..1a2f9a0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,4 +4,4 @@ Most recent changes:
- 2020-12-08 Update `README.md` for Ubuntu (like) system with `z3` dependency.
-- 2020-12-08 Update `README.md` and `examples/get_sign` to reflect the recent `klee 2.2` and `aur` package.
\ No newline at end of file
+- 2020-12-08 Update `README.md` and `examples/get_sign` to reflect the recent `klee 2.2` and `aur` package.
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..c288b3d
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,33 @@
+[package]
+name = "klee_tutorial"
+version = "0.1.0"
+authors = ["pln <Per Lindgren>"]
+edition = "2018"
+
+[dependencies.panic-klee]
+git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
+version = "0.1.0"
+
+
+[dependencies.klee-sys]
+git = "https://gitlab.henriktjader.com/pln/klee-sys.git"
+# path = "../klee-sys"
+version = "0.1.0"
+#features = ["inline-asm"]
+
+[features]
+klee-analysis = [ "klee-sys/klee-analysis" ]
+klee-replay = [ "klee-sys/klee-replay"]
+
+[profile.dev]
+panic = "abort"
+incremental = false # better optimization
+lto = true # better optimization
+codegen-units = 1 # better optimization
+
+[profile.release]
+panic = "abort"
+debug = true # better debugging
+incremental = false # better optimization
+lto = true # better optimization
+codegen-units = 1 # better optimization
\ No newline at end of file
diff --git a/examples/get_sign.rs b/examples/get_sign.rs
new file mode 100644
index 0000000..1ad6f7f
--- /dev/null
+++ b/examples/get_sign.rs
@@ -0,0 +1,27 @@
+// example that shows different types of path termination
+// and their effect to KLEE test case generation
+#![no_std]
+#![no_main]
+
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+use panic_klee as _;
+
+fn get_sign(x: i32) -> i32 {
+ if x == 0 {
+ return 0;
+ }
+ if x < 0 {
+ return -1;
+ } else {
+ return 1;
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let mut a: i32 = 0;
+ klee_make_symbolic!(&mut a, "a");
+ // std::process::exit(get_sign(a));
+}
+
+// > cargo rustc --example get_sign -- --emit=llvm-ir
--
GitLab