Closed Delja closed 4 years ago
I used this method first, but there are two drawbacks:
add a dependency between the contracts and the different compiler phases to guarantee that the weaving phase will be executed before their calls.
modify the interpreter to call the run_global_phases()
in order to call the process_mainmodule
method.
I did the modifications, it seems good to me, depending on the tests result we will adapt.
This pr introduces a new hook method in the execution of the
process_nmodule_after_phases
phases. This method makes it possible to analyze each module again after the execution of all phases in order to benefit from the information of the whole program.This method is useful in the context of contracts. Example:
Actually, when you call the foo property in the bar method, no contract is called, while a postcondition was added by refinement in the
b
module. In fact it was not possible to call the contract face because it was not yet introduced during the analysis of modulea
. It is now possible to re-analyze all the modules to make the redirection once all the information are known.