From 4d54c303bc0a031fda1fb1b39cad3a0d24ed6a89 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Mon, 14 Dec 2020 15:39:50 +0100
Subject: [PATCH] array.rs C exercise, clarification
---
cargo_klee_examples/Cargo.toml | 4 ++++
cargo_klee_examples/examples/array.rs | 5 ++++-
2 files changed, 8 insertions(+), 1 deletion(-)
diff --git a/cargo_klee_examples/Cargo.toml b/cargo_klee_examples/Cargo.toml
index e0d04a0..af929d0 100644
--- a/cargo_klee_examples/Cargo.toml
+++ b/cargo_klee_examples/Cargo.toml
@@ -22,6 +22,10 @@ version = "0.6.1"
[dependencies]
vcell = "0.1.2"
+[dependencies.cstr_core]
+version = "0.2.2"
+default-features = false
+
[patch.crates-io]
cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
diff --git a/cargo_klee_examples/examples/array.rs b/cargo_klee_examples/examples/array.rs
index 6c055e6..9ec5e10 100644
--- a/cargo_klee_examples/examples/array.rs
+++ b/cargo_klee_examples/examples/array.rs
@@ -48,11 +48,14 @@ fn main() {
//
// C) In the example, the array is holding only zeroes.
// Figure out a way to make the content symbolic.
-// (Hint, declare as mutable, iterate and set each element symbolic)
+// (Hint, declare as mutable, iterate and set each element symbolic.)
+// (Hint2, it seems that you can set the whole array symbolic directly
+// without messing with an iterator, super!!!.)
//
// [Git commit "C"]
//
// D) Analyze the example using KLEE. Now a new (maybe unexpected) error should occur!
+// Notice, the error occurs only in `debug/dev` builds.
//
// Explain what caused the error.
//
--
GitLab