package frama-c

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

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

(** Points-to graphs datastructure. *)
module G = Abstract_state.G

let vid = Abstract_state.vid

module LSet = Abstract_state.LSet

module Abstract_state = Abstract_state

let check_computed () =
  if not (Analysis.is_computed ())
  then
    Options.abort "Static analysis must be called before any function of the API can be called"


let lset
    (get_set : Abstract_state.t -> LSet.t)
    (kf : kernel_function) (s : stmt) =
  check_computed ();
  match Analysis.get_state_before_stmt kf s with
  | None -> LSet.empty
  | Some state -> get_set state

let points_to_set_stmt kf s lv = lset (Abstract_state.points_to_set lv) kf s

let new_points_to_set_stmt kf s lv =
  let get_set state =
    let new_state = Analysis.do_stmt state s in
    Abstract_state.points_to_set lv new_state
  in
  lset get_set kf s

let aliases_stmt kf s lv =
  lset (Abstract_state.find_all_aliases lv) kf s

let new_aliases_stmt kf s lv =
  let get_set state =
    let new_state = Analysis.do_stmt state s in
    Abstract_state.find_all_aliases lv new_state
  in
  lset get_set kf s

let points_to_set_kf (kf : kernel_function) (lv : lval) =
  check_computed ();
  if Kernel_function.has_definition kf
  then
    let s = Kernel_function.find_return kf in
    new_points_to_set_stmt kf s lv
  else
    Options.abort "points_to_set_kf: function %a has no definition" Kernel_function.pretty kf

let aliases_kf (kf : kernel_function) (lv : lval) =
  check_computed ();
  if Kernel_function.has_definition kf
  then
    let s = Kernel_function.find_return kf in
    new_aliases_stmt kf s lv
  else
    Options.abort "aliases_kf: function %a has no definition" Kernel_function.pretty kf

let fundec_stmts (kf : kernel_function) (lv : lval) =
  check_computed ();
  if Kernel_function.has_definition kf
  then
    List.map
      (fun s -> s, new_aliases_stmt kf s lv)
      (Kernel_function.get_definition kf).sallstmts
  else
    Options.abort "fundec_stmts: function %a has no definition" Kernel_function.pretty kf


let fold_points_to_set f_fold acc kf s lv =
  LSet.fold (fun e a -> f_fold a e) (points_to_set_stmt kf s lv) acc

let fold_aliases_stmt f_fold acc kf s lv =
  LSet.fold (fun e a -> f_fold a e) (aliases_stmt kf s lv) acc

let fold_new_aliases_stmt f_fold acc kf s lv =
  LSet.fold (fun e a -> f_fold a e) (new_aliases_stmt kf s lv) acc

let fold_points_to_set_kf (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
  LSet.fold (fun e a -> f_fold a e) (points_to_set_kf kf lv) acc

let fold_aliases_kf (f_fold : 'a -> lval -> 'a) (acc : 'a) (kf : kernel_function) (lv : lval) : 'a =
  LSet.fold (fun e a -> f_fold a e) (aliases_kf kf lv) acc

let fold_fundec_stmts (f_fold: 'a -> stmt -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
  List.fold_left
    (fun acc (s, set) ->
       LSet.fold (fun lv a -> f_fold a s lv) set acc
    )
    acc
    (fundec_stmts kf lv)

let are_aliased (kf: kernel_function) (s:stmt) (lv1: lval) (lv2:lval) : bool =
  check_computed ();
  match Analysis.get_state_before_stmt kf s with
    None -> false
  | Some state ->
    let setv1 = Abstract_state.find_all_aliases lv1 state in
    LSet.mem lv2 setv1

let fold_vertex (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
  check_computed ();
  match Analysis.get_state_before_stmt kf s with
    None -> acc
  | Some state ->
    let v : G.V.t = Abstract_state.find_vertex lv state in
    let set_aliases = Abstract_state.find_aliases lv state in
    LSet.fold (fun lv a-> f_fold a v lv) set_aliases acc

let fold_vertex_closure  (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: kernel_function)  (s:stmt) (lv: lval) : 'a =
  check_computed ();
  match Analysis.get_state_before_stmt kf s with
    None -> acc
  | Some state ->
    let list_closure : (G.V.t * LSet.t) list = Abstract_state.find_transitive_closure lv state in
    List.fold_left
      (fun acc (i,s) -> LSet.fold (fun lv a -> f_fold a i lv) s acc)
      acc
      list_closure

let get_state_before_stmt =
  Analysis.get_state_before_stmt

let call_function a f res args =
  match Analysis.get_summary f with
    None -> None
  | Some su -> Some(Abstract_state.call a res args su)

let simplify_lval = Simplified.Lval.simplify
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