|
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
|