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