Project

General

Profile

Revision 04a188ec

View differences:

src/backends/Ada/ada_backend.ml
155 155
    match Machine_code_common.get_machine_opt filtered_machines main_node with
156 156
    | None -> begin
157 157
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
158
      raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
158
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
159 159
    end
160 160
    | Some m -> Some m
161 161
  )) in
src/backends/C/c_backend.ml
54 54
    | None -> begin
55 55
      Global.main_node := main_node;
56 56
      Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
57
      raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
57
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
58 58
    end
59 59
    | Some m -> begin
60 60
      let source_main_file = (if !Options.cpp then destname ^ "_main.cpp" else destname ^ "_main.c") in (* Could be changed *)
......
76 76
    | None -> begin
77 77
      Global.main_node := mauve;
78 78
      Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
79
      raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
79
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
80 80
    end
81 81
    | Some m -> begin
82 82
      let source_mauve_file = destname ^ "_mauve.hpp" in
src/backends/C/c_backend_common.ml
762 762
	Format.eprintf "Code generation error: %a%a@."
763 763
	  Error.pp_error_msg Error.Main_wrong_kind
764 764
	  Location.pp_loc v'.var_loc;
765
	raise (Error (v'.var_loc, Error.Main_wrong_kind))
765
	raise (Error.Error (v'.var_loc, Error.Main_wrong_kind))
766 766
      end
767 767
  in
768 768
  Utils.List.iteri2 (fun idx v' v ->
src/basic_library.ml
247 247
           Const_tag tag_true
248 248
         else
249 249
           Const_tag tag_false
250
      | "=", [Const_tag t1; Const_tag t2]
251
             ->
252
         if t1 = t2 then
253
           Const_tag tag_true
254
         else
255
           Const_tag tag_false
256
      | "!=", [Const_tag t1; Const_tag t2]
257
             ->
258
         if t1 = t2 then
259
           Const_tag tag_false
260
         else
261
           Const_tag tag_true
250 262
      | "not", [Const_tag c] -> Const_tag( if c = tag_true then tag_false else if c = tag_false then tag_true else assert false)
251 263
      | bool_fun, [Const_tag c1; Const_tag c2]
252 264
           when List.mem bool_fun bool_funs ->
253 265
         eval_bool_fun bool_fun c1 c2 
254
      | _ -> assert false
266
      | _ -> let loc= e.expr_loc in
267
             let err =Error.Unbound_symbol (op ^ (string_of_bool (List.mem op rel_funs)) ^ " in basic library") in
268
             raise (Error.Error (loc, err))
255 269
    in
256 270
    Expr_const new_cst 
257 271
  )       
......
285 299
                  (* Local Variables: *)
286 300
                  (* compile-command:"make -C .." *)
287 301
                  (* End: *)
302

  
303

  
304
let _ =
305
  (* Loading environement *)
306
  Global.type_env := type_env;
307
  Global.clock_env := clock_env
src/checks/algebraicLoop.ml
373 373
      (* We stop with unresolved AL *)(* TODO create a report *)
374 374
      (* Printing the report on stderr *)
375 375
      Format.eprintf "%a" pp_report report;
376
      raise (Corelang.Error (Location.dummy_loc, Error.AlgebraicLoop))
376
      raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop))
377 377
    )
378 378
  in
379 379
  (* Printing the report on stderr *)
src/checks/stateless.ml
41 41
          with Not_found ->
42 42
            let loc = expr.expr_loc in
43 43
            Error.pp_error loc (fun fmt -> Format.fprintf fmt "Unable to find node %s in expression %a" i Printers.pp_expr expr);
44
            raise (Corelang.Error (loc, Error.Unbound_symbol i))
44
            raise (Error.Error (loc, Error.Unbound_symbol i))
45 45
        ))
46 46
  
47 47
and compute_node nd = (* returns true iff the node is stateless.*)
src/compiler_common.ml
18 18
  if !Options.main_node = "" then
19 19
    begin
20 20
      eprintf "Code generation error: %a@." Error.pp_error_msg Error.No_main_specified;
21
      raise (Error (Location.dummy_loc, Error.No_main_specified))
