Loop Tests

Objetive

Have a solid data about the behavior of the tool when dealing with loops and functions in different contexts.
With the data consider the continuity of the tool in this project and documentation.
Study about the assert(0) <- this is espected to be an error

Tests

Loop array 1-1

Click here to see the tests

Loop array 1-2

Click here to see the tests

Loop array 2-1

Click here to see the tests

Loop array 2-2

Click here to see the tests

Loop functions 1-1

Click here to see the tests

Loop multivar 1-1

Click here to see the tests

Loop nested 1-1

Click here to see the tests

Loop underapprox 1-1

Click here to see the tests

Loop underapprox 1-2

Click here to see the tests

Loop Tests Data

original functions	sliced parts in Frama-c	original results in ESBMC	sliced results in ESBMC
loop_array2-2	#define SZ, assert(0)
loop_functions1-1
loop_multivar1-1
loop_nested1-1
loop_underapprox1-2

to go back to the previous page: Click me!