2020 updates, wip

.vscode/settings.json

+{
+    "cSpell.ignoreWords": [
+        "backtrace",
+        "eabihf",
+        "em",
+        "fffffffd",
+        "file",
+        "istats",
+        "ktest",
+        "ktest file",
+        "libc",
+        "libcore",
+        "lldb",
+        "llvm",
+        "maybe",
+        "maybe uninit",
+        "openocd",
+        "satisfiability",
+        "sigabrt",
+        "thumbv",
+        "thumbv em",
+        "trustit",
+        "uninit",
+        "vcell",
+        "x",
+        "x fffffffd"
+    ]
+}
\ No newline at end of file

README.md

@@ -6,10 +6,9 @@ See section `Cargo.toml` for detailed information on features introduced.
 
 ### General dependencies
 
-- LLVM toolchain tested with (9.0.1)
-- rustup tested with 1.40.0 (73528e339 2019-12-16)
-- klee tested with KLEE 2.1-pre (https://klee.github.io)
-
+- LLVM toolchain tested with (9.0.1 and 10.0.1)
+- rustup tested with rust toolchain 1.47.0 (18bf6b4f0 2020-10-07) and 1.49.0-nightly (ffa2e7ae8 2020-10-24) 
+- klee tested with KLEE 2.1 (https://klee.github.io)
 - cargo-klee (installed from git)
 
 ---

examples/README.md

+# Examples
+
+## assume_assert
+
+Exercises the ability to introduce assumptions in order to prove assertions.
+
+This leads into possibilities for contracts.
+
+## register_test
+
+Exercises the ability to automatically treat hardware read accesses as streams of unknown values,
+and hardware write accesses as no operations. In this way, we can *pessimistically* analyse low-level
+code such as drivers. More detailed information (assumptions) on the behavior of the hardware can be 
+modelled as mocks for the corresponding register blocks.
\ No newline at end of file

examples/assume_assert.rs

@@ -50,7 +50,7 @@ fn f1(a: u32) -> u32 {
 //         #100000193 in _ZN4core9panicking9panic_fmt17hdeb7979ab6591473E (=94422569870368, =94422566526016) at src/libcore/panicking.rs:139
 //         #200000227 in _ZN4core9panicking5panic17hb5daa85c7c72fc62E (=94422566525664, =28, =94422566526016) at src/libcore/panicking.rs:70
 //         #300000130 in _ZN13assume_assert2f117h371b5439de984e07E () at examples/assume_assert.rs:19
-//        #400000088 in main () at examples/assume_assert.rs:13
+//         #400000088 in main () at examples/assume_assert.rs:13
 //
 // So its line 19, (a + 1)
 //
@@ -74,7 +74,7 @@ fn f1(a: u32) -> u32 {
 // So KLEE tracks the "path condition", i.e., at line 18 it knows (assumes) that that
 // a < u32::MAX, and finds that the assumption a == u32::MAX cannot be satisfied.
 //
-// This is extremely powerful as KLEE tracks all known "constraints" and all their raliaitons
+// This is extremely powerful as KLEE tracks all known "constraints" and all their relations
 // and mathematically checks for the satisfiability of each "assume" and "assert".
 // So what we get here is not a mere test, but an actual proof!!!!
 // This is the way!
@@ -102,7 +102,7 @@ fn f1(a: u32) -> u32 {
 //     a + 1
 // }
 //
-// It might even be possible to derive post condtitions from pre conditions,
+// It might even be possible to derive post conditions from pre-conditions,
 // and report them to the user. Problem is that the conditions are
 // represented as "first order logic" (FOL) constraints, which need to be
 // converted into readable form (preferably Rust expressions.)

examples/register_test.rs

@@ -27,7 +27,7 @@ fn main() {
 // 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
+// gives 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.
 //
@@ -104,7 +104,7 @@ fn main() {
 // object 1: uint: 2
 // object 1: text: ....
 //
-// The first read gives 1, the second 2, and we hit unreacable.
+// The first read gives 1, the second 2, and we hit unreachable.
 //
 // We can replay the last test to gather more information:
 // $ cargo klee --example register_test -r -k -g -v
@@ -136,7 +136,9 @@ fn main() {
 // (gdb) print read_2
 // $2 = 2
 //
-// If this does not work its a gdb problem, try lldb the LLVM debugger
+// If this does not work its a gdb problem, try `lldb` (or `rust-lldb`) the LLVM debugger
 // (debug info may not be completely compatible)
 //
+// https://lldb.llvm.org/use/map.html
+//
 // This is the way!