From 13126a2059caa22d743ae27ff0e160f205243d46 Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Mon, 30 Dec 2019 16:44:27 +0100
Subject: [PATCH] examples updated
---
Cargo.lock | 289 +++++++++++++++++-
Cargo.toml | 1 +
.../{klee_test.rs => klee_hybrid_test.rs} | 3 +
examples/klee_only_test.rs | 24 ++
examples/register_test.rs | 105 +++++++
5 files changed, 421 insertions(+), 1 deletion(-)
rename examples/{klee_test.rs => klee_hybrid_test.rs} (86%)
create mode 100644 examples/klee_only_test.rs
create mode 100644 examples/register_test.rs
diff --git a/Cargo.lock b/Cargo.lock
index e8967d8..06c5d27 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1,5 +1,99 @@
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
+[[package]]
+name = "aligned"
+version = "0.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "as-slice"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "autocfg"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "bare-metal"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "byteorder"
+version = "1.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "cortex-m"
+version = "0.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rt"
+version = "0.6.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cortex-m-rt-macros 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
+ "r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rt-macros"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rtfm"
+version = "0.5.1"
+dependencies = [
+ "cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rtfm-macros 0.5.0",
+ "heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rtfm-macros"
+version = "0.5.0"
+dependencies = [
+ "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-semihosting"
+version = "0.3.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
[[package]]
name = "cstr_core"
version = "0.1.2"
@@ -14,21 +108,80 @@ name = "cty"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
+[[package]]
+name = "generic-array"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "generic-array"
+version = "0.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "hash32"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "heapless"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "indexmap"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
[[package]]
name = "klee-examples"
version = "0.1.0"
dependencies = [
- "klee-sys 0.1.0",
+ "cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rtfm 0.5.1",
+ "cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
+ "lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)",
+ "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+ "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "klee-sys"
version = "0.1.0"
+source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#e3a296be9ce3376aa501dd60eefb3d0699506aef"
dependencies = [
"cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
+[[package]]
+name = "lm3s6965"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
[[package]]
name = "memchr"
version = "2.2.1"
@@ -39,8 +192,142 @@ name = "panic-halt"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
+[[package]]
+name = "panic-klee"
+version = "0.1.0"
+source = "git+https://gitlab.henriktjader.com/pln/panic-klee.git#3b0c897f49d7fff017424364e280bcb9dbaffa5d"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "r0"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rtfm-core"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rtfm-syntax"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "rustc_version"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver-parser"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "stable_deref_trait"
+version = "1.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "syn"
+version = "1.0.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "typenum"
+version = "1.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "vcell"
+version = "0.1.2"
+source = "git+https://github.com/perlindgren/vcell.git?branch=trustit#29304497be5cf16aec53447473ff5a3f41783ba3"
+dependencies = [
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
+]
+
+[[package]]
+name = "volatile-register"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+]
+
[metadata]
+"checksum aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "eb1ce8b3382016136ab1d31a1b5ce807144f8b7eb2d5f16b2108f0f07edceb94"
+"checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
+"checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
+"checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
+"checksum byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a7c3dd8985a7111efc5c80b44e23ecdd8c007de8ade3b96595387e812b957cf5"
+"checksum cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)" = "145da2fc379bbd378ed425e75e1748214add9bbd800d4d5b77abb54ca423dbca"
+"checksum cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)" = "33a716cd7d8627fae3892c2eede9249e50d2d79aedfb43ca28dad9a2b23876d9"
+"checksum cortex-m-rt-macros 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "72b1073338d1e691b3b7aaf6bd61993e589ececce9242a02dfa5453e1b98918d"
+"checksum cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
+"checksum generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)" = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
+"checksum generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)" = "0ed1e761351b56f54eb9dcd0cfaca9fd0daecf93918e1cfc01c8a3d26ee7adcd"
+"checksum hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "d4041af86e63ac4298ce40e5cca669066e75b6f1aa3390fe2561ffa5e1d9f4cc"
+"checksum heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "f339aa7d51777fc0af6aa7cbeb277dfc6e6c029cbdeda48d0fbb92c2337f0e69"
+"checksum indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "712d7b3ea5827fcb9d4fda14bf4da5f136f0db2ae9c8f4bd4e2d1c6fde4e6db2"
+"checksum klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)" = "<none>"
+"checksum lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "8698042a7495160eac9f7298a32cd1ddbb6ad2780f766f5a99b4f0a6b915e0ad"
"checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
"checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
+"checksum panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)" = "<none>"
+"checksum proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)" = "9c9e470a8dc4aeae2dee2f335e8f533e2d4b347e1434e5671afc49b054592f27"
+"checksum quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
+"checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
+"checksum rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "9ec893edb2aa5b70320b94896ffea22a7ebb1cf3f942bb67cd5b60a865a63493"
+"checksum rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "4455e23c34df3d66454e7e218a4d76a7f83321d04a806be614463341cec4116e"
+"checksum rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)" = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
+"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
+"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
+"checksum stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
+"checksum syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)" = "dff0acdb207ae2fe6d5976617f887eb1e35a2ba52c13c7234c790960cdad9238"
+"checksum typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
+"checksum unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
+"checksum vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)" = "<none>"
+"checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
diff --git a/Cargo.toml b/Cargo.toml
index 8cdb97f..9403828 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -9,6 +9,7 @@ panic-halt = "0.2.0"
cortex-m-semihosting = "0.3.5"
lm3s6965 = "0.1.3"
vcell = "0.1.2"
+volatile-register = "0.2.0"
[dependencies.panic-klee]
git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
diff --git a/examples/klee_test.rs b/examples/klee_hybrid_test.rs
similarity index 86%
rename from examples/klee_test.rs
rename to examples/klee_hybrid_test.rs
index 282d2bc..11ea854 100644
--- a/examples/klee_test.rs
+++ b/examples/klee_hybrid_test.rs
@@ -1,3 +1,6 @@
+// example to show conditional compilation of hybrid applications
+// compiling both for klee analysis and just as bare metal
+//
#![no_std]
#![no_main]
diff --git a/examples/klee_only_test.rs b/examples/klee_only_test.rs
new file mode 100644
index 0000000..1269206
--- /dev/null
+++ b/examples/klee_only_test.rs
@@ -0,0 +1,24 @@
+// 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 _;
+
+#[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
+}
diff --git a/examples/register_test.rs b/examples/register_test.rs
new file mode 100644
index 0000000..a8acc1b
--- /dev/null
+++ b/examples/register_test.rs
@@ -0,0 +1,105 @@
+// showcase volatile register
+// This is the underlying abstraction to all register accesses using the
+// embedded Rust ecosystem.
+//
+// When analyzed by KLEE, we make the return value symbolic, thus each access
+// givs a new unique symbol. Even if we write a value to it, the next read
+// 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
+// ...
+// 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
+
+// KLEE: done: total instructions = 33
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+//
+// > ls target/release/deps/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)
+//
+// 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']
+// num objects: 1
+// object 0: name: 'vcell'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+// 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']
+// num objects: 2
+// object 0: name: 'vcell'
+// object 0: size: 4
+// object 0: data: b'\x01\x00\x00\x00'
+// object 0: hex : 0x01000000
+// object 0: int : 1
+// object 0: uint: 1
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x00\x00\x00\x00'
+// object 1: hex : 0x00000000
+// object 1: int : 0
+// object 1: uint: 0
+// object 1: text: ....
+// Here we are saved by the second reading of the register NOT giving
+// 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']
+// num objects: 2
+// object 0: name: 'vcell'
+// object 0: size: 4
+// object 0: data: b'\x01\x00\x00\x00'
+// object 0: hex : 0x01000000
+// object 0: int : 1
+// object 0: uint: 1
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x02\x00\x00\x00'
+// object 1: hex : 0x02000000
+// object 1: int : 2
+// object 1: uint: 2
+// object 1: text: ....
+//
+// The first read gives 1, the second 2, and we hit unreacable.
+
+#![no_std]
+#![no_main]
+
+use panic_klee as _;
+
+use volatile_register::RW;
+
+#[no_mangle]
+fn main() {
+ // we emulate a read/write hardware register (rw)
+ let rw: RW<u32> = unsafe { core::mem::MaybeUninit::uninit().assume_init() };
+
+ // reading will render a symbolic value of type u32
+ if rw.read() == 1 {
+ // we emulate a write to the hardware register
+ unsafe { rw.write(0) };
+ // this read is still treated as a new symbolic value of type u32
+ if rw.read() == 2 {
+ unreachable!();
+ }
+ }
+}
--
GitLab