Project

General

Profile

Revision 0d79d0f3 src/main_lustre_verifier.ml

View differences:

src/main_lustre_verifier.ml
45 45
  let source_name = dirname ^ "/" ^ basename ^ extension in
46 46

  
47 47
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
48
  decr Options.verbose_level;
48 49

  
49 50
  (* Parsing source *)
50 51
  let prog = parse_source source_name in
51 52

  
52 53
  (* Checking which solver is active *)
54
  incr Options.verbose_level;
53 55
  let verifier = Verifiers.get_active () in
54 56
  let module Verifier = (val verifier : VerifierType.S) in
55 57

  
56
  
58
  decr Options.verbose_level;
57 59
  (* Normalizing it *)
58 60
  let prog, dependencies = 
59 61
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
60 62
    try
63
      incr Options.verbose_level;
61 64
      let params = Verifier.get_normalization_params () in
65
      decr Options.verbose_level;
62 66
      Compiler_stages.stage1 params prog dirname basename
63 67
    with Compiler_stages.StopPhase1 prog -> (
64 68
        assert false
......
75 79

  
76 80
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
77 81
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code_common.pp_machines machine_code);
78

  
82
  
79 83
  if Scopes.Plugin.show_scopes () then
80 84
    begin
81 85
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
......
90 94
  let machine_code = Plugins.refine_machine_code prog machine_code in
91 95

  
92 96
  assert (dependencies = []); (* Do not handle deps yet *)
97
  incr Options.verbose_level;
93 98
  Verifier.run basename prog machine_code;
94 99
  begin
95
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
100
    decr Options.verbose_level;
101
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ ");
102
    incr Options.verbose_level;
103
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@.");
96 104
    (* We stop the process here *)
97 105
    exit 0
98 106
  end

Also available in: Unified diff