Open fshahinfar1 opened 7 months ago
My current rough idea is to change every while/do-while loops to a for loop with an upper bound. The original condition of the loop would be checked inside the body of the new for-loop. For deciding the upper bound of the for-loop I can rely on the __ANNOTATE_LOOP to provide information.
There can also be some unbounded for-loops. Currently, I have no idea on how to check if a for loop is bounded or not.
The tool need to transform loops of variable number of iteration in order to pass the verifier. One approach is to ask the user to provide an upper bound and then perform the transformation.