Handle Recursive Calls in Why3 Output

[iconmaster5326]

Currently, programs that are recursive, or call a function that calls it, do not correctly generate into Why3. This is because functions are grouped into theories, and theories cannot be forward declared like constants and predicates- This makes recursive imports impossible.

For simple recursion, the answer is simple. We have to detect a call to itself, and when this happens, replace the call predicate with the function’s execute predicate.

However, mutual recursion between functions is difficult. We will have to merge these functions into a single theory somehow. This could be done by altering the names of all the variables and placing them in the same theory, or maybe by inlining the LLVM of all mutual recursion. It will require potentially large changes to how we generate Why3.