21
      raise (Error.Error (Location.dummy_loc, Error.No_main_specified))
22 22
    end
23 23

  
24 24
let create_dest_dir () =
......
59 59
    | (Parse.Error err) as exc -> 
60 60
       Parse.report_error err;
61 61
       raise exc
62
    | Corelang.Error (loc, err) as exc -> (
62
    | Error.Error (loc, err) as exc -> (
63 63
      eprintf "Parsing error: %a%a@."
64 64
        Error.pp_error_msg err
65 65
        Location.pp_loc loc;
......
74 74
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. expanding automata@ ");
75 75
  try
76 76
    Automata.expand_decls decls
77
  with (Corelang.Error (loc, err)) as exc ->
77
  with (Error.Error (loc, err)) as exc ->
78 78
    eprintf "Automata error: %a%a@."
79 79
      Error.pp_error_msg err
80 80
      Location.pp_loc loc;
......
237 237
            let stmts = in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts in
238 238
            let c = merge_contracts c imp_c in
239 239
            stmts, locals, c 
240
          with Not_found -> Format.eprintf "Where is contract %s@.@?" name; raise (Error (loc, (Error.Unbound_symbol ("contract " ^ name))))
240
          with Not_found -> Format.eprintf "Where is contract %s@.@?" name; raise (Error.Error (loc, (Error.Unbound_symbol ("contract " ^ name))))
241 241

  
242 242
         
243 243
        ) ([], c.consts@c.locals, c) c.imports
src/compiler_stages.ml
92 92
        ignore (Corelang.node_from_name main_node)
93 93
      with Not_found -> (
94 94
        Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
95
        raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
95
        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
96 96
    ))
97 97
  in
98 98
  
src/corelang.ml
15 15
(*open Dimension*)
16 16

  
17 17

  
18
exception Error of Location.t * Error.error_kind
19

  
20 18
module VDeclModule =
21 19
struct (* Node module *)
22 20
  type t = var_decl
......
1438 1436
       if Basic_library.is_expr_internal_fun e then
1439 1437
         Basic_library.partial_eval op args opt
1440 1438
       else
1441
         Expr_appl (op, pa e, opt)
1439
         Expr_appl (op, args, opt)
1442 1440
    | Expr_array el ->
1443 1441
       Expr_array (List.map pa el)
1444 1442
    | Expr_access (e, d) ->
src/corelang.mli
12 12

  
13 13
open Lustre_types
14 14

  
15
exception Error of Location.t * Error.error_kind
16 15
module VSet: sig
17 16
  include Set.S
18 17
  val pp: Format.formatter -> t -> unit 
src/error.ml
1 1
open Format
2 2

  
3

  
3 4
type ident = Lustre_types.ident
4 5
type error_kind =
5 6
    Main_not_found
......
11 12
  | Wrong_number of ident
12 13
  | AlgebraicLoop
13 14
  | LoadError of string
15
exception Error of Location.t * error_kind
14 16

  
15 17
let return_code kind =
16 18
  match kind with
......
63 65
    pp_msg
64 66

  
65 67
let pp_error loc pp_msg =
66
  Format.eprintf "@.%a@.Error: @[<v 0>%t@]@."
68
  Format.eprintf "@.%a@.Error: @[<v 0>%t@]@.@?"
67 69
    Location.pp_loc loc
68 70
    pp_msg
71
    
69 72

  
70 73
    
src/global.ml
1 1
module Types = Types.Main
2 2

  
3
let type_env : (Types.type_expr Env.t) ref = ref Basic_library.type_env
4
let clock_env : (Clocks.clock_expr Env.t) ref = ref Basic_library.clock_env
3
let type_env : (Types.type_expr Env.t) ref = ref Env.initial (* Basic_library.type_env *)
4
let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial (*Basic_library.clock_env *)
5 5
let basename = ref ""
6 6
let main_node = ref ""
7 7

  
src/lusic.ml
44 44
    prog []
45 45

  
46 46
let check_obsolete lusic basename =
47
  if lusic.obsolete then raise (Error (Location.dummy_loc, Error.Wrong_number basename))
