From 57fed02f0910bf9d5bd7fbbfb9292f77753201fb Mon Sep 17 00:00:00 2001
From: Blinningjr <nicke.l@telia.com>
Date: Tue, 8 Dec 2020 10:37:01 +0100
Subject: [PATCH] Finished

---
 examples/get_sign.c | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/examples/get_sign.c b/examples/get_sign.c
index fb9195f..a10b519 100644
--- a/examples/get_sign.c
+++ b/examples/get_sign.c
@@ -210,7 +210,7 @@ int main()
 // [your answer here]
 // (gdb) print x
 // $1 = 0
-// It has the value 0 and it got that because the constraint x == o is the fist split in the paths. 
+// It has the value 0 and it got that because the constraint x == 0 is the fist split in the paths. 
 //
 // Step the code
 // > (gdb) next
@@ -271,6 +271,9 @@ int main()
 //
 // [your answer here]
 // (hint, mark memory region as symbolic)
+// Klee creates a symbol for the variable 'a', the symbol doesn't have any value. Instead it has constraints that are added to it when the paths branch. In the code example above the first if statement gives two paths. The first path has the condition 'a == 0' and the other path condition 'a != 0'.  Then if we had another if statement in the fist path that has the condition 'a > 0', it would always be false because 'a' can't be 'a = 0 && a > 0'. Thus the inside of that if statement would be unreachable.
+//
+//
 //
 // Explain in your own words how
 // `klee_make_symbolic(&a, sizeof(a), "a");`
@@ -279,3 +282,5 @@ int main()
 // [your answer here]
 // (hint, KTEST_FILE points to a concrete assignment
 // of the memory region)
+// It works by loading in the constrains for the path and then generating a value that satisfies that path. After that it runs the code with the generated value and checks that all the constraints are the same as before. If they are not it means that something has changed with the path and thus the behavior of the code has changed.
+//
-- 
GitLab