package frama-c

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

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


let mthread_global_var var_name () =
  try Globals.Vars.find_from_astinfo var_name Global
  with Not_found ->
    Mt_options.fatal
      "Variable@ %s@ not@ found.@ It@ should@ be@ in@ %a."
      var_name Filepath.pretty (Mt_lib.mthread_h ())

let is_call_to_sync stmt =
  match stmt.skind with
  | Instr (Call (_, { enode = Lval (Var vi, _)}, _, _))
    when vi.vname = "Frama_C_mthread_sync" -> true
  (* No Local_init possible here, as Frama_C_mthread_sync returns void. *)
  | _ -> false

(* -------------------------------------------------------------------------- *)
(* --- Pretty-printing                                                    --- *)
(* -------------------------------------------------------------------------- *)

let kinstr_to_source = function
  | Kglobal -> None
  | Kstmt stmt -> Some (fst (Cil_datatype.Stmt.loc stmt))


let pretty_succs fmt stmt =
  (Pretty_utils.pp_list ~sep:" "
     (fun fmt s -> Format.fprintf fmt "%d" s.sid)) fmt stmt.succs



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

type stack_elt = kernel_function * kinstr

module StackElt = struct
  include Datatype.Pair(Kernel_function)(Cil_datatype.Kinstr)

  let pretty fmt (f, ki) =
    Format.fprintf fmt "@[<hov 2>%s%t@]"
      (Ast_info.Function.get_name f.fundec)
      (fun fmt -> match ki with
         | Kstmt stmt ->
           let loc = Cil_datatype.Stmt.loc stmt in
           Format.fprintf fmt " :: %a" Cil_datatype.Location.pretty loc
         | Kglobal -> ()
      )

end

type stack = stack_elt list

module Stack = struct

  include Datatype.List(StackElt)

  let pretty =
    Pretty_utils.pp_list ~pre:"@[<hv>" ~sep:" <-@ " ~suf:"@]" StackElt.pretty

  module FunAccessVars =
    State_builder.Option_ref(Cil_datatype.Kf)
      (struct let dependencies = [Ast.self]
        let name = "Stack.FunAccessVars"
      end)

  let fun_access_vars () =
    FunAccessVars.memo (fun () -> Kernel_function.dummy ())

  let access_to_var stmt : stack_elt = fun_access_vars (), Kstmt stmt
  let is_access_to_var (kf, _) =
    Kernel_function.equal kf (fun_access_vars ())

end
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