| 1 |
8446bf03
|
ploc
|
open Lustre_types
|
| 2 |
e70326c9
|
ploc
|
(* 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
|