package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
850
851
852
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

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

(* Collect all properties that have a status *)
let all_properties () =
  let globals = ref Property.Set.empty in
  let functions = ref Kernel_function.Map.empty in
  (* Dispatch properties into globals and per-function map *)
  Property_status.iter
    (fun ip ->
       match Property.get_kf ip with
       | None -> globals := Property.Set.add ip !globals
       | Some kf ->
         if not (Ast_info.is_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 (* TODO: it would be great to find the location
                                             of global invariants or lemmas, but there isn't
                                             enough information in the ast *)
    | 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 (* used to compare checks *);
    add: GPack.box -> unit;
    get: unit -> bool;
    set: bool -> unit;
    reset: unit -> unit (* change to default state if needed *);
  }

  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 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
  (* Function to be called during the idle time of the GUI *)
  let refreshers = ref []
  let add_refresher f = refreshers := f::!refreshers
  let set_refresh_needed = ref (fun _ -> (*will be defined later*)())
  let apply () =
    List.iter (fun f -> f ()) !refreshers

  type check = {
    id: int (* unique ID, used to compare checks *);
    add: GPack.box -> unit (* pack the corresponding checkbox in the argument*);
    get: unit -> bool (* state of the checkbox (set/unset *) ;
    set: bool -> unit (* change checkbox state *) ;
    reset: unit -> unit (* change to default state if needed *);
  }

  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

  (* ref below used by [add] to set the configuration, since it must be delayed
     until the session directory has been set *)
  let first_extended_ref = ref true

  (* This function must always be called at OCaml toplevel, because it registers
     a new Frama-C state. *)
  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 () ->
           (* avoid loading the configuration file several times *)
           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" ()
  (* Function called when RTEs are enabled or disabled. *)
  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 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 () -> (* Save expansion of panels*)
                  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

  (* [list_alarms] is the instantiation of [add] for all the various kind
     of alarms. It is computed by ad hoc introspection on the reprs field of the
     datatype. [active_alarm] finds the category of the alarm, and returns
     whether it should be shown according to the corresponding checkbox. *)
  let list_alarms, active_alarm =
    (*[h] maps alarms hints to the corresponding [get] checkbox. *)
    let h = Datatype.String.Hashtbl.create 16 in
    let aux alarm = (* instantiates [add] for the category of [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 (* should not happen *)
    in
    List.map aux Alarms.reprs, active_alarm

  let pack (box:GPack.box) =
    (*    let hb = make_expand box
            ~tooltip:"Locations of the properties that are shown" "Where"
          in *)
    onlyCurrent.add (*hb*) 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;
    lemmas.add hb;
    typeInvariants.add hb;
    globalInvariants.add hb;
    instances.add hb;
    other.add hb;
    reachable.add hb;
    (*Pragma.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;
    (* Register additional callbacks *)
    set_rte :=
      (fun b ->
         hb_category#misc#set_sensitive b;
         if not b then expand_category#set_expanded false);
    !set_rte (rte.get ()) (* For the initial state *);
  ;;

end

open Refreshers

(* Process the rte statuses for the given kf, and add the result in the
   accumulator. Filter the statuses according to user-selected filters*)
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 ->
    (* Considered that leaf functions are not verified internally *)
    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
(* Used to change dynamically the label of the "Properties" tab. *)

(* Lists of checkboxes (used by popup menus) *)
(* all checks:
   preconditions; ensures; behaviors; allocations; assigns; from;
   assertions; invariant; variant; terminates; stmtSpec; axiomatic;
   typeInvariants; globalInvariants; instances; other; reachable; valid;
   validHyp; unknown; invalid; invalidHyp; considered_valid; untried; dead;
   inconsistent; rteNotGenerated; rteGenerated *)

(* [reset_checks to_check to_uncheck] sets all checks in [to_check] and
   unsets all checks in [to_uncheck], then refreshes the view. *)
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");

  (* button to modify all checkboxes according to presets *)
  let checks_menu = 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 reset_menu_button =
    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
  (* TODO: this avoids some problems when changing projects, where
     the property navigator displays outdated information. A better solution
     would be to projectify what is being displayed *)
  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));
             (* Note: the code below generates double scrolling:
                the previous call to main_ui#scroll causes the original source
                viewer to scroll to the beginning of the function, and then
                the code below re-scrolls it to the exact statement. *)
             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

  (* Function name column viewer *)
  make_view_column (GTree.cell_renderer_text [top])
    (function{function_name=m} -> [`TEXT m])
    ~title:"Function";

  (* Module name column viewer *)
  make_view_column (GTree.cell_renderer_text [top])
    (function{module_name=m} -> [`TEXT (Filepath.Normalized.to_pretty_string m)])
    ~title:"File";

  (* Kind name column viewer *)
  make_view_column (GTree.cell_renderer_text [top])
    (function{kind=k} -> [`TEXT k])
    ~title:"Kind";

  (* Status colored column viewer *)
  make_view_column (GTree.cell_renderer_pixbuf [top])
    (function {status_icon=status_icon} ->
       [`PIXBUF (Gtk_helper.Icon.get status_icon)])
    ~title:"Status";

  (* Consolidated status name column viewer *)
  make_view_column (GTree.cell_renderer_text [top])
    (function{consolidated_status_name=k}-> [`TEXT k])
    ~title:"Consolidated Status";

  (* (Local) status name column viewer *)
  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 ())
    | 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 {ica_ca={annot_content = APragma p}} ->
      Logic_utils.is_property_pragma p (* currently always false. *)
    | IPCodeAnnot _ -> false (* status of inner nodes *)
    | 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
    (* Add global properties at the top of the list *)
    Property.Set.iter add_ip globals;

    (* Will the results for this kf be ultimately displayed *)
    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
    (* All non-filtered RTE statuses for a given function *)
    let rte_kf kf = List.fold_left (aux_rte kf) [] rte_get_all_statuses in
    (* Add RTE statuses for all functions. We cannot simply iterate over
       [by_kf], as functions without any property will not be present in it *)
    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
    (* Sort functions by names, in a case-insensitive way *)
    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

    (* Add the properties for all the relevant functions *)
    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);

  (* To fill at startup:
     let (_:GtkSignal.id) = view#misc#connect#after#realize fill_model in *)
  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 ())

(* Graphical markers in text showing the status of properties.
   Aka. "bullets" in left margin *)
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
    (* We separate the consolidated statuses of the preconditions inside
       guarded behaviors from those outside. For guarded behaviors, since we
       do not keep track of the status of 'assumes' clauses, we cannot know
       if they are active. Hence, we must weaken any 'Invalid' status into
       'Unknown'. *)
    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 ->
          (* Weaken if the invalidity comes from [ips_unsure]. We do nothing
             for statuses [Invalid] (a path should exist, hence the behavior
             must be active), or [Invalid_but_dead] (equivalent to [True]) *)
          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
      (* Positioning the bullet is tricky. We cannot use [start] as offset,
         because the bullet ends up at the beginning of the spec (assertions,
         contracts, etc) instead of in front of the function name. We use
         the beginning of the C part of the statement (which has been computed
         when the source was rendered). *)
      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 (* fallback *)
      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;
  (* There is a hack here. We need to access the state of
     [main_ui#reactive_buffer] inside [highlighter], but it is not an argument
     of the callback. Instead, we pass [main_ui] as an additional argument.
     This only works because there is only one instance of [main_ui]. *)
  main_ui#register_source_highlighter highlighter

let () = Design.register_extension extend

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