RAC : List functions and loops that might have a too weak contract
When the small step RAC succeeds but the giant step RAC fails, this means we have a weakness in the contract of some previous loop of function that has been executed. We should list the previously called functions/loops as being the potential culprits.
We should filter from this list functions from the standard library as well as whyML builtins (like ref
for instance), to keep only user-defined functions and loops. A way to do this is to add an attribute [@stdlib]
on all stdlib functions so that we can distinguish them easily, and an attribute [@mlw:builtin]
for whyML builtins functions.