Project

General

Profile

« Previous | Next » 

Revision e70326c9

Added by Pierre-Loïc Garoche about 5 years ago

Providing means to have specification as dynamic checks.
[bug] seems to crash with EMF backend

View differences:

src/main_lustre_compiler.ml
49 49
    Log.report ~level:1
50 50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51 51
    Lusic.write_lusic true header destname lusic_ext;
52
    Lusic.print_lusic_to_h destname lusic_ext;
52
    generate_lusic_header destname lusic_ext;
53 53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@ ")
54 54
  end
55 55

  
......
89 89

  
90 90

  
91 91

  
92
let dynamic_checks () =
93
  match !Options.output, !Options.spec with
94
  | "C", "C" -> true
95
  | _ -> false
96
     
92 97
(* From prog to prog *)
93 98
let stage1 prog dirname basename =
94 99
  (* Removing automata *)
......
196 201
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
197 202
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
198 203

  
204
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
205
  let prog =
206
    if dynamic_checks () then
207
      Spec.enforce_spec_prog prog
208
    else
209
      prog
210
  in
211
  
199 212
  (* Normalization phase *)
200 213
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
201 214
  (* Special treatment of arrows in lustre backend. We want to keep them *)

Also available in: Unified diff