|
35 | 35 | private class ContractsPhase |
36 | 36 | super Phase |
37 | 37 |
|
38 | | - # The entry point of the contract phase |
39 | | - # In reality, the contract phase is executed on each module |
40 | | - # FIXME: Actually all method is checked to add method if any contract is inherited |
41 | 38 | redef fun process_nmodule(nmodule)do |
42 | 39 | # Check if the contracts are disabled |
43 | 40 | if toolcontext.opt_no_contract.value then return |
44 | 41 | nmodule.do_contracts(self.toolcontext) |
45 | 42 | end |
| 43 | + |
| 44 | + redef fun process_mainmodule(mainmodule: MModule, given_mmodules: SequenceRead[MModule]) do |
| 45 | + # Visit all loaded modules `toolcontext.nmodules` to do contract weaving |
| 46 | + for nmodule in toolcontext.modelbuilder.nmodules do |
| 47 | + nmodule.do_weaving_contracts(self.toolcontext) |
| 48 | + end |
| 49 | + end |
46 | 50 | end |
47 | 51 |
|
48 | 52 | redef class AModule |
49 | | - # Compile all contracts |
50 | | - # |
51 | | - # The implementation of the contracts is done in two visits. |
52 | | - # |
53 | | - # - First step, the visitor analyzes and constructs the contracts |
54 | | - # for each class (invariant) and method (expect, ensure). |
55 | | - # |
56 | | - # - Second step the visitor analyzes each `ASendExpr` to see |
57 | | - # if the callsite calls a method with a contract. If this is |
58 | | - # the case the callsite is replaced by another callsite to the contract method. |
| 53 | + |
| 54 | + # Entry point to generate the entire contract infrastructure. |
| 55 | + # Once this method is called we must call the `do_weaving_contracts` method (see it for more information). |
59 | 56 | fun do_contracts(toolcontext: ToolContext) do |
60 | 57 | var ast_builder = new ASTBuilder(mmodule.as(not null)) |
61 | 58 | # |
62 | 59 | var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, ast_builder) |
63 | 60 | contract_visitor.enter_visit(self) |
64 | | - # |
| 61 | + end |
| 62 | + |
| 63 | + # Entry point to execute the weaving in order to redirect the calls to the contract sides if it's needed. |
| 64 | + fun do_weaving_contracts(toolcontext: ToolContext) |
| 65 | + do |
| 66 | + var ast_builder = new ASTBuilder(mmodule.as(not null)) |
65 | 67 | var callsite_visitor = new CallSiteVisitor(toolcontext, ast_builder) |
66 | 68 | callsite_visitor.enter_visit(self) |
67 | 69 | end |
|
0 commit comments