package frama-c

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

Source file wpTarget.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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

module Fct = Cil_datatype.Kf.Set

module TargetKfs =
  State_builder.Set_ref
    (Fct)
    (struct
      let dependencies = [ Ast.self ]
      let name = "WpTarget.TargetKfs"
    end)

let get_called_stmt stmt =
  match stmt.skind with
  | Instr (Call(_, fct, _, _)) ->
    begin match Kernel_function.get_called fct with
      | Some kf -> [kf]
      | None -> Option.value ~default:[] @@ Option.map snd (Dyncall.get stmt)
    end
  | Instr (Local_init (_,ConsInit(vi,_,_),_)) -> [ Globals.Functions.get vi ]
  | _ -> []

module Callees =
  State_builder.Hashtbl
    (Cil_datatype.Kf.Hashtbl)
    (Fct)
    (struct
      let dependencies = [Ast.self]
      let name = "WpTarget.Callees"
      let size = 17
    end)

(** Note: we add the kf received in parameter in the set only if it has a
    definition (and thus if it does not have one, we add nothing as it has
    no visible callee).

    This prevent to warn on prototypes that have a contract but are unused. If
    the function is used, it will be added to the set via its caller(s) if they
    are under verification.
*)
let with_callees kf =
  try
    let stmts = (Kernel_function.get_definition kf).sallstmts in
    let fold s stmt =
      List.fold_left (fun s kf -> Fct.add kf s) s (get_called_stmt stmt)
    in
    List.fold_left fold (Fct.singleton kf) stmts
  with Kernel_function.No_Definition -> Fct.empty

let with_callees = Callees.memo with_callees

let add_with_callees kf =
  let add kf =
    let insert_spec kf =
      let specs =
        if Kernel_function.has_definition kf
        then [ `Exits ; `Terminates ]
        else [ `Exits ; `Terminates ; `Assigns ]
      in
      Populate_spec.populate_funspec ~do_body:true kf specs
    in
    insert_spec kf ;
    TargetKfs.add kf
  in
  Fct.iter add (with_callees kf)

exception Found

let check_properties behaviors props kf =
  let open Property in
  let exists_selected_behavior l =
    behaviors = [] || List.exists (fun b -> List.mem b behaviors) l
  in
  let check_ip ip =
    if exists_selected_behavior (WpPropId.user_bhv_names ip) then
      let names = WpPropId.user_prop_names ip in
      if props = [] || WpPropId.are_selected_names props names then raise Found
  in
  let check_bhv_requires kf kinstr bv =
    List.iter (fun p -> check_ip (ip_of_requires kf kinstr bv p)) bv.b_requires
  in
  let check_bhv_ensures kf kinstr bv =
    List.iter (fun p -> check_ip (ip_of_ensures kf kinstr bv p)) bv.b_post_cond
  in
  let opt_check = function None -> () | Some p -> check_ip p in
  let check_bhv_assigns kf kinstr bv =
    opt_check (ip_assigns_of_behavior kf kinstr ~active:[] bv)
  in
  let check_bhv_allocation kf kinstr bv =
    opt_check (ip_allocation_of_behavior kf kinstr ~active:[] bv)
  in
  let check_complete_disjoint kf kinstr =
    try
      let spec = Annotations.funspec kf in
      let comp = ip_complete_of_spec kf kinstr ~active:[] spec in
      let disj = ip_disjoint_of_spec kf kinstr ~active:[] spec in
      List.iter check_ip comp ;
      List.iter check_ip disj ;
    with Annotations.No_funspec _ -> ()
  in
  let check_bhv kf kinstr bv =
    if CfgInfos.is_entry_point kf then
      check_bhv_requires kf kinstr bv ;
    check_bhv_assigns kf kinstr bv ;
    check_bhv_allocation kf kinstr bv ;
    check_bhv_ensures kf kinstr bv ;
    check_complete_disjoint kf kinstr
  in
  let check_code () =
    let stmts =
      try (Kernel_function.get_definition kf).sallstmts
      with Kernel_function.No_Definition -> []
    in
    let check stmt _ ca =
      List.iter check_ip (ip_of_code_annot kf stmt ca)
    in
    let check_call stmt =
      let check_callee kf =
        let kf_behaviors = Annotations.behaviors kf in
        List.iter (check_bhv_requires kf Kglobal) kf_behaviors
      in
      List.iter check_callee (get_called_stmt stmt)
    in
    let check_stmt stmt =
      check_call stmt ;
      Annotations.iter_code_annot (check stmt) stmt
    in
    List.iter check_stmt stmts
  in
  let check_funbhv bv = check_bhv kf Kglobal bv in
  Annotations.iter_behaviors check_funbhv kf ;
  check_code ()

let add_with_behaviors behaviors props kf =
  if behaviors = [] && props = [] then
    add_with_callees kf
  else begin
    try check_properties behaviors props kf
    with Found -> add_with_callees kf
  end

let compute_kf model bhv prop kf =
  let rtes = Wp_parameters.RTE.get () in
  if rtes then WpRTE.generate model kf ;
  add_with_behaviors bhv prop kf

let compute model
    ?(fct=Wp_parameters.get_fct())
    ?(bhv=Wp_parameters.Behaviors.get())
    ?(prop=Wp_parameters.Properties.get ()) ()
  =
  Wp_parameters.iter_fct (compute_kf model bhv prop) fct

let compute_kf model kf =
  compute_kf model [] [] kf

let iter = TargetKfs.iter
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