package frama-c

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

Source file derefs.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil
open Locations


class virtual do_it_ = object(self)
  inherit [Zone.t] Cumulative_analysis.cumulative_visitor
  val mutable derefs = Zone.bottom

  method bottom = Zone.bottom

  method result = derefs

  method join new_ =
    derefs <- Zone.join new_ derefs;

  method! vlval (base,_ as lv) =
    begin match base with
      | Var _ -> ()
      | Mem e ->
        let stmt = Option.get self#current_stmt in
        let r = Eva.Results.(before stmt |> eval_exp e |> as_cvalue) in
        let loc = loc_bytes_to_loc_bits r in
        let size = Bit_utils.sizeof_lval lv in
        self#join
          (enumerate_valid_bits Read (make_loc loc size))
    end;
    DoChildren

  method compute_funspec (_: kernel_function) =
    Zone.bottom

  method clean_kf_result (_ : kernel_function) (r: Locations.Zone.t) = r

end

module Analysis = Cumulative_analysis.Make(
  struct
    let analysis_name ="derefs"

    type t = Locations.Zone.t
    module T = Locations.Zone

    class virtual do_it = do_it_
  end)

let get_internal = Analysis.kernel_function

let externalize _return fundec x =
  Zone.filter_base
    (fun v -> not (Base.is_formal_or_local v fundec))
    x

module Externals =
  Kernel_function.Make_Table(Locations.Zone)
    (struct
      let name = "Inout.Derefs.Externals"
      let dependencies = [ Analysis.Memo.self ]
      let size = 17
    end)

let get_external =
  Externals.memo
    (fun kf ->
       Eva.Analysis.compute ();
       if Kernel_function.is_definition kf then
         try
           externalize
             (Kernel_function.find_return kf)
             (Kernel_function.get_definition kf)
             (get_internal kf)
         with Kernel_function.No_Statement ->
           assert false
       else
         (* assume there is no deref for leaf functions *)
         Zone.bottom)

let compute_external kf = ignore (get_external kf)

let _pretty_internal fmt kf =
  Format.fprintf fmt "@[Derefs (internal) for function %a:@\n@[<hov 2>  %a@]@]@\n"
    Kernel_function.pretty kf
    Zone.pretty (get_internal kf)

let pretty_external fmt kf =
  Format.fprintf fmt "@[Derefs for function %a:@\n@[<hov 2>  %a@]@]@\n"
    Kernel_function.pretty kf
    Zone.pretty (get_external kf)
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