47
  if lusic.obsolete then raise (Error.Error (Location.dummy_loc, Error.Wrong_number basename))
48 48

  
49 49
(* encode and write a header in a file *)
50 50
let write_lusic lusi (header : top_decl list) basename extension =
src/lustre_types.ml
8 8
(*  version 2.1.                                                    *)
9 9
(*                                                                  *)
10 10
(********************************************************************)
11
  
11

  
12

  
12 13
type ident = Utils.ident
13 14
type rat = Utils.rat
14 15
type tag = Utils.tag
src/main_lustre_compiler.ml
140 140
  with
141 141
  | Parse.Error _
142 142
  | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
143
  | Corelang.Error (loc , kind) (*| Task_set.Error _*) ->
143
  | Error.Error (loc , kind) (*| Task_set.Error _*) ->
144 144
     Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
145 145
     exit (Error.return_code kind)
146 146
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
src/main_lustre_testgen.ml
191 191
  with
192 192
  | Parse.Error _
193 193
  | Types.Error (_,_) | Clocks.Error (_,_)
194
  | Corelang.Error _ (*| Task_set.Error _*)
194
  | Error.Error _ (*| Task_set.Error _*)
195 195
  | Causality.Error _ -> exit 1
196 196
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
197 197
  | exc -> (track_exception (); raise exc)
src/main_lustre_verifier.ml
133 133
    Arg.parse options anonymous usage
134 134
  with
135 135
  | Parse.Error _
136
  | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
137
  | Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind)
136
    | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
137
  | Error.Error (loc , kind) (*| Task_set.Error _*) -> 
138
     Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
139
     exit (Error.return_code kind)
138 140
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
139 141
  | Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1
140 142
  | exc -> (track_exception (); raise exc) 
141 143

  
142
(* Local Variables: *)
143
(* compile-command:"make -C .." *)
144
(* End: *)
144
             (* Local Variables: *)
145
             (* compile-command:"make -C .." *)
146
             (* End: *)
src/modules.ml
18 18
    Options_management.name_dependency (local, dep) ext 
19 19
  with Not_found ->
20 20
    (* Error.pp_error loc (fun fmt -> Format.fprintf fmt "Unknown library %s" dep); *)
21
    raise (Error (loc, Error.Unknown_library dep))
21
    raise (Error.Error (loc, Error.Unknown_library dep))
22 22

  
23 23
  
24 24
let add_symbol loc msg hashtbl name value =
25 25
 if Hashtbl.mem hashtbl name
26
 then raise (Error (loc, Error.Already_bound_symbol msg))
26
 then raise (Error.Error (loc, Error.Already_bound_symbol msg))
27 27
 else Hashtbl.add hashtbl name value
28 28

  
29 29
let check_symbol loc msg hashtbl name =
30 30
 if not (Hashtbl.mem hashtbl name)
31
 then raise (Error (loc, Error.Unbound_symbol msg))
31
 then raise (Error.Error (loc, Error.Unbound_symbol msg))
32 32
 else ()
33 33

  
34 34

  
......
42 42
    let itf = value.top_decl_itf in
43 43
    match value'.top_decl_desc, value.top_decl_desc with
44 44
    | Node _        , ImportedNode _  when owner = owner' && itf' && (not itf) -> update_node name value
45
    | ImportedNode _, ImportedNode _            -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
45
    | ImportedNode _, ImportedNode _            -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
46 46
    | _                                         -> assert false
47 47
  with
48 48
    Not_found                                   -> update_node name value
......
57 57
    let itf = value.top_decl_itf in
58 58
    match value'.top_decl_desc, value.top_decl_desc with
59 59
    | ImportedNode _, Node _          when owner = owner' && itf' && (not itf) -> ()
60
    | Node _        , Node _                    -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
60
    | Node _        , Node _                    -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
61 61
    | _                                         -> assert false
62 62
  with
63 63
    Not_found                                   -> update_node name value
......
65 65

  
66 66
let add_tag loc name typ =
67 67
  if Hashtbl.mem tag_table name then
68
    raise (Error (loc, Error.Already_bound_symbol ("enum tag " ^ name)))
