Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

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