lustrec / src / spec.ml @ 3340aff0
History | View | Annotate | Download (524 Bytes)
| 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 |
|