Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
| src/spec.ml | ||
|---|---|---|
| 1 | 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 |
*) |
|
| 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. *) |
|
| 7 | 5 |
|
| 8 |
let enforce_spec_node nd =
|
|
| 9 |
(* TODO: add asserts for quantifier free normalized eexpr *)
|
|
| 6 |
let enforce_spec_node nd = |
|
| 7 |
(* TODO: add asserts for quantifier free normalized eexpr *)
|
|
| 10 | 8 |
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 | 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 |
|
Also available in: Unified diff
reformatting