From 2733789a995a23bab7d1e89886cf7dc3963d1f10 Mon Sep 17 00:00:00 2001
From: Blinningjr <nicke.l@telia.com>
Date: Sun, 13 Dec 2020 15:55:51 +0100
Subject: [PATCH] Finished get_sign.rs
---
examples/get_sign.rs | 10 +++++++++-
1 file changed, 9 insertions(+), 1 deletion(-)
diff --git a/examples/get_sign.rs b/examples/get_sign.rs
index 7028183..a7862fb 100644
--- a/examples/get_sign.rs
+++ b/examples/get_sign.rs
@@ -109,13 +109,17 @@ mod ll {
// What was the generated hash.
//
// [your answer here]
+// 85c57be6132dac1d
//
// B) Inspecting the test cases.
//
// Figure out to run `ktest-tool` on the generated test cases.
// (Hint, it is just a matter of paths.)
//
-// [your answer here]
+// [your answer here] TODO: What is the question here?
+// ktest-tool target/debug/examples/klee-out-0/test000001.ktest x < 0 return -1
+// ktest-tool target/debug/examples/klee-out-0/test000002.ktest x > 0 retunr 1
+// ktest-tool target/debug/examples/klee-out-0/test000003.ktest x = 0 retunr 0
//
// C) Replaying your test cases.
//
@@ -136,6 +140,7 @@ mod ll {
// > ls *.o
//
// [your answer here]
+// get_sign-85c57be6132dac1d.o
//
// Now we need to link it with the `libkleeRuntest`.
//
@@ -154,14 +159,17 @@ mod ll {
// Now run the code in the debugger. What path was triggered.
//
// [your answer here]
+// x < 0, return -1
//
// Change to test000002, what path does it trigger.
//
// [your answer here]
+// x > 0, return 1
//
// And finally change to test000003, what path was triggered.
//
// [your answer here]
+// x = 0, return 0
//
// D) Remarks and conclusions.
//
--
GitLab