Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / spec.ml @ 684d39e7

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