Source file register_gui.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
open Cil_types
open Printer_tag
open Gui_types
type main_ui = Design.main_window_extension_points
module UsedVarState =
Cil_state_builder.Varinfo_hashtbl
(Datatype.Bool)
(struct
let size = 17
let name = "Value.Gui.UsedVarState"
let dependencies = [ Self.state ]
end)
let used_var = UsedVarState.memo
(fun var ->
Function_calls.partial_results () ||
try
let f = fst (Globals.entry_point ()) in
let inputs = Eva_dynamic.Inout.kf_inputs f in
let outputs = Eva_dynamic.Inout.kf_outputs f in
let b = Base.of_varinfo var in
Locations.Zone.mem_base b inputs || Locations.Zone.mem_base b outputs
with e ->
Gui_parameters.error ~once:true
"Exception during usability analysis of var %s: %s"
var.vname (Printexc.to_string e);
true
)
let hide_unused = ref (fun () -> false)
let sync_filetree (filetree:Filetree.t) =
if not (!hide_unused ()) then
(Globals.Functions.iter
(fun kf ->
try
let vi = Kernel_function.get_vi kf in
let strikethrough =
Analysis.is_computed () && not (Results.is_called kf)
in
filetree#set_global_attribute ~strikethrough vi
with Not_found -> ());
Globals.Vars.iter
(fun vi _ ->
if vi.vsource = true then
filetree#set_global_attribute
~strikethrough:(Analysis.is_computed () && not (used_var vi))
vi
);
if not (filetree#flat_mode) then
List.iter
(fun file ->
let globals_state = filetree#get_file_globals file in
filetree#set_file_attribute
~strikethrough:(Analysis.is_computed () &&
List.for_all snd globals_state)
file
)
(Globals.FileIndex.get_files ())
)
else
()
let hide_unused_function_or_var g =
!hide_unused () && Analysis.is_computed () &&
(match g with
| GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
let kf = Globals.Functions.get vi in
not (Results.is_called kf)
| GVarDecl (vi, _) | GVar (vi, _, _) ->
not (used_var vi)
| _ -> false
)
let value_panel pack (main_ui:main_ui) =
let box = GPack.vbox () in
let run_button = GButton.button ~label:"Run" ~packing:(box#pack) () in
let w =
GPack.table ~packing:(box#pack ~expand:true ~fill:true) ~columns:2 ()
in
let box_1_1 = GPack.hbox ~packing:(w#attach ~left:1 ~top:1) () in
let precision_refresh =
let tooltip = Parameters.Precision.parameter.Typed_parameter.help in
Gtk_helper.on_int ~lower:(-1) ~upper:11 ~tooltip
box_1_1 "precision (meta-option)"
Parameters.Precision.get
Parameters.Precision.set
in
let box_1_2 = GPack.hbox ~packing:(w#attach ~left:1 ~top:2) () in
let slevel_refresh =
let tooltip =
Parameters.SemanticUnrollingLevel.parameter.Typed_parameter.help
in
Gtk_helper.on_int ~lower:0 ~upper:1000000 ~tooltip
box_1_2 "slevel"
Parameters.SemanticUnrollingLevel.get
Parameters.SemanticUnrollingLevel.set
in
let box_1_3 = GPack.hbox ~packing:(w#attach ~left:1 ~top:3) () in
let validator s =
not
(Kernel_function.Set.is_empty
(Parameter_customize.get_c_ified_functions s))
in
let main_refresh = Gtk_helper.on_string
~tooltip:Kernel.MainFunction.parameter.Typed_parameter.help
~validator box_1_3 "main" Kernel.MainFunction.get Kernel.MainFunction.set
in
let refresh () = precision_refresh (); slevel_refresh (); main_refresh() in
ignore (run_button#connect#pressed
~callback:(fun () ->
main_ui#protect ~cancelable:true
(fun () -> refresh (); Analysis.compute (); main_ui#reset ());
));
pack box;
"Eva", box#coerce, Some refresh
let active_highlighter buffer localizable ~start ~stop =
let open Gtk_helper in
let buffer = buffer#buffer in
if Analysis.is_computed () then
match localizable with
| PStmt (kf, stmt) -> begin
let degenerate =
try
Some (
if Eva_utils.DegenerationPoints.find stmt
then (make_tag buffer ~name:"degeneration" [`BACKGROUND "orange"])
else (make_tag buffer ~name:"unpropagated" [`BACKGROUND "yellow"])
)
with Not_found -> None
in
match degenerate with
| Some color_area ->
apply_tag buffer color_area start stop
| None ->
if Analysis.status kf <> Analyzed NoResults then begin
let csf = Gui_callstacks_filters.focused_callstacks () in
if Gui_callstacks_filters.is_reachable_stmt csf stmt then begin
if Gui_callstacks_filters.is_non_terminating_instr csf stmt then
let non_terminating =
Gtk_helper.make_tag
buffer ~name:"value_non_terminating"
[`BACKGROUND "tomato"]
in
apply_tag buffer non_terminating (stop-1) stop
end
else
let dead_code_area =
make_tag buffer ~name:"deadcode"
[`BACKGROUND "tomato";`STYLE `ITALIC]
in
apply_tag buffer dead_code_area start stop
end
end
| _ -> ()
let display_eval_errors (main_ui:main_ui) l =
let pp = function
| Eval_terms.LogicEvalError ee ->
main_ui#pretty_information "Cannot evaluate: %a@."
Eval_terms.pretty_logic_evaluation_error ee
| e ->
main_ui#pretty_information "Unknown error during evaluation (%s)@."
(Printexc.to_string e)
in
List.iter pp l
let pretty_kf_escaped kf =
Pretty_utils.(escape_underscores (to_string Kernel_function.pretty kf))
let (main_ui:main_ui) (:menu) funs =
let aux kf =
try
let g = Kernel_function.get_global kf in
ignore
(popup_factory#add_item
("Go to definition of " ^ pretty_kf_escaped kf ^ " (indirect)")
~callback:(fun () -> main_ui#select_or_display_global g))
with Not_found -> ()
in
List.iter aux funs
let gui_compute_values (main_ui:main_ui) =
if not (Analysis.is_computed ())
then main_ui#launcher ()
let cleaned_outputs kf s =
let outs = Eva_dynamic.Inout.stmt_outputs s in
let accept = Logic_inout.accept_base ~formals:true ~locals:true kf in
let filter = Locations.Zone.filter_base accept in
filter outs
let pretty_stmt_info (main_ui:main_ui) kf stmt =
if Results.is_reachable stmt then begin
if Eva_results.is_non_terminating_instr stmt then
match stmt.skind with
| Instr (Call (_, _, _, _)
| Local_init (_, ConsInit _, _)) ->
main_ui#pretty_information "This call never terminates.@."
| Instr _ ->
main_ui#pretty_information "This instruction always fail.@."
| _ -> ()
else
let outs = cleaned_outputs kf stmt in
main_ui#pretty_information
"Modifies @[<hov>%a@]@." Locations.Zone.pretty outs
end
else main_ui#pretty_information "This code is dead@."
type term_or_pred = Term | Pred
let pp_term_or_pred fmt = function
| Term -> Format.pp_print_string fmt "term"
| Pred -> Format.pp_print_string fmt "predicate"
let last_evaluate_acsl_request = ref ""
(** Responses of the GUI to user actions. Built by the Select functor. *)
module type Responses = sig
val eval_acsl_term_pred: main_ui -> gui_loc -> term_or_pred -> unit -> unit
val left_click_values_computed: main_ui -> localizable -> unit
val right_click_values_computed: main_ui -> menu -> localizable -> unit
end
(** A "no response" module, when the GUI has not been built. *)
module No_Response = struct
let eval_acsl_term_pred _ _ _ () = ()
let left_click_values_computed _ _ = ()
let right_click_values_computed _ _ _ = ()
end
module type Eval = sig
include Gui_eval.S
val display_data_by_callstack:
Analysis.Val.t Gui_callstacks_manager.display_data_by_callstack
end
module Select (Eval: Eval) = struct
let select_loc main_ui ev loc v =
let data, errors = Eval.make_data_all_callstacks ev loc v in
display_eval_errors main_ui errors;
let selection = ev.Eval.expr_to_gui_selection v in
Eval.display_data_by_callstack loc selection data
let is_scalar typ =
match Cil.unrollType typ with
| TInt _ | TEnum _ | TPtr _ | TFloat _ -> true
| _ -> false
let select_lv main_ui loc lv =
if is_scalar (Cil.typeOfLval lv)
then select_loc main_ui Eval.lval_ev loc lv
else select_loc main_ui Eval.lval_as_offsm_ev loc lv
let select_null main_ui loc =
select_loc main_ui Eval.null_ev loc ()
let select_exp main_ui loc exp =
select_loc main_ui Eval.exp_ev loc exp
let select_term main_ui loc t =
select_loc main_ui (Eval.term_ev loc) loc t
let select_tlv main_ui loc tlv =
select_loc main_ui (Eval.tlval_ev loc) loc tlv
let select_predicate main_ui loc p =
select_loc main_ui (Eval.predicate_ev loc) loc p
let select_predicate_with_red main_ui loc a =
select_loc main_ui (Eval.predicate_with_red loc) loc a
let eval_user_term_predicate (main_ui:main_ui) loc tp txt =
let kf = kf_of_gui_loc loc in
try
Gui_callstacks_manager.focus_selection_tab ();
let env = Gui_eval.gui_loc_logic_env loc in
match tp with
| Term -> begin
if txt = "NULL" then
select_null main_ui loc
else
let term = Logic_parse_string.term ~env kf txt in
match term.term_node with
| TLval _ | TStartOf _ -> select_tlv main_ui loc term
| _ -> select_term main_ui loc term
end
| Pred ->
let pred = Logic_parse_string.predicate ~env kf txt in
select_predicate main_ui loc pred
with
| Logic_parse_string.Error (_, mess) ->
main_ui#error "Invalid %a: %s" pp_term_or_pred tp mess
| Parsing.Parse_error ->
main_ui#error "Invalid %a: Parse error" pp_term_or_pred tp
| Eval_terms.LogicEvalError ee ->
main_ui#error "Cannot evaluate %a (%a)"
pp_term_or_pred tp Eval_terms.pretty_logic_evaluation_error ee
| Log.AbortFatal s when s = "kernel" ->
let bt = Printexc.get_backtrace () in
main_ui#error "Invalid %a (see the 'Console' tab for more details)."
pp_term_or_pred tp;
Gui_parameters.debug "%s" bt
| e ->
main_ui#error "Invalid %a: %s" pp_term_or_pred tp (Cmdline.protect e)
let eval_acsl_term_pred main_ui loc tp () =
let txt =
Gtk_helper.input_string ~title:"Evaluate"
~parent:main_ui#main_window
~text:!last_evaluate_acsl_request
(Format.asprintf " Enter an ACSL %a to evaluate "
pp_term_or_pred tp)
in
match txt with
| None -> ()
| Some txt ->
last_evaluate_acsl_request:=txt;
eval_user_term_predicate main_ui loc tp txt
let (main_ui:main_ui) (:menu) csf kf =
try
let aux (:menu) (kf, call_sites) =
let nb_sites = List.length call_sites in
let label = "Go to caller " ^ pretty_kf_escaped kf in
let label =
if nb_sites > 1 then
label ^ " (" ^ (string_of_int nb_sites) ^ " call sites)"
else label
in
let callback () =
let g = Kernel_function.get_global kf in
main_ui#select_or_display_global g;
match call_sites with
| first_call_site :: rest ->
main_ui#view_stmt first_call_site;
let other_call_sites =
List.map (fun call ->
let kf = Kernel_function.find_englobing_kf call in
History.Localizable (PStmt (kf, call))
) rest
in
History.set_forward other_call_sites
| [] -> assert false
in
ignore (menu#add_item ~callback label)
in
let aux_focus (acc_focus, acc_unfocus) (kf, call_sites) =
let focus, unfocus =
List.partition (Gui_callstacks_filters.callsite_matches csf) call_sites
in
(if focus <> [] then (kf, focus) :: acc_focus else acc_focus),
(if unfocus <> [] then (kf, unfocus) :: acc_unfocus else acc_unfocus)
in
let focused, unfocused =
List.fold_left aux_focus ([], []) (Results.callsites kf)
in
List.iter (aux menu) focused;
if unfocused <> [] then
let = GMenu.menu () in
let item =
GMenu.menu_item ~label:"Callers in unselected callstack(s)" ()
in
item#set_submenu submenu;
menu#menu#add item;
let factory = new GMenu.factory submenu in
List.iter (aux factory) unfocused
with Not_found -> ()
let left_click_values_computed main_ui localizable =
try
let open Property in
match localizable with
| PStmt (kf,stmt) ->
if Gui_eval.results_kf_computed kf then
pretty_stmt_info main_ui kf stmt
| PLval (Some kf, Kstmt stmt,lv) ->
if not (Cil.isFunctionType (Cil.typeOfLval lv)) then
select_lv main_ui (GL_Stmt (kf, stmt)) lv
| PLval (Some kf, Kglobal, lv) ->
if not (Cil.isFunctionType (Cil.typeOfLval lv)) then
select_lv main_ui (GL_Pre kf) lv
| PExp (Some kf, Kstmt stmt,e) ->
select_exp main_ui (GL_Stmt (kf, stmt)) e
| PTermLval (Some kf, Kstmt stmt, _, tlv) ->
let term = Logic_const.term (TLval tlv) (Cil.typeOfTermLval tlv) in
select_tlv main_ui (GL_Stmt (kf, stmt)) term
| PTermLval (Some kf, Kglobal, ip, tlv) -> begin
match Gui_eval.classify_pre_post kf ip with
| Some loc ->
let term = Logic_const.term (TLval tlv) (Cil.typeOfTermLval tlv) in
select_tlv main_ui loc term
| None -> ()
end
| PVDecl (Some kf, _, vi) when vi.vformal ->
let lv = (Var vi, NoOffset) in
select_lv main_ui (GL_Pre kf) lv
| PVDecl (Some kf, Kstmt stmt, vi) ->
let lv = (Var vi, NoOffset) in
select_lv main_ui (GL_Stmt (kf, stmt)) lv
| PIP (
IPCodeAnnot {
ica_kf = kf; ica_stmt = stmt;
ica_ca = {
annot_content =
AAssert (_, p) | AInvariant (_, true, p)
} as ca
} as ip) ->
begin
let loc = GL_Stmt (kf, stmt) in
let p = p.tp_statement in
let alarm_or_property =
match Alarms.find ca with
| None -> Red_statuses.Prop ip
| Some a -> Red_statuses.Alarm a
in
select_predicate_with_red main_ui loc (alarm_or_property, p)
end;
| PIP (IPPredicate {ip_kf=kf; ip_kinstr=Kglobal; ip_pred=p} as ip) -> begin
match Gui_eval.classify_pre_post kf ip with
| None -> ()
| Some loc ->
select_predicate_with_red
main_ui loc (Red_statuses.Prop ip, Logic_const.pred_of_id_pred p)
end
| PIP (IPPropertyInstance {ii_kf=kf;ii_stmt=stmt;
ii_pred=Some pred;ii_ip=ip}) ->
let loc = GL_Stmt (kf, stmt) in
select_predicate_with_red main_ui loc
(Red_statuses.Prop ip, Logic_const.pred_of_id_pred pred)
| PLval (None , _, _)
| PExp ((_,Kglobal,_) | (None, Kstmt _, _))
| PTermLval (None, _, _, _)-> ()
| PVDecl (_kf,_ki,_vi) -> ()
| PGlobal _ | PIP _ | PStmtStart _ | PType _ -> ()
with
| Eval_terms.LogicEvalError ee ->
main_ui#pretty_information "Cannot evaluate term: %a@."
Eval_terms.pretty_logic_evaluation_error ee
let right_click_values_computed main_ui localizable =
match localizable with
| PVDecl (Some kf, _, _) ->
let filter = Gui_callstacks_filters.focused_callstacks () in
menu_go_to_callers main_ui menu filter kf
| PStmt (kf,stmt) ->
if Gui_eval.results_kf_computed kf then
ignore
(menu#add_item "_Evaluate ACSL term"
~callback:(eval_acsl_term_pred main_ui (GL_Stmt (kf, stmt)) Term))
| PLval (_kfopt, ki, lv) ->
let ty = Cil.typeOfLval lv in
begin
(match lv with
| Var _,NoOffset when Cil.isFunctionType ty ->
()
| Mem _, NoOffset when Cil.isFunctionType ty -> begin
let e = Eva_utils.lval_to_exp lv in
let state =
match ki with
| Kglobal -> Eval.Analysis.get_global_state ()
| Kstmt stmt -> Eval.Analysis.get_stmt_state ~after:false stmt
in
match state with
| `Bottom | `Top -> ()
| `Value state ->
let funs, _ = Eval.Analysis.eval_function_exp state e in
match funs with
| `Bottom -> ()
| `Value funs ->
menu_go_to_fun_definition main_ui menu funs
end
| _ -> ()
)
end
| PStmtStart _
| PVDecl (None, _, _) | PExp _ | PTermLval _ | PGlobal _ | PIP _
| PType _-> ()
let _right_click_value_not_computed (main_ui:main_ui) (:menu) localizable =
match localizable with
| PVDecl (_,_,_) -> begin
ignore
(menu#add_item "Compute callers"
~callback:(fun () -> (gui_compute_values main_ui)))
end
| _ -> ()
end
let responses_ref = ref (module No_Response: Responses)
let to_do_on_select (:menu) (main_ui:main_ui) ~button selected =
let module Responses = (val !responses_ref) in
if Analysis.is_computed () then
if button = 1 then
Responses.left_click_values_computed main_ui selected
else if button = 3 then
Responses.right_click_values_computed main_ui menu selected
let find_loc kf fdec block =
if block == fdec.sbody then
Some (GL_Pre kf)
else
match block.bstmts with
| [] -> None
| s :: _ -> Some (GL_Stmt (kf, s))
let add_keybord_shortcut_evaluate main_ui =
let selected_loc_for_acsl = ref None in
let () =
Project.register_after_set_current_hook
~user_only:false
(fun _ -> selected_loc_for_acsl := None)
in
let can_eval_acsl_expr_selector _main ~button:_ selected =
let clear () = Gui_callstacks_manager.clear_default () in
let select new_loc =
begin
match new_loc, !selected_loc_for_acsl with
| None, None -> ()
| None, Some _ | Some _, None -> clear ()
| Some new_loc, Some old_loc ->
if not (gui_loc_equal new_loc old_loc) then clear ();
end;
selected_loc_for_acsl := new_loc
in
match selected with
| PStmt (kf, stmt)
| PLval (Some kf, Kstmt stmt, _)
| PExp (Some kf, Kstmt stmt, _)
| PTermLval (Some kf, Kstmt stmt, _, _) ->
if Gui_eval.results_kf_computed kf
then select (Some (GL_Stmt (kf, stmt)))
else select None
| PLval (Some kf, Kglobal, _) ->
if Gui_eval.results_kf_computed kf
then select (Some (GL_Pre kf))
else select None
| PTermLval (Some kf, Kglobal, ip, _) ->
select (Gui_eval.classify_pre_post kf ip)
| PVDecl (Some kf, _, vi) when vi.vformal ->
select (Some (GL_Pre kf))
| PVDecl (Some kf, ki, vi) when not (vi.vformal || vi.vglob) ->
begin
match ki with
| Kstmt stmt ->
select (Some (GL_Stmt (kf, stmt)))
| Kglobal ->
let fdec = Kernel_function.get_definition kf in
let bl = Ast_info.block_of_local fdec vi in
select (find_loc kf fdec bl)
end
| PIP (Property.(IPCodeAnnot {ica_kf = kf; ica_stmt = stmt;
ica_ca = {annot_content =
AAssert _ | AInvariant (_, true, _)}})) ->
select (Some (GL_Stmt (kf, stmt)))
| PIP (Property.(IPPredicate {ip_kf; ip_kinstr=Kglobal} as ip)) ->
select (Gui_eval.classify_pre_post ip_kf ip)
| _ -> select None
in
main_ui#register_source_selector can_eval_acsl_expr_selector;
let accel_group = GtkData.AccelGroup.create () in
let register_accel modi kind =
GtkData.AccelGroup.connect accel_group
~key:GdkKeysyms._E ~modi
~callback:(fun _ ->
match !selected_loc_for_acsl with
| None -> ()
| Some loc ->
let module Responses = (val !responses_ref) in
Responses.eval_acsl_term_pred main_ui loc kind ()
);
in
register_accel [`CONTROL] Term;
register_accel [`CONTROL; `SHIFT] Pred;
main_ui#main_window#add_accel_group accel_group
;;
let reset (main_ui:main_ui) (module A: Analysis.S) =
let module Gui_Types = Gui_types.Make (A.Val) in
let module Gui_Eval = Gui_eval.Make (A) in
Gui_callstacks_filters.register_to_zone_functions (module Gui_Eval);
let module Input = struct
type value = A.Val.t
include Gui_Types
let make_data_for_lvalue lval loc =
fst (Gui_Eval.make_data_all_callstacks Gui_Eval.lval_as_offsm_ev loc lval)
end in
let display_data_by_callstack =
Gui_callstacks_manager.create main_ui (module Input)
in
let module Eval : Eval = struct
include Gui_Eval
let display_data_by_callstack = display_data_by_callstack
end in
let module Responses = Select (Eval) in
responses_ref := (module Responses)
let red_checkbox (panel: GObj.widget) (box: GPack.box) =
let tooltip =
"Panel listing the properties which were invalid for some states"
in
let chk = new Widget.checkbox ~label:"Show list of red alarms" ~tooltip () in
box#pack chk#coerce;
let key_red = "Value.show_red" in
chk#connect (fun b ->
Gtk_helper.Configuration.(set key_red (ConfBool b));
if b then panel#misc#show () else panel#misc#hide ()
);
chk#set (Gtk_helper.Configuration.find_bool ~default:true key_red);
;;
let main (main_ui:main_ui) =
let hide, =
main_ui#file_tree#add_global_filter
~text:"Analyzed by Value only"
~key:"value_hide_unused" hide_unused_function_or_var
in
hide_unused := hide;
main_ui#file_tree#register_reset_extension sync_filetree;
if !hide_unused () then
main_ui#file_tree#reset ()
else
sync_filetree main_ui#file_tree;
reset main_ui (Analysis.current_analyzer ());
Analysis.register_hook (reset main_ui);
Design.register_reset_extension (fun _ -> Gui_callstacks_manager.reset ());
main_ui#register_source_selector (to_do_on_select );
main_ui#register_source_highlighter active_highlighter;
let panel_red = Gui_red.make_panel main_ui in
main_ui#register_panel (value_panel (red_checkbox panel_red));
add_keybord_shortcut_evaluate main_ui;
;;
let () = Design.register_extension main
;;