Exercise 1
===========

1) get_sign.c

We find 3 possible concrete integer inputs corresdponding to each possible program paths:
  - a strictly positive value
  - a strictly negative value
  - a null value

2) regexp.c

First we find to memory overflow errors, at line 28 and 26.
These errors are due to the fact that our symoblic "re" string is not NULL-terminated
(which was an implicit assumption of the code under test).


After adding a NULL character at the end of buffer "re" (using the klee_assume directive after 
the call to klee_make_symbolic, to constrain the symbolic value), we do not get any errors when 
running KLEE.
(Actually we only get an error to signal that non NULL-terminated inputs are rejected) 

Exercise 2
===========

1) Running KLEE we get an error, showing that KLEE *always* tries to symbolic inputs triggerring 
  buffer overflows.
 
Note that during KLEE execution, ecch error (identified by its source line number) is reported 
only once, hence we may have several test cases leading to the error but only one of them 
flagged as erroneous.


2) This example shows that a "bounded loop" (by a non symbolic expression) is "normally" executed by 
   KLEE at runtime, leading on this code to only two possible paths (due to the final if statement).

3) Contrarily to the previous one, this example shows that a "non bounded loop" (those condition depend on a symbolic expression) 
   will lead to a potentially huge number of execution paths, since KLEE needs to exercise all the situations leading to 
   each possible post-condition (i.e, iterating 0, 1, 2, 3, ... times).

Exercise 3
===========

Running KLEE on this example we see that we manage to get the buffer overflow error, but without reaching the "You win" 
scenario, as it was the case when executing the corresponding binary code.
This is because KLEE execution is based on an LLVM bytecode interpreter, which does not rely on the processor level 
memory model, and which traps immediately memory overflows.