package frama-c

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

Source file callstack.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
(**************************************************************************)
(*                                                                        *)
(*  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

module Callsite = Datatype.Pair (Kernel_function) (Cil_datatype.Kinstr)
type call_site = Callsite.t

include Datatype.With_collections (Datatype.List (Callsite))
    (struct let module_name = "Dive.Callstack" end)

let init kf = [(kf,Kglobal)]

let pop cs =
  match cs with
  | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
  | [(_,Kglobal)] -> None
  | (kf,Kstmt stmt) :: t -> Some (kf,stmt,t)

let top_kf cs =
  match cs with
  | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
  | (kf,_) :: _ -> kf

let rec pop_downto top_kf = function
  | [] -> failwith "the callstack doesn't contain this function"
  | ((kf,_kinstr) :: tail) as cs ->
    if Kernel_function.equal kf top_kf
    then cs
    else pop_downto top_kf tail

let push (kf,stmt) cs =
  match cs with
  (* When the callstack is truncated, we ignore the first callsite *)
  | [] -> [(kf,Kglobal)]
  | cs -> (kf,Kstmt stmt) :: cs

let rec is_prefix cs1 cs2 =
  match cs1, cs2 with
  | [], _ -> true
  | _, [] -> false
  | [(kf,Kglobal)], (kf',_)::_ -> Kernel_function.equal kf kf'
  | _, [(_,Kglobal)] -> false
  | s1 :: t1, s2 :: t2 ->
    if Callsite.equal s1 s2
    then is_prefix t1 t2
    else false

let truncate_to_sub full_cs sub_cs =
  let rec aux acc = function
    | [] -> None
    | (s :: t) as cs ->
      if is_prefix sub_cs cs
      then Some (List.rev_append acc sub_cs)
      else aux (s :: acc) t
  in
  aux [] full_cs
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