package frama-c

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

Source file GuiProver.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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).            *)
(*                                                                        *)
(**************************************************************************)

let no_status = `Share "theme/default/never_tried.png"
let ok_status = `Share "theme/default/surely_valid.png"
let ko_status = `Share "theme/default/unknown.png"
let wg_status = `Share "theme/default/surely_invalid.png"
let smoke_status = `Share "theme/default/valid_under_hyp.png"

let filter = function
  | VCS.Qed | VCS.Tactical -> false
  | VCS.Why3 _ -> true

(* -------------------------------------------------------------------------- *)
(* --- Palette Tool                                                       --- *)
(* -------------------------------------------------------------------------- *)

let timeout_for = function
  | VCS.Why3 _ ->
    let value = Wp_parameters.Timeout.get () in
    let spin = new Widget.spinner
      ~tooltip:"Prover Timeout (0 for none)"
      ~min:0 ~step:5 ~value () in
    Some spin
  | _ -> None

let stepout_for = function
  | VCS.Why3 _ ->
    let value = Wp_parameters.Steps.get () in
    let spin = new Widget.spinner
      ~tooltip:"Prover Step Limit (0 for none)"
      ~min:0 ~step:100 ~value () in
    Some spin
  | _ -> None

class prover ~(console:Wtext.text) ~prover =
  let tooltip = "Configure Prover" in
  let content = new Wpane.form () in
  let result = new Widget.label ~style:`Code ~align:`Center ~text:"No Result" () in
  let timeout = timeout_for prover in
  let stepout = stepout_for prover in
  object(self)
    inherit Wpalette.tool ~tooltip ~content:content#widget ()
    initializer
      begin
        assert (filter prover) ;
        content#add_row ~xpadding:6 ~ypadding:4 result#coerce ;
        Wutil.on timeout (fun spin -> content#add_field ~label:"Timeout" spin#coerce) ;
        Wutil.on stepout (fun spin -> content#add_field ~label:"Steps" spin#coerce) ;
      end

    method prover = prover

    method private log wpo res =
      begin
        let fout = Wpo.get_file_logout wpo prover in
        let ferr = Wpo.get_file_logerr wpo prover in
        let lout = Filepath.exists fout in
        let lerr = Filepath.exists ferr in
        if lout || lerr then console#hrule ;
        console#scroll () ;
        console#printf "[%a] %a@.%a" VCS.pp_prover prover
          VCS.pp_result res
          VCS.pp_model res.prover_model ;
        if lout then Command.pp_from_file console#fmt fout ;
        if lerr then Command.pp_from_file console#fmt ferr ;
        if lout || lerr then console#hrule ;
      end

    method private run wpo =
      begin
        let spinner = function None -> None | Some s -> Some s#get in
        let m = Wp_parameters.Memlimit.get () in
        let config = {
          VCS.valid = false ;
          VCS.timeout = Option.map float @@ spinner timeout ;
          VCS.stepout = spinner stepout ;
          VCS.memlimit = if m > 0 then Some m else None ;
        } in
        let result wpo _prv _res = self#update wpo in
        let task = Prover.prove ~config ~result wpo prover in
        let thread = Task.thread task in
        let kill () =
          Wpo.set_result wpo prover VCS.no_result ;
          Task.cancel thread in
        Wpo.set_result wpo prover (VCS.computing kill) ;
        let server = ProverTask.server () in
        Task.spawn server thread ;
        Task.launch server ;
        Wutil.later (fun () -> self#update wpo) ;
      end

    method clear =
      begin
        self#set_status no_status ;
        self#set_action ~icon:`MEDIA_PLAY ~tooltip:"Run Prover" ?callback:None () ;
        Pretty_utils.ksfprintf self#set_label "%a" VCS.pp_prover prover ;
        result#set_text "No Goal" ;
      end

    method update wpo =
      begin
        let res = Wpo.get_result wpo prover in
        result#set_text (Pretty_utils.to_string VCS.pp_result res) ;
        match res.VCS.verdict with
        | VCS.NoResult ->
          let callback () = self#run wpo in
          self#set_status no_status ;
          self#set_action ~icon:`MEDIA_PLAY ~tooltip:"Run Prover" ~callback () ;
        | VCS.Computing callback ->
          self#set_status `EXECUTE ;
          self#set_action ~tooltip:"Interrrupt Prover" ~icon:`STOP ~callback () ;
          Pretty_utils.ksfprintf self#set_label "%a (...)" VCS.pp_prover prover ;
        | VCS.Valid ->
          let callback () = self#run wpo in
          self#set_status ok_status ;
          self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
          Pretty_utils.ksfprintf self#set_label "%a (%a)" VCS.pp_prover prover
            Rformat.pp_time res.VCS.prover_time ;
        | VCS.Unknown | VCS.Timeout | VCS.Stepout | VCS.Invalid ->
          let callback () = self#run wpo in
          self#set_status ko_status ;
          self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
          Pretty_utils.ksfprintf self#set_label "%a (?)" VCS.pp_prover prover ;
        | VCS.Failed ->
          let callback () = self#log wpo res in
          self#set_status `DIALOG_WARNING ;
          self#set_action ~tooltip:"Dump Logs" ~icon:`FILE ~callback () ;
          Pretty_utils.ksfprintf self#set_label "%a (failed)" VCS.pp_prover prover ;
      end

  end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct