Skip to content
Snippets Groups Projects
Commit 4611bc48 authored by Henrik Tjäder's avatar Henrik Tjäder
Browse files

Spellcheck

parent cadb9a4c
No related branches found
No related tags found
No related merge requests found
...@@ -114,11 +114,11 @@ fn idle() -> ! { ...@@ -114,11 +114,11 @@ fn idle() -> ! {
// here 'j' has the value 0x00 (0 as integer), triggering the `else` branch // here 'j' has the value 0x00 (0 as integer), triggering the `else` branch
// //
// How, can KLEE figure out concrete values for the symbolic variable `j`? // How, can KLEE figure out concrete values for the symbolic variable `j`?
// Well, it tracks the data dependencies and condititonals along feasible execution paths // Well, it tracks the data dependencies and conditionals along feasible execution paths
// of the program (task EXTI1 in our case). And when encountering a `k_abort` // of the program (task EXTI1 in our case). And when encountering a `k_abort`
// it passes the collected (path) condition to an SMT solver. // it passes the collected (path) condition to an SMT solver.
// The solver returns with a concrete assigmnent for a `k_abort` if possible. // The solver returns with a concrete assignment for a `k_abort` if possible.
// This can be seen as a reachabilty proof or (equivalently) as a counter example // This can be seen as a reachability proof or (equivalently) as a counter example
// to an `k_assert`. // to an `k_assert`.
// //
// Show to the lab assistant that you can replicate the above, and explain // Show to the lab assistant that you can replicate the above, and explain
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment