Source file `VC.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

open Wpo

(* -------------------------------------------------------------------------- *)
(* --- Verification Conditions Interface                                  --- *)
(* -------------------------------------------------------------------------- *)

type t = Wpo.t

let get_id = Wpo.get_gid
let get_model = Wpo.get_model
let get_scope = Wpo.get_scope
let get_context = Wpo.get_context
let get_description = Wpo.get_label
let get_property = Wpo.get_property
let get_sequent w = snd (Wpo.compute w)
let get_result = Wpo.get_result
let get_results = Wpo.get_results
let is_trivial = Wpo.is_trivial
let is_valid = Wpo.is_valid
let is_passed = Wpo.is_passed
let has_unknown = Wpo.has_unknown

let get_formula po =
  WpContext.on_context
    (get_context po) (Wpo.GOAL.compute_proof ~pid:po.po_pid) po.po_formula.goal

let clear = Wpo.clear
let proof = Wpo.goals_of_property
let iter_ip on_goal ip = Wpo.iter ~ip ~on_goal ()
let iter_kf on_goal ?bhv kf =
  match bhv with
  | None ->
    (* iter on all behaviors, see Wpo.iter *)
    Wpo.iter ~index:(Wpo.Function(kf,None)) ~on_goal ()
  | Some bs ->
    List.iter
      (fun b ->
         Wpo.iter ~index:(Wpo.Function(kf,Some b)) ~on_goal ()
      ) bs

let remove = iter_ip Wpo.remove
let () = Property_status.register_property_remove_hook remove

(* -------------------------------------------------------------------------- *)
(* --- Generator Interface                                                --- *)
(* -------------------------------------------------------------------------- *)

let generator model =
  let setup = match model with
    | None -> None
    | Some s -> Some (Factory.parse [s]) in
  Generator.create ~dump:false ?setup ()

let generate_ip ?model ip =
  (generator model)#compute_ip ip

let generate_kf ?model ?bhv ?prop kf =
  let kfs = Kernel_function.Set.singleton kf in
  (generator model)#compute_main ~fct:(Fct_list kfs) ?bhv ?prop ()

let generate_call ?model stmt =
  (generator model)#compute_call stmt

(* -------------------------------------------------------------------------- *)
(* --- Prover Interface                                                   --- *)
(* -------------------------------------------------------------------------- *)

let prove = Prover.prove
let spawn = Prover.spawn ~delayed:true

let server = ProverTask.server
let command ?provers ?tip vcs =
  Register.do_wp_proofs ?provers ?tip vcs

(* -------------------------------------------------------------------------- *)