package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

doc/src/frama-c-region.core/analysis.ml.html

Source file `analysis.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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

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

module DOMAIN : Datatype.S with type t = Code.domain =
  Datatype.Make
    (struct
      type t = Code.domain
      include Datatype.Undefined
      let name = "Region.Analysis.MEMORY"
      let mem_project = Datatype.never_any_project
      let reprs = [ Memory.create () ]
    end)

module STATE = State_builder.Hashtbl(Kernel_function.Hashtbl)(DOMAIN)
    (struct
      let size = 0
      let name = "Region.Analysis.STATE"
      let dependencies = [Ast.self]
    end)

(* -------------------------------------------------------------------------- *)
(* ---  Memoized Access                                                   --- *)
(* -------------------------------------------------------------------------- *)

let dump = Options.register_category "dump"
    ~help:"Dump regions for each analyzed function"

let find = STATE.find

let get kf =
  try STATE.find kf with Not_found ->
    Options.feedback ~ontty:`Transient
      "Function %a%t" Kernel_function.pretty kf Unicode.pp_ellipsis ;
    let domain = Code.domain kf in
    STATE.add kf domain ;
    if Options.is_debug_key_enabled dump then
      Options.result "@[<v 2>Function %a:%t@]@."
        Kernel_function.pretty kf
        begin fun fmt ->
          List.iter
            begin fun r ->
              Format.pp_print_newline fmt () ;
              Memory.pp_region fmt r ;
            end @@
          Memory.regions domain ;
        end ;
    domain

let compute kf = ignore @@ get kf

let add_hook f = STATE.add_hook_on_change (fun _ -> f())

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