package frama-c

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

Source file studia_request.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 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 Server
open Cil_types

let package =
  Package.package ~plugin:"studia" ~name:"studia" ~title:"Studia" ()

type effects =
  { direct: stmt list;
    indirect: stmt list; }

module Effects = struct
  open Server.Data

  type record
  let record: record Record.signature = Record.signature ()

  module Location = Data.Jpair (Kernel_ast.Function) (Kernel_ast.Marker)

  let direct = Record.field record ~name:"direct"
      ~descr:(Markdown.plain "List of statements with direct effect.")
      (module Data.Jlist (Location))
  let indirect = Record.field record ~name:"indirect"
      ~descr:(Markdown.plain "List of statements with indirect effect.")
      (module Data.Jlist (Location))

  let data = Record.publish record ~package ~name:"effects"
      ~descr:(Markdown.plain "Statements that read or write a location.")

  module R : Record.S with type r = record = (val data)
  type t = effects
  let jtype = R.jtype

  let to_json effects =
    let output_stmt stmt =
      let kf = Kernel_function.find_englobing_kf stmt in
      kf, Printer_tag.PStmtStart (kf, stmt)
    in
    R.default |>
    R.set direct (List.map output_stmt effects.direct) |>
    R.set indirect (List.map output_stmt effects.indirect) |>
    R.to_json
end

let compute_writes zone =
  let reads = Writes.compute zone in
  let add acc = function
    | Writes.Assign stmt | CallDirect stmt ->
      { acc with direct = stmt :: acc.direct }
    | CallIndirect stmt ->
      { acc with indirect = stmt :: acc.indirect }
    | FormalInit (_vi, callsites) ->
      let calls = List.flatten (List.map snd callsites) in
      { acc with direct = calls @ acc.direct }
    | GlobalInit (_vi, _initinfo) ->
      acc (* for now ignore global initializations *)
  in
  let empty = { direct = []; indirect = []; } in
  List.fold_left add empty reads

let compute_reads zone =
  let reads = Reads.compute zone in
  let add acc = function
    | Reads.Direct stmt -> { acc with direct = stmt :: acc.direct }
    | Indirect stmt -> { acc with indirect = stmt :: acc.indirect }
  in
  let empty = { direct = []; indirect = []; } in
  List.fold_left add empty reads

let lval_location kinstr lval =
  Eva.Results.(before_kinstr kinstr |> eval_address lval |> as_zone)

let () = Request.register ~package
    ~kind:`GET ~name:"getReadsLval"
    ~descr:(Markdown.plain "Get the list of statements that read a lval.")
    ~input:(module Kernel_ast.Lval)
    ~output:(module Effects)
    (fun (kinstr, lval) -> compute_reads (lval_location kinstr lval))

let () = Request.register ~package
    ~kind:`GET ~name:"getWritesLval"
    ~descr:(Markdown.plain "Get the list of statements that write a lval.")
    ~input:(module Kernel_ast.Lval)
    ~output:(module Effects)
    (fun (kinstr, lval) -> compute_writes (lval_location kinstr lval))
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