cargo_klee_examples/array.rs, A complete

cargo_klee_examples/examples/array.rs

@@ -38,6 +38,29 @@ fn main() {
 // (Hint, even if we don't use the result `b`, Rust do not optimize out the call, why?)
 //
 // [your answer here]
+/*
+In debug mode, we get 10 test cases.
+9 tests for different indecies, 0-8.
+And one for which the index overflows, this is marked with a name of type [test-name-here].abort.err
+
+In release, we only get 2 test cases.
+One containing the testvalue zero.
+And another containing a testcase for 9.
+
+Why?
+Well, the compiler has inserted a check for the value 9 for which it will panic without doing anything else.
+Running the test case in gdb will show yhou this in the asm code (shown code is for test index == 0):
+│B+ 0x555555555121 <array::main+1>  movq   $0x0,(%rsp)              <-- index = 0
+│   0x555555555129 <array::main+9>  lea    0xed4(%rip),%rdx        # 0x555555556004                                                                                                                                                  │
+│   0x555555555130 <array::main+16> mov    %rsp,%rdi                                                                                                                                                                                 │
+│   0x555555555133 <array::main+19> mov    $0x8,%esi                                                                                                                                                                                 │
+│   0x555555555138 <array::main+24> call   *0x2e8a(%rip)        # 0x555555557fc8                                                                                                                                                     │
+│  >0x55555555513e <array::main+30> cmpq   $0x9,(%rsp)   <------ The comparison                                                                                                                            │
+│   0x555555555143 <array::main+35> jae    0x555555555147 <array::main+39>   <-- Jumps to the panick code if index==9                                                                                                                                                        │
+│   0x555555555145 <array::main+37> pop    %rax                                                                                                                                                                                      │
+│   0x555555555146 <array::main+38> ret                                                                                                                                                                                              │
+│   0x555555555147 <array::main+39> call   0x555555555150 <_ZN4core9panicking18panic_bounds_check17he935ba9af86f066bE>
+*/
 //
 // B) Fix the code so that you don't get an error.
 // (It should still compute the sum of the n first elements