68
    raise (Error.Error (loc, Error.Already_bound_symbol ("enum tag " ^ name)))
69 69
  else Hashtbl.add tag_table name typ
70 70

  
71 71
let add_field loc name typ =
72 72
  if Hashtbl.mem field_table name then
73
    raise (Error (loc, Error.Already_bound_symbol ("struct field " ^ name)))
73
    raise (Error.Error (loc, Error.Already_bound_symbol ("struct field " ^ name)))
74 74
  else Hashtbl.add field_table name typ
75 75

  
76 76
let import_typedef name tydef =
......
84 84
    | Tydec_clock ty      -> import ty
85 85
    | Tydec_const c       ->
86 86
       if not (Hashtbl.mem type_table (Tydec_const c))
87
       then raise (Error (loc, Error.Unbound_symbol ("type " ^ c)))
87
       then raise (Error.Error (loc, Error.Unbound_symbol ("type " ^ c)))
88 88
       else ()
89 89
    | Tydec_array (c, ty) -> import ty
90 90
    | _                   -> ()
......
100 100
    let itf = value.top_decl_itf in
101 101
    match value'.top_decl_desc, value.top_decl_desc with
102 102
    | TypeDef ty', TypeDef ty when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf' && (not itf) -> ()
103
    | TypeDef ty', TypeDef ty -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("type " ^ name)))
103
    | TypeDef ty', TypeDef ty -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("type " ^ name)))
104 104
    | _       -> assert false
105 105
  with Not_found -> (import_typedef name value; Hashtbl.add type_table (Tydec_const name) value)
106 106

  
107 107
let check_type loc name =
108 108
 if not (Hashtbl.mem type_table (Tydec_const name))
109
 then raise (Error (loc, Error.Unbound_symbol ("type " ^ name)))
109
 then raise (Error.Error (loc, Error.Unbound_symbol ("type " ^ name)))
110 110
 else ()
111 111

  
112 112
let add_const itf name value =
......
118 118
    let itf = value.top_decl_itf in
119 119
    match value'.top_decl_desc, value.top_decl_desc with
120 120
    | Const c', Const c when c.const_value = c'.const_value && owner' = owner && itf' && (not itf) -> ()
121
    | Const c', Const c -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("const " ^ name)))
121
    | Const c', Const c -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("const " ^ name)))
122 122
    | _       -> assert false
123 123
  with Not_found -> Hashtbl.add consts_table name value
124 124

  
......
156 156
      lusic
157 157
    with
158 158
    | Sys_error _  ->
159
       raise (Error (loc, Error.Unknown_library basename))
159
       raise (Error.Error (loc, Error.Unknown_library basename))
160 160
  )
161 161
  | _ -> assert false (* should not happen *)
162 162

  
......
224 224
          | Not_found ->
225 225
             let loc = decl.top_decl_loc in
226 226
             Error.pp_error loc (fun fmt -> Format.fprintf fmt "Unknown library %s" dep);
227
             raise (Error (loc, Error.Unknown_library dep (*basename*)))
227
             raise (Error.Error (loc, Error.Unknown_library dep (*basename*)))
228 228
        )
229 229
        | Include name ->
230 230
           let basename = name_dependency decl.top_decl_loc (true, name) "" in
......
235 235
             in
236 236
             decl::accu_prog, accu_dep, typ_env, clk_env
237 237
           else
238
             raise (Error (decl.top_decl_loc, LoadError("include requires a lustre file")))
238
             raise (Error.Error (decl.top_decl_loc, LoadError("include requires a lustre file")))
239 239
           
240 240
        | Node nd ->
241 241
           if is_header then
242
             raise (Error(decl.top_decl_loc,
242
             raise (Error.Error(decl.top_decl_loc,
243 243
                          LoadError ("node " ^ nd.node_id ^ " declared in a header file")))  
244 244
           else (
245 245
             (* Registering node *)
......
254 254
             decl::accu_prog, accu_dep, typ_env', clk_env'                   
255 255
           )
256 256
           else
257
             raise (Error(decl.top_decl_loc,
257
             raise (Error.Error(decl.top_decl_loc,
258 258
                          LoadError ("imported node " ^ ind.nodei_id ^
259 259
                                       " declared in a regular Lustre file")))  
260 260
        | Const c -> (
......
281 281
    in
282 282
    List.rev prog, List.rev deps, (typ_env, clk_env)
283 283
  with
284
    Corelang.Error (loc, err) as exc -> (
284
    Error.Error (loc, err) as exc -> (
285 285
    (* Format.eprintf "Import error: %a%a@."
286 286
     *   Error.pp_error_msg err
287 287
     *   Location.pp_loc loc; *)
src/parsers/lexer_lustre.mll
91 91
  with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift orig_loc loc, Parse.Annot_error s))
92 92

  
93 93
let make_spec orig_loc lexbuf s = 
94
  Format.eprintf "make spec loc %a" Location.pp_loc orig_loc;
95 94
  try
96 95
    Location.push_loc orig_loc;	
97 96
    let ns = LexerLustreSpec.spec s in
src/tools/seal/seal_extract.ml
3 3
open Seal_utils			
4 4
open Zustre_data (* Access to Z3 context *)
5 5
   
6

  
6
let _ =
7
  Z3.Params.update_param_value !ctx "timeout" "10000"
8
  
7 9
(* Switched system extraction: expression are memoized *)
8 10
(*let expr_mem = Hashtbl.create 13*)
9 11
    
......
373 375
    in
374 376
    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
375 377
    let zl = simplify zl in
376
        if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
378
    if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
379
    (* Format.eprintf "Calling Z3@."; *)
377 380
    let status_res = Z3.Solver.check solver zl in
381
    (* Format.eprintf "Z3 done@."; *)
378 382
     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
379 383
    match status_res with
380 384
    | Z3.Solver.UNSATISFIABLE -> false, []
......
675 679
  (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "
676 680
   *   Printers.pp_expr expr
677 681
   *   (Utils.fprintf_list ~sep:"@ "
678
   *        pp_guard_expr) res; *)
682
   *        (pp_guard_expr pp_elem)) res; *)
679 683
  res
680 684
  
681 685
and add_def defs vid expr =
......
685 689
  let vid_defs = rewrite defs expr in
686 690
  (* Format.eprintf "-> @[<v 0>%a@]@."
687 691
   *   (Utils.fprintf_list ~sep:"@ "
688
   *      (pp_guard_expr pp_elem)) vid_defs;   *)
692
   *      (pp_guard_expr pp_elem)) vid_defs; *)
689 693
  report ~level:6 (fun fmt -> Format.fprintf fmt  "Add_def: %s = %a@. -> @[<v 0>%a@]@."
690 694
      vid
691 695
      Printers.pp_expr expr
......
845 849
          (Expr elem)
846 850
          mem_defs
847 851
      in
852
      report ~level:4 (fun fmt -> Format.fprintf fmt "split by guard done@.");
853
      
848 854
  (*    Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."
849 855
        Printers.pp_expr elem
850 856
        pp_all_defs mem_defs
......
861 867
      | Expr_const (Const_tag tag) when tag = tag_false 
862 868
        ->   build_switch_sys neg prefix
863 869
      | _ -> (* Regular case *)
870
         report ~level:4 (fun fmt -> Format.fprintf fmt "Building both children branches@."); 
864 871
         (* let _ = (
865 872
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
866 873
          *     match elem.expr_desc with
......
872 879
          * in *)
873 880
         let clean l =
874 881
           let l = List.map (fun (e,b) -> (Expr e), b) l in
882
           report ~level:4 (fun fmt -> Format.fprintf fmt "Checking satisfiability of %a@."
883
                                     (pp_guard_list pp_elem) l
884
             );
875 885
           let ok, l = check_sat l in
876 886
           let l = List.map (fun (e,b) -> deelem e, b) l in
877 887
           ok, l
878 888
         in
879 889
         let pos_prefix = (elem, true)::prefix in
880 890
         let neg_prefix = (elem, false)::prefix in
891
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches ...@."); 
881 892
         let ok_pos, pos_prefix = clean pos_prefix in         
893
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche pos done@."); 
882 894
         let ok_neg, neg_prefix = clean neg_prefix in
895
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche neg done@."); 
896
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches done@."); 
883 897
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
884 898
         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
885 899
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
......
946 960
     Each assign is stored in a hash tbl as list of guarded
947 961
     expressions. The memory definition is also "rewritten" as such a
948 962
     list of guarded assigns.  *)
963
  report ~level:1 (fun fmt -> Format.fprintf fmt "registering all definitions in guarded form ...@.");
949 964
  let mem_defs, output_defs =
950 965
    List.fold_left (fun (accu_mems, accu_outputs) eq ->
951 966
        match eq.eq_lhs with
......
984 999
        | _ -> assert false (* should have been removed by normalization *)
985 1000
      ) ([], []) sorted_eqs
986 1001
  in
1002
  report ~level:1 (fun fmt -> Format.fprintf fmt "registering all definitions done@.");
987 1003

  
988 1004
  
989 1005
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
......
1035 1051
        ))
1036 1052
        update_defs);
1037 1053
  (* Format.eprintf "Build init@."; *)
1038
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@.");
1054
  
1055
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@.");
1039 1056
  let sw_init= 
1040 1057
    build_switch_sys init_defs []
1041 1058
  in
1042 1059
  (* Format.eprintf "Build step@."; *)
1043
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@.");
1044 1060
  let sw_sys =
1045 1061
    build_switch_sys update_defs []
1046 1062
  in
1063
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@.");
1047 1064

  
1048
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@.");
1065
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@.");
1049 1066
  let init_out =
1050 1067
    build_switch_sys init_out []
1051 1068
  in
1052
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@.");
1069
  (* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *)
1053 1070

  
1054 1071
  let update_out =
1055 1072
    build_switch_sys update_out []
1056 1073
  in
1074
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@.");
1075

  
1076
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@.");
1057 1077

  
1058 1078
  let sw_init = clean_sys sw_init in
1059 1079
  let sw_sys = clean_sys sw_sys in
1060 1080
  let init_out = clean_sys init_out in
1061 1081
  let update_out = clean_sys update_out in
1082
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1062 1083

  
1063 1084
  (* Some additional checks *)
1064 1085
  
src/tools/seal/seal_verifier.ml
57 57
      | None -> begin
58 58
          Global.main_node := s;
59 59
          Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
60
          raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
60
          raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
61 61
        end
62 62
      | Some _ -> s
63 63
    )
......
66 66
  let nd = m.mname in
67 67
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
68 68
  let mems = m.mmemory in
69
  report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems));
69 70
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
70 71
  let msch = Utils.desome m.msch in
71 72
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
......
106 107
       let pp_res = pp_res Printers.pp_expr in
107 108
      Format.fprintf fmt "DynSys:@ @[<v 0>@[<v 3>Init:@ %a@]@ "
108 109
        pp_res  sw_init;
109
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
110
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
110 111
        pp_res  sw_sys
111 112
    );
112
  report ~level:1 (fun fmt ->
113

  
114

  
115
                
116
 report ~level:1 (fun fmt ->
113 117
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
114 118
       let pp_res = pp_res Printers.pp_expr in
115
      Format.fprintf fmt "Output:@ @[<v 0>@[<v 3>Init:@ %a@]@ "
116
        pp_res  init_out;
117
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
119
      Format.fprintf fmt "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ "
120
             (List.length init_out)
121
                   (List.length update_out)
122
                   pp_res  init_out;
123
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
118 124
        pp_res  update_out
119 125
    );
120 126
  let _ = match !seal_export with
src/tools/zustre/zustre_common.ml
697 697
				      let hash = Hashtbl.hash
698 698
  end)
699 699
  in
700
(* Fonction seems unused 
701

  
700 702
  let rec get_expr_vars e =
701 703
    let open Utils in
702 704
    let nb_args = Z3.Expr.get_num_args e in
......
729 731
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
730 732
	FDSet.empty (Z3.Expr.get_args e)
731 733
  in
734
 *)
732 735
  (* Unsed variable. Coul;d be reintroduced 
733 736
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
734 737
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in

Also available in: Unified diff