Project

General

Profile

Download (538 Bytes) Statistics
| Branch: | Tag: | Revision:
1 8446bf03 ploc
open Lustre_types
2 ca7ff3f7 Lélio Brun
(* TODO: - verifier que les spec sont quantifiers free ou sinon mettre un
3
   warning - rajouter les expressions requires => ensures dans le node - sauver
4
   le nom des variables locales qui encodent ces specs. *)
5 e70326c9 ploc
6 ca7ff3f7 Lélio Brun
let enforce_spec_node nd =
7
  (* TODO: add asserts for quantifier free normalized eexpr *)
8 e70326c9 ploc
  nd
9
10 ca7ff3f7 Lélio Brun
let enforce_spec_prog prog =
11
  List.map
12
    (fun top ->
13
      match top.top_decl_desc with
14
      | Node nd ->
15
        { top with top_decl_desc = Node (enforce_spec_node nd) }
16
      | _ ->
17
        top)
18
    prog