Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 2ed9b6f2

History | View | Annotate | Download (2.43 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

    
15
   This is a modified version that handle reset
16
*)
17

    
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

    
23
open Horn_backend_common
24
open Horn_backend_printers
25
open Horn_backend_collecting_sem
26

    
27
(*
28
TODO:
29
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows
30

    
31
- gerer le reset --- DONE
32
- reconstruire les rechable states DONE
33
- reintroduire le cex/traces ... DONE
34
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
35
*)
36

    
37
let main_print machines fmt =
38
if !Options.main_node <> "" then
39
  begin
40
    let node = !Options.main_node in
41
    let machine = get_machine machines node in
42
    collecting_semantics machines fmt node machine;
43
    check_prop machines fmt node machine;
44
    if !Options.horn_cex then(
45
      cex_computation machines fmt node machine;
46
      get_cex machines fmt node machine)
47
end
48

    
49
let print_type_definitions fmt =
50
  let cpt_type = ref 0 in
51
  Hashtbl.iter (fun typ decl ->
52
    match typ with
53
    | Tydec_const var ->
54
      (match decl.top_decl_desc with
55
      | TypeDef tdef -> (
56
	match tdef.tydef_desc with
57
	| Tydec_enum tl ->
58
	  incr cpt_type;
59
	  fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
60
	    var
61
	    (Utils.fprintf_list ~sep:" " pp_print_string) tl
62
	| _ -> assert false
63
      )
64
      | _ -> assert false
65
      )
66
    | _        -> ()) type_table
67

    
68

    
69
let translate fmt basename prog machines =
70
  (* We print typedef *)
71
  print_type_definitions fmt;
72
  List.iter (print_machine machines fmt) (List.rev machines);
73
  main_print machines fmt
74

    
75
(* Local Variables: *)
76
(* compile-command:"make -C ../.." *)
77
(* End: *)