Skip to content
Snippets Groups Projects
Commit 57fed02f authored by Blinningjr's avatar Blinningjr
Browse files

Finished

parent 1015fe95
No related branches found
No related tags found
No related merge requests found
...@@ -210,7 +210,7 @@ int main() ...@@ -210,7 +210,7 @@ int main()
// [your answer here] // [your answer here]
// (gdb) print x // (gdb) print x
// $1 = 0 // $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 // Step the code
// > (gdb) next // > (gdb) next
...@@ -271,6 +271,9 @@ int main() ...@@ -271,6 +271,9 @@ int main()
// //
// [your answer here] // [your answer here]
// (hint, mark memory region as symbolic) // (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 // Explain in your own words how
// `klee_make_symbolic(&a, sizeof(a), "a");` // `klee_make_symbolic(&a, sizeof(a), "a");`
...@@ -279,3 +282,5 @@ int main() ...@@ -279,3 +282,5 @@ int main()
// [your answer here] // [your answer here]
// (hint, KTEST_FILE points to a concrete assignment // (hint, KTEST_FILE points to a concrete assignment
// of the memory region) // 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.
//
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment