Source file property_navigator.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
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
module Rte = struct
type status_accessor =
string
* (Cil_types.kernel_function -> bool -> unit)
* (Cil_types.kernel_function -> bool)
let get_all_status: (unit -> status_accessor list) option ref = ref None
let register_get_all_status getter = get_all_status := Some getter
end
open Design
open Cil_types
open Property_status
let all_properties () =
let globals = ref Property.Set.empty in
let functions = ref Kernel_function.Map.empty in
Property_status.iter
(fun ip ->
match Property.get_kf ip with
| None -> globals := Property.Set.add ip !globals
| Some kf ->
if not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
with Not_found ->
let ips = Property.Set.singleton ip in
functions := Kernel_function.Map.add kf (ref ips) !functions
);
!functions, !globals
type property = {
module_name:Datatype.Filepath.t;
function_name:string;
kind:string;
status_name:string;
consolidated_status:Consolidation.consolidated_status option;
consolidated_status_name:string;
status_icon:Gtk_helper.Icon.kind;
visible:bool;
ip: Property.t;
}
let kf_name_and_module kf =
let name = Kernel_function.get_name kf in
let loc = Kernel_function.get_location kf in
let file = (fst loc).Filepath.pos_path in
name, file
let make_property ip =
let status = Property_status.get ip in
let status_name = Format.asprintf "%a" Property_status.pretty status in
let con_status = Consolidation.get ip in
let consolidated_status_name =
Format.asprintf "%a" Consolidation.pretty con_status
in
let function_name, module_name = match Property.get_kf ip with
| None -> "", Datatype.Filepath.dummy
| Some kf -> kf_name_and_module kf
in
let kind =
Format.asprintf "@[<hov>%a@]" Property.pretty ip
in
let status_icon = Gtk_helper.Icon.Feedback (Feedback.get ip) in
{
module_name = module_name;
function_name = function_name;
visible = true;
ip=ip; kind=kind;
status_name = status_name ;
consolidated_status = Some con_status ;
consolidated_status_name = consolidated_status_name ;
status_icon = status_icon ;
}
module Refreshers: sig
type check = {
id: int ;
add: GPack.box -> unit;
get: unit -> bool;
set: bool -> unit;
reset: unit -> unit ;
}
val onlyCurrent: check
val ensures: check
val extended: check
val preconditions: check
val behaviors: check
val complete_disjoint: check
val allocations: check
val assigns: check
val from: check
val user_assertions: check
val user_checks: check
val user_admits: check
val rte: check
val invariant: check
val variant: check
val terminates: check
val stmtSpec: check
val reachable: check
val other: check
val instances: check
val lemmas: check
val axiomatic: check
val modules: check
val typeInvariants: check
val globalInvariants: check
val rteNotGenerated: check
val rteGenerated: check
val valid: check
val validHyp: check
val unknown: check
val invalid: check
val invalidHyp: check
val considered_valid: check
val untried: check
val dead: check
val inconsistent: check
val active_alarm: Alarms.t -> bool
val pack: GPack.box -> unit
val set_refresh_needed : (bool -> unit) ref
val apply: unit -> unit
val all_checks : unit -> check list
end
=
struct
let refreshers = ref []
let add_refresher f = refreshers := f::!refreshers
let set_refresh_needed = ref (fun _ -> ())
let apply () =
List.iter (fun f -> f ()) !refreshers
type check = {
id: int ;
add: GPack.box -> unit ;
get: unit -> bool ;
set: bool -> unit ;
reset: unit -> unit ;
}
let last_id = ref 0
let next_id () = incr last_id; !last_id
let checks : check list ref = ref []
let all_checks () = List.rev !checks
let first_extended_ref = ref true
let add ~name ~hint ?(default=true) ?(set=(fun _b -> ())) () =
let open Gtk_helper in
let key_name =
String.map
(fun c -> if c < 'A' || c > 'z' || (c > 'Z' && c < 'a') then '_' else c)
name
in
let key_name = "property_panel." ^ key_name in
let module M = State_builder.Ref
(Datatype.Bool)
(struct
let name = "show " ^ name
let dependencies = []
let default () = default
end)
in
let get = M.get in
let () =
Cmdline.run_after_extended_stage
(fun () ->
if !first_extended_ref then begin
first_extended_ref := false;
Configuration.load ()
end);
Cmdline.run_after_loading_stage
(fun () ->
let v = Configuration.find_bool ~default key_name in
M.set v)
in
let set v =
Configuration.set key_name (Configuration.ConfBool v);
set v;
!set_refresh_needed true;
M.set v
in
let add hb = add_refresher
(Gtk_helper.on_bool ~tooltip:hint hb name get set)
in
let reset () = if get () <> default then set default in
let chk = { id = next_id(); get; set; add; reset } in
checks := chk :: !checks;
chk
let hint_rte hint =
if Option.is_some !Rte.get_all_status then hint
else hint ^ " (but RteGen plugin is inactive)"
let onlyCurrent = add ~name:"Current function" ~default:false
~hint:"Only show properties related to current function" ()
let preconditions = add ~name:"Preconditions"
~hint:"Show function preconditions" ()
let ensures = add ~name:"Postconditions"
~hint:"Show function postconditions" ()
let extended = add ~name:"Extended"
~hint:"Show extended function annotation" ()
let behaviors = add ~name:"Behaviors" ~default:false
~hint:"Show function behaviors" ()
let complete_disjoint = add ~name:"Complete/disjoint"
~hint:"Show complete/disjoint behaviors" ()
let allocations = add ~name:"Allocations"
~hint:"Show function allocations" ()
let assigns = add ~name:"Assigns"
~hint:"Show function assigns" ()
let from = add ~name:"From" ()
~hint:"Show functional dependencies in function assigns"
let user_assertions =
add ~name:"User assertions" ~hint:"Show user assertions" ()
let user_checks =
add ~name:"User checks" ~hint:"Show user checks" ()
let user_admits =
add ~name:"User admits" ~hint:"Show user hypotheses" ()
let set_rte = ref (fun _b -> ())
let rte = add ~set:(fun b -> !set_rte b) ~name:"RTEs"
~hint:(hint_rte "Show runtime errors") ()
let invariant = add ~name:"Invariant"
~hint:"Show loop invariants" ()
let variant = add ~name:"Variant"
~hint:"Show loop termination argument" ()
let terminates = add ~name:"Terminates"
~hint:"Show function termination clauses" ()
let stmtSpec = add ~name:"Stmt contract"
~hint:"Show statement contracts" ()
let lemmas = add ~name:"Lemmas"
~hint:"Show lemmas" ()
let axiomatic = add ~name:"Axiomatic" ~default:false
~hint:"Show global axiomatics" ()
let modules = add ~name:"Module" ~default:false
~hint:"Show global modules" ()
let instances = add ~name:"Instances"
~hint:"Show properties that are instances of root properties" ()
let typeInvariants = add ~name:"Type invariants"
~hint:"Show type invariants" ()
let globalInvariants = add ~name:"Global invariants"
~hint:"Show global invariants" ()
let other = add ~name:"Other"
~hint:"Show other properties" ()
let reachable = add ~default:false ~name:"Reachable"
~hint:"Show 'reachable' hypotheses" ()
let rteNotGenerated = add ~default:false ~name:"Non generated"
~hint:(hint_rte "Show RTEs assertions that remain to generate") ()
let rteGenerated = add ~default:false ~name:"Generated"
~hint:(hint_rte "Show RTEs assertions that have been generated") ()
let valid = add ~name:"Valid"
~hint:"Show properties that are proven valid" ()
let validHyp = add ~name:"Valid under hyp."
~hint:"Show properties that are are valid, but depend on some hypotheses"
()
let unknown = add ~name:"Unknown"
~hint:"Show properties with an 'unknown' status" ()
let invalid = add ~name:"Invalid"
~hint:"Show properties that are proven invalid" ()
let invalidHyp = add ~name:"Invalid under hyp."
~hint:"Show properties that are are invalid, but depend on \
some hypotheses" ()
let considered_valid = add ~name:"Considered valid" ~default:false
~hint:"Show properties that are considered valid because \
the platform has no way to prove them" ()
let untried = add ~name:"Untried" ~default:false
~hint:"Show properties whose proof has not been attempted" ()
let dead = add ~name:"Dead" ~default:false
~hint:"Show properties on unreachable code" ()
let inconsistent = add ~name:"Inconsistent"
~hint:"Show properties that have an inconsistent status" ()
let make_expand (box:GPack.box) ?tooltip text =
let key_config = "Properties." ^ text in
let expanded =Gtk_helper.Configuration.find_bool ~default:true key_config in
let expander = GBin.expander ~expanded ~packing:box#pack () in
ignore (expander#connect#activate
~callback:(fun () ->
Gtk_helper.Configuration.set key_config
(Gtk_helper.Configuration.ConfBool (not expander#expanded))));
let hb = GPack.vbox ~packing:expander#add () in
let markup = Printf.sprintf "<span font_weight=\"bold\">%s</span>" text in
let label = GMisc.label ~markup () in
Gtk_helper.do_tooltip ?tooltip label;
expander#set_label_widget label#coerce;
hb, expander
let list_alarms, active_alarm =
let h = Datatype.String.Hashtbl.create 16 in
let aux alarm =
let name = Alarms.get_short_name alarm in
let hint = Alarms.get_description alarm in
let ({get} as check) = add ~name ~hint () in
Datatype.String.Hashtbl.add h (Alarms.get_short_name alarm) get;
check
in
let active_alarm alarm =
try (Datatype.String.Hashtbl.find h (Alarms.get_short_name alarm)) ()
with Not_found ->
Gui_parameters.warning "Unregistered alarm type";
true
in
List.map aux Alarms.reprs, active_alarm
let pack (box:GPack.box) =
onlyCurrent.add box;
let hb, _ = make_expand box
~tooltip:"Validity status of the properties that are shown" "Status"
in
valid.add hb;
validHyp.add hb;
unknown.add hb;
invalid.add hb;
invalidHyp.add hb;
considered_valid.add hb;
untried.add hb;
dead.add hb;
inconsistent.add hb;
let hb, _ = make_expand box
~tooltip:"Which properties (precondition, assertion, etc) are shown"
"Kind"
in
preconditions.add hb;
ensures.add hb;
extended.add hb;
behaviors.add hb;
complete_disjoint.add hb;
allocations.add hb;
assigns.add hb;
from.add hb;
user_assertions.add hb;
user_checks.add hb;
user_admits.add hb;
rte.add hb;
invariant.add hb;
variant.add hb;
terminates.add hb;
stmtSpec.add hb;
axiomatic.add hb;
modules.add hb;
lemmas.add hb;
typeInvariants.add hb;
globalInvariants.add hb;
instances.add hb;
other.add hb;
reachable.add hb;
let hb_category, expand_category = make_expand box
~tooltip:"Category of runtime errors leading to the emission of an \
assertion. Enabled only when RTEs are displayed."
"RTE category"
in
List.iter (fun check_alarm -> check_alarm.add hb_category) list_alarms;
let hb, _ = make_expand box
~tooltip:"Whether assertions against runtime errors of a certain class \
have been generated"
"RTE emission"
in
rteNotGenerated.add hb;
rteGenerated.add hb;
set_rte :=
(fun b ->
hb_category#misc#set_sensitive b;
if not b then expand_category#set_expanded false);
!set_rte (rte.get ()) ;
;;
end
open Refreshers
let aux_rte kf acc (name, _, rte_status_get: Rte.status_accessor) =
let st = rte_status_get kf in
match st, rteGenerated.get (), rteNotGenerated.get () with
| true, true, _
| false, _, true ->
let status_name, status =
if st then
if Kernel_function.is_definition kf
then "Generated", Feedback.Valid
else "Considered generated", Feedback.Considered_valid
else "Not generated", Feedback.Invalid
in
let function_name, module_name = kf_name_and_module kf in
let status_icon = Gtk_helper.Icon.Feedback status in
let ip =
Property.ip_other name
(Property.OLGlob (Kernel_function.get_location kf))
in
{
module_name = module_name;
function_name = function_name;
visible = true;
ip=ip;
kind=Format.asprintf "@[<hov>%a@]" Property.pretty ip;
status_name = "" ;
consolidated_status = None ;
consolidated_status_name = status_name ;
status_icon = status_icon ;
} :: acc
| true, false, _
| false, _, false -> acc
let properties_tab_label = ref None
let reset_checks to_check to_uncheck =
List.iter (fun chk -> chk.set true) to_check;
List.iter (fun chk -> chk.set false) to_uncheck;
Refreshers.apply ()
let reset_checks_default () =
List.iter (fun chk -> chk.reset ()) (all_checks ());
Refreshers.apply ()
let unproven_checks_true = [unknown; invalid; invalidHyp; inconsistent]
let unproven_checks_false = [valid; validHyp; considered_valid; untried; dead]
let check_default () = reset_checks_default ()
let check_unproven () = reset_checks unproven_checks_true unproven_checks_false
let check_all () = reset_checks (all_checks ()) []
let check_none () = reset_checks [] (all_checks ())
let make_panel (main_ui:main_window_extension_points) =
let container = GPack.hbox () in
let vb_left = GPack.vbox ~packing:container#pack () in
let hb_refresh_reset = GPack.hbox ~packing:vb_left#pack () in
let refresh_button =
GButton.button ~packing:(hb_refresh_reset#pack ~expand:true) ()
in
let refresh_label = GMisc.label ~markup:"<b>Refresh</b>" () in
refresh_button#add refresh_label#coerce;
Refreshers.set_refresh_needed :=
(fun b ->
if b then refresh_label#set_label "<b>Refresh</b>"
else refresh_label#set_label "Refresh");
let = GMenu.menu () in
let mi_check_def = GMenu.menu_item ~label:"Reset all filters to default" () in
checks_menu#add mi_check_def;
ignore (mi_check_def#connect#activate ~callback:(fun () -> check_default ()));
let mi_check_unproven =
GMenu.menu_item ~label:"Reset 'Status' filters to show only unproven/invalid" ()
in
checks_menu#add mi_check_unproven;
ignore (mi_check_unproven#connect#activate
~callback:(fun () -> check_unproven ()));
let mi_check_all =
GMenu.menu_item ~label:"Select all" ()
in
checks_menu#add mi_check_all;
ignore (mi_check_all#connect#activate
~callback:(fun () -> check_all ()));
let mi_check_none =
GMenu.menu_item ~label:"Unselect all" ()
in
checks_menu#add mi_check_none;
ignore (mi_check_none#connect#activate
~callback:(fun () -> check_none ()));
let icon = GMisc.image ~stock:`INDEX () in
let =
GButton.button ~packing:(hb_refresh_reset#pack ~expand:false) ()
in
reset_menu_button#misc#set_tooltip_text "Reconfigure filters according to presets";
reset_menu_button#add icon#coerce;
ignore (reset_menu_button#connect#clicked
~callback:(fun () -> checks_menu#popup ~button:0
~time:(GtkMain.Main.get_current_event_time ())));
let sc_buttons =
GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`NEVER ()
in
let vb = GPack.vbox () in
Refreshers.pack vb;
sc_buttons#add_with_viewport vb#coerce;
vb_left#add sc_buttons#coerce;
let module MODEL =
Gtk_helper.MAKE_CUSTOM_LIST(struct type t = property end)
in
let model = MODEL.custom_list () in
let append m = if m.visible then model#insert m in
let clear () = model#clear () in
Design.register_reset_extension (fun _ -> clear ();
match !properties_tab_label with
| None -> ()
| Some label ->
GtkMisc.Label.set_text label "Properties"
);
let sc =
GBin.scrolled_window
~vpolicy:`AUTOMATIC
~hpolicy:`AUTOMATIC
~packing:(container#pack ~expand:true ~fill:true)
()
in
let view = GTree.view
~rules_hint:true
~headers_visible:true
~packing:sc#add ()
in
view#selection#set_select_function
(fun path currently_selected ->
if not currently_selected then
begin match model#custom_get_iter path with
| Some {MODEL.finfo={ip = ip;}} ->
ignore (main_ui#scroll (Printer_tag.PIP ip));
main_ui#view_original (Property.location ip)
| None -> ()
end;
true);
let top = `YALIGN 0.0 in
let make_view_column renderer properties ~title =
let cview = MODEL.make_view_column model renderer properties ~title in
cview#set_resizable true;
ignore (view#append_column cview)
in
make_view_column (GTree.cell_renderer_text [top])
(function{function_name=m} -> [`TEXT m])
~title:"Function";
make_view_column (GTree.cell_renderer_text [top])
(function{module_name=m} -> [`TEXT (Filepath.Normalized.to_pretty_string m)])
~title:"File";
make_view_column (GTree.cell_renderer_text [top])
(function{kind=k} -> [`TEXT k])
~title:"Kind";
make_view_column (GTree.cell_renderer_pixbuf [top])
(function {status_icon=status_icon} ->
[`PIXBUF (Gtk_helper.Icon.get status_icon)])
~title:"Status";
make_view_column (GTree.cell_renderer_text [top])
(function{consolidated_status_name=k}-> [`TEXT k])
~title:"Consolidated Status";
make_view_column (GTree.cell_renderer_text [top])
(function{status_name=k}-> [`TEXT k])
~title:"Local Status";
view#set_model (Some model#coerce);
let visible ip =
let open Property in match ip with
| IPOther _ -> other.get ()
| IPReachable _ -> reachable.get ()
| IPBehavior {ib_kinstr=Kglobal} -> behaviors.get ()
| IPBehavior {ib_kinstr=Kstmt _} -> behaviors.get () && stmtSpec.get ()
| IPPredicate {ip_kind=PKRequires _;ip_kinstr=Kglobal} ->
preconditions.get ()
| IPPredicate {ip_kind=PKRequires _;ip_kinstr=Kstmt _} ->
preconditions.get () && stmtSpec.get ()
| IPPredicate {ip_kind = PKAssumes _} -> false
| IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kglobal} -> ensures.get ()
| IPExtended _ -> extended.get ()
| IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kstmt _} ->
ensures.get() && stmtSpec.get()
| IPPredicate {ip_kind = PKTerminates} -> terminates.get ()
| IPTypeInvariant _ -> typeInvariants.get()
| IPGlobalInvariant _ -> globalInvariants.get()
| IPAxiomatic _ -> axiomatic.get () && not (onlyCurrent.get ())
| IPModule _ -> modules.get () && not (onlyCurrent.get ())
| IPLemma _ -> lemmas.get ()
| IPComplete _ -> complete_disjoint.get ()
| IPDisjoint _ -> complete_disjoint.get ()
| IPCodeAnnot {ica_ca={annot_content=AAssert(_, {tp_kind})} as ca} ->
begin
match Alarms.find ca with
| Some a -> rte.get () && active_alarm a
| None ->
match tp_kind with
| Assert -> user_assertions.get ()
| Check -> user_checks.get ()
| Admit -> user_admits.get ()
end
| IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
| IPCodeAnnot _ -> false
| IPAllocation {ial_kinstr=Kglobal} -> allocations.get ()
| IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_loop _} ->
allocations.get ()
| IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_contract _} ->
allocations.get() && stmtSpec.get()
| IPAssigns {ias_kinstr=Kglobal} -> assigns.get ()
| IPAssigns {ias_kinstr=Kstmt _;ias_bhv=Id_loop _} ->
assigns.get ()
| IPAssigns {ias_kinstr=Kstmt _;ias_bhv=Id_contract _} ->
assigns.get() && stmtSpec.get()
| IPFrom _ -> from.get ()
| IPDecrease _ -> variant.get ()
| IPPropertyInstance _ -> instances.get ()
in
let visible_status_aux = function
| Consolidation.Never_tried -> untried.get ()
| Consolidation.Considered_valid -> considered_valid.get ()
| Consolidation.Valid _ -> valid.get ()
| Consolidation.Valid_under_hyp _ -> validHyp.get ()
| Consolidation.Unknown _ -> unknown.get ()
| Consolidation.Invalid _ -> invalid.get ()
| Consolidation.Invalid_under_hyp _ -> invalidHyp.get ()
| Consolidation.Invalid_but_dead _
| Consolidation.Valid_but_dead _
| Consolidation.Unknown_but_dead _ -> dead.get ()
| Consolidation.Inconsistent _ -> inconsistent.get ()
in
let visible_status = Option.fold ~some:visible_status_aux ~none:true in
let fill_model () =
let add_ip ip =
if visible ip then
let p = make_property ip in
if visible_status p.consolidated_status then append p
in
let by_kf, globals = all_properties () in
Property.Set.iter add_ip globals;
let display kf =
not (Cil_builtins.is_unused_builtin (Kernel_function.get_vi kf)) &&
not (onlyCurrent.get ()) ||
(let kfvi = Kernel_function.get_vi kf in
List.exists
(function
| GFun ({svar = fvi},_) | GFunDecl (_, fvi, _) ->
Cil_datatype.Varinfo.equal fvi kfvi
| _ -> false
) main_ui#file_tree#selected_globals)
in
let rte_get_all_statuses = match !Rte.get_all_status with
| None -> []
| Some registered_getter -> registered_getter ()
in
let rte_kf kf = List.fold_left (aux_rte kf) [] rte_get_all_statuses in
let with_rte =
let aux kf acc =
if display kf then
let props =
try !(Kernel_function.Map.find kf by_kf)
with Not_found -> Property.Set.empty
in
(kf, (props, rte_kf kf)) :: acc
else acc
in
Globals.Functions.fold aux []
in
let cmp (k1, _) (k2, _) =
Extlib.compare_ignore_case
(Kernel_function.get_name k1) (Kernel_function.get_name k2)
in
let by_kf = List.sort cmp with_rte in
List.iter
(fun (kf, (ips, rtes)) ->
if display kf then begin
Property.Set.iter add_ip ips;
List.iter append rtes;
end
) by_kf;
match !properties_tab_label with
| None -> ()
| Some label ->
let text = Format.sprintf "Properties (%d)" (model#custom_iter_n_children None) in
GtkMisc.Label.set_text label text
in
ignore
(let callback _ =
main_ui#protect ~cancelable:false
(fun () ->
clear ();
Refreshers.apply ();
!Refreshers.set_refresh_needed false;
fill_model ())
in
refresh_button#connect#released ~callback);
let tab_label = (GMisc.label ~text:"Properties" ())#coerce in
properties_tab_label := Some (GtkMisc.Label.cast tab_label#as_widget);
let (_:int) = main_ui#lower_notebook#append_page
~tab_label (container#coerce)
in
register_reset_extension (fun _ -> Refreshers.apply ())
let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
match localizable with
| Printer_tag.PIP ppt ->
if Property.has_status ppt then
Design.Feedback.mark
buffer#buffer ~offset:start (Property_status.Feedback.get ppt)
| PStmt(_,({ skind=Instr(Call _| Local_init (_, ConsInit _, _)) } as stmt)) ->
let kfs = Statuses_by_call.all_functions_with_preconditions stmt in
let filter (ip_src, _ip_copy) =
match ip_src with
| Property.IPPredicate {Property.ip_kind=Property.PKRequires bhv} ->
bhv.b_assumes = []
| _ -> false
in
let ips_sure, ips_unsure = Kernel_function.Hptset.fold
(fun kf (ips_sure, ips_unsure) ->
Statuses_by_call.setup_all_preconditions_proxies kf;
let ips_kf =
Statuses_by_call.all_call_preconditions_at ~warn_missing:false kf stmt
in
let ips_kf_sure, ips_kf_unsure = List.partition filter ips_kf in
(List.map snd ips_kf_sure @ ips_sure),
(List.map snd ips_kf_unsure @ ips_unsure))
kfs ([], [])
in
let ips = ips_sure @ ips_unsure in
if ips <> [] then
let validity = Property_status.Feedback.get_conjunction ips in
let validity =
match validity with
| Feedback.Invalid_under_hyp ->
let invalid ip = Feedback.get ip = Feedback.Invalid_under_hyp in
if List.exists invalid ips_unsure &&
not (List.exists invalid ips_sure)
then Feedback.Unknown
else validity
| _ -> validity
in
let offset =
try Pretty_source.stmt_start buffer#locs stmt
with Not_found ->
Gui_parameters.error
"Invalid internal state for statement %d" stmt.sid;
stop
in
Design.Feedback.mark buffer#buffer ~call_site:stmt ~offset validity
| PStmt _ | PStmtStart _ | PGlobal _| PVDecl _ | PTermLval _| PLval _
| PExp _ | PType _ -> ()
let extend (main_ui:main_window_extension_points) =
make_panel main_ui;
main_ui#register_source_highlighter highlighter
let () = Design.register_extension extend