package frama-c

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

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

(* -------------------------------------------------------------------------- *)
(* --- Proxy to Region Analysis for Region Model                          --- *)
(* -------------------------------------------------------------------------- *)

type region = Region.node

let get_map () =
  match WpContext.get_scope () with
  | Kf kf -> Region.map kf
  | Global -> Wp_parameters.not_yet_implemented "[region] logic context"

let id region = Region.uid (get_map ()) region

let of_id id =
  try Some (Region.find (get_map ()) id)
  with Not_found -> None
let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r

module R =
struct
  type t = region
  let compare = compare
  let pretty = pretty
end

(* Keeping track of the decision to apply which memory model to each region *)
module Kind = WpContext.Generator(R)
    (struct
      open MemRegion
      let name = "Wp.RegionAnalysis.Kind"
      type key = region
      type data = kind
      let kind map r p = if Region.singleton map r then Single p else Many p
      let compile r =
        let map = get_map () in
        match Region.typed map r with
        | Some ty ->
          begin
            match Ctypes.object_of ty with
            | C_int i -> kind map r (Int i)
            | C_float f -> kind map r (Float f)
            | C_pointer _ -> kind map r Ptr
            | _ -> Garbled
          end
        | None -> Garbled
    end)

module Name = WpContext.Generator(R)
    (struct
      let name = "Wp.RegionAnalysis.Name"
      type key = region
      type data = string option
      let compile r =
        let map = get_map () in
        match Region.labels map r with
        | label::_ -> Some label
        | [] ->
          match Region.roots map r with
          | v::_ -> Some v.vorig_name
          | _ -> None
    end)

let kind = Kind.get
let name = Name.get
let points_to region = Region.points_to (get_map ()) region
let separated r1 r2 = Region.separated (get_map ()) r1 r2
let included r1 r2 = Region.included (get_map ()) r1 r2

let cvar var =
  try Some (Region.cvar (get_map ()) var)
  with Not_found -> None

let field r fd =
  try Some (Region.field (get_map ()) r fd)
  with Not_found -> None

let shift r obj =
  try Some (Region.index (get_map ()) r (Ctypes.object_to obj))
  with Not_found -> None

let literal ~eid _ = ignore eid ; None

let footprint r = Region.footprint (get_map ()) r
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