Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / verifiers.ml @ e8250987

History | View | Annotate | Download (1.22 KB)

1
open Lustre_types
2

    
3
open VerifierList
4

    
5
let active = ref None
6
           
7
let options () = 
8
  List.flatten (
9
    List.map Options_management.verifier_opt (
10
      List.map (fun m ->
11
	let module M = (val m : VerifierType.S) in
12
	(M.name, M.activate, M.options)
13
      ) verifiers
14
    ))
15
  
16
let verifier_list verifiers =
17
  List.fold_left (fun acc m ->
18
      let module M =  (val m : VerifierType.S) in
19
      (if acc = "" then "" else acc ^ ", ") ^ M.name
20
    ) "" verifiers
21
  
22
let get_active () =
23
  match !active with
24
  | None ->
25
     begin
26
       (* check that a single one is active and register it *)
27
       let found =
28
         List.fold_left (fun found m ->
29
             let module M =  (val m : VerifierType.S) in
30
             if M.is_active () then
31
               m::found
32
             else
33
               found
34
           ) [] verifiers
35
       in
36
       match found with
37
       | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers))
38
       | [m] -> active := Some m; m
39
       | _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found))
40
     end
41

    
42
  | Some m -> m
43

    
44

    
45
                
46
                (* Local Variables: *)
47
                (* compile-command:"make -C .." *)
48
                (* End: *)