Revision 6c3f2837
Added by Pierre-Loïc Garoche almost 3 years ago
| src/main_lustre_verifier.ml | ||
|---|---|---|
| 78 | 78 |
in |
| 79 | 79 |
|
| 80 | 80 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "); |
| 81 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code_common.pp_machines machine_code); |
|
| 81 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ " |
|
| 82 |
Machine_code_common.pp_machines machine_code); |
|
| 82 | 83 |
|
| 83 | 84 |
if Scopes.Plugin.show_scopes () then |
| 84 | 85 |
begin |
| ... | ... | |
| 93 | 94 |
|
| 94 | 95 |
let machine_code = Plugins.refine_machine_code prog machine_code in |
| 95 | 96 |
|
| 96 |
assert (dependencies = []); (* Do not handle deps yet *)
|
|
| 97 |
(*assert (dependencies = []); (* Do not handle deps yet *)*)
|
|
| 97 | 98 |
incr Options.verbose_level; |
| 98 | 99 |
Verifier.run basename prog machine_code; |
| 99 | 100 |
begin |
Also available in: Unified diff
lustrev: removed the check of no dependencies