Exercise
========

Q1. 

line 8: 
	x in [0,8] 
    y is undefined
    i is undefined

 Rk: Since x is defined as un "unsigned char" and initialized  by a "read" 
     operation at line 5, we may expect to have x in [0,255] at line 7, 
     and hence  253, 254 ou 255 being possible values for x at line 8.
	Actually this is is not the case in C, since integer comparisons are 
    always performed on (signed) int, using implicit type conversions. 
	Thus "x+3,12" is casted into "(int)x + 3 < 12"

Q2. 

	- No runtime error at line 8
    - possible runtime error at line 14 

Q3. 

	Frama-C is supposed to over-approximate the set of values obtained for each variables 
    (potential false positives, but no false negatives)
    Hence, according to this tool:
		- no BoF vulnerability should occur at line 8 
           (according to the remark above)
		- a vulnerability may occur at line 14 ...

Q4. Path B0-B1
		1. path condition = (x0>=253 and x0<=255) or (x0>=0 and x0<=8)
        2. possible solution : x0=0
		3. to trigger the vuln:
		     (x0>=253 and x0<=255) or (x0>=0 and x0<=8) and (x0<=0 or x0>8)
			  possible solution : x0=253

Q5.

    1. From B3, B5 can be reached in 4 possible paths:
			B3-B5					(not entering the loop)
			B3-B4-B3-B5 				(1 iteration)
			B3-B4-B3-B4-B3-B5 			(2 iterations)
			B3-B4-B3-B4-B3-B4-B3-B5 	(3 iterations)
		From B0, B3 can be reached in 2 different paths:
			B0-B2
			B0-B1-B2
		The total number of paths is then 8 (4 times 2)

	2. path B0-B1-B2-B3-B4-B3-B4-B3-B4-B3-B5 
		path predicate: 
			x0+3<12 and y0=x0+1 and i0=y0 and 
            i0<3 and y1=y0+2 and i1=i0+1 and 
            i1<3 and y2=y1+2 and i2=i1+1 and 
            i2<3 and y3=y2+2 and i3=i2+1 and 
            i3>=3 and (y3<0 or y3>8)

		No solution since :
			- to execute the loop 3 times we need x0=255 (hence y0=0 and i0=0)
			- if it is the case then necessary we have y3=6

    3. Vulnerability at line 8 can be triggered, but not at line 14 (following this path) ...

        Rq: this result contradicts the one found by Frama-C (question Q3),
this is due to a different interpretation of the C semantics by these 2 tools,
Frama-C being more correct :-)

Q6. With this modification:
		- For Frama-C, using interval analysis there is no way to keep track of the relationnal dependency between i and y (namel i<y),
          both variable will then be considered as taking arbitrary independent values, which may led to numerous false positives ... 
		- PathCrawler may be no longer be able to explore all the paths (since there number is huge, depending on the number of iterations performed),
          so it may or may not found the vulnerabilities (depending on the exploration strategy ...)