Project

General

Profile

Download (538 Bytes) Statistics
| Branch: | Tag: | Revision:
1
open Lustre_types
2
(* 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

    
6
let enforce_spec_node nd =
7
  (* TODO: add asserts for quantifier free normalized eexpr *)
8
  nd
9

    
10
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
(56-56/66)