| 1 |
8446bf03
|
ploc
|
open Lustre_types
|
| 2 |
ca7ff3f7
|
Lélio Brun
|
(* 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 |
e70326c9
|
ploc
|
|
| 6 |
ca7ff3f7
|
Lélio Brun
|
let enforce_spec_node nd =
|
| 7 |
|
|
(* TODO: add asserts for quantifier free normalized eexpr *)
|
| 8 |
e70326c9
|
ploc
|
nd
|
| 9 |
|
|
|
| 10 |
ca7ff3f7
|
Lélio Brun
|
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
|