D

cargo_klee_examples/examples/array.rs

@@ -8,11 +8,11 @@
 use klee_sys::klee_make_symbolic;
 use panic_klee as _;
 
-fn sum_first_elements(arr: &[u8], index: usize) -> u8 {
-    let mut acc = 0;
+fn sum_first_elements(arr: &[u8], index: usize) -> u16 {
+    let mut acc: u16 = 0;
     for i in 0..index {
         if index < arr.len() {
-            acc += arr[i as usize];
+            acc += arr[i as usize] as u16;
         } else {
             break;
         }
@@ -45,7 +45,7 @@ fn main() {
 // [your answer here]]
 // The diffrence is that debug test all 10 possible paths and release only checks 2. This is becaus
 // 9 of the paths are basicly the same. These are the path were index is 0..8, the last path is
-// diffrent because then the index is out side of the array(index = 255), thus there will be an error.
+// diffrent because then the index is out side of the array(index = 255), thus there will be an error/panic.
 //
 //
 // Debug:
@@ -80,11 +80,15 @@ fn main() {
 // Explain what caused the error.
 //
 // [your answer here]
+// acc = 255 and arr[i as usize] = 127 in the secound loop in sum_first_elements, test4. Thus acc
+// is a u8 variable that will overflow and cause a panic.
 //
 // E) Make a sensible fix to the code.
 // Motivate your choice.
 //
 // [your answer here]
+// I made acc a u16 instead of a u8 because the maximum sum of arr is 8 * 255, which will easily
+// fit in a u16. And thus will avoid the overflow problem.
 //
 // [Git commit "D"]
 //