diff --git a/cargo_klee_examples/Cargo.toml b/cargo_klee_examples/Cargo.toml index e0d04a04df6483a138cfec8d126665639931bcba..af929d08e149550f36822a70966ab77553af530a 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 6c055e634feb7c5f6a5d509bf44dd1110780f98b..9ec5e1001018328b5faced47a765caf80b610028 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. //