|
1
|
open Lustre_types
|
|
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
|
|