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/compiler_common.ml
188 188
   (Env.initial, Env.initial)
189 189
 *)
190 190

  
191
let generate_lusic_header destname lusic_ext =	
192
  match !Options.output with
193
  | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
194
  | _ -> ()
195
	 
196

  
197
    
191 198
let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
192 199
  try
193 200
    (* checking defined types are compatible with declared types*)
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 *)
src/spec.ml
1
open LustreSpec
2
(*      TODO:
3
	- verifier que les spec sont quantifiers free ou sinon mettre un warning
4
      - rajouter les expressions requires => ensures dans le node
5
    - sauver le nom des variables locales qui encodent ces specs.
6
*)
7

  
8
let enforce_spec_node nd = 
9
(* TODO: add asserts for quantifier free normalized eexpr  *)
10
  nd
11
  
12
let enforce_spec_prog prog =
13
  List.map (
14
    fun top -> match top.top_decl_desc with
15
    | Node nd -> {top with top_decl_desc = Node (enforce_spec_node nd) }
16
    | _ -> top
17
  ) prog
18

  

Also available in: Unified diff