package frama-c
Platform dedicated to the analysis of source code written in C
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493
doc/src/frama-c-callgraph.core/services.ml.html
Source file services.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
(**************************************************************************) (* *) (* 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). *) (* *) (**************************************************************************) module type S = Graph.Graphviz.GraphWithDotAttrs let initial_service_roots cg = let roots = Options.Service_roots.get () in let roots = if Kernel_function.Set.is_empty roots then (* if possible, use the main function as initial root *) try Kernel_function.Set.singleton (fst (Globals.entry_point ())) with Globals.No_such_entry_point _ -> (* otherwise use every uncalled function *) Cg.G.fold_vertex (fun v set -> if Cg.G.in_degree cg v = 0 then Kernel_function.Set.add v set else set) cg Kernel_function.Set.empty else roots in (* Add the callees of initial roots as roots *) Kernel_function.Set.fold (fun v set -> Cg.G.fold_succ Kernel_function.Set.add cg v set) roots roots (* Intermediate module because of Ocaml: "The parameter cannot be eliminated in the result type. Please bind the argument to a module identifier." *) module G_for_S = struct let datatype_name = "Callgraph.Cg" module V = struct include Cg.G.V let id = Kernel_function.get_id let name = Kernel_function.get_name let attributes = Cg.Graphviz_attributes.vertex_attributes let entry_point () = try Some (fst (Globals.entry_point ())) with Globals.No_such_entry_point _ -> None end include (Cg.G: Graph.Sig.G with module V := V and type t = Cg.G.t) end module S = Service_graph.Make(G_for_S) module G = S.Service_graph module Graphviz_attributes = S.TP let entry_point = S.entry_point let is_root kf = (S.vertex kf).Service_graph.is_root module State = State_builder.Option_ref (S.Service_graph.Datatype) (struct let name = "Callgraph.Services" let dependencies = [ Cg.self; Kernel.MainFunction.self ] end) module StateHook = Hook.Build (S.Service_graph.Datatype) (* eta-expansion required to mask optional argument [?project] *) let is_computed () = State.is_computed () let self = State.self let add_hook = StateHook.extend let compute () = let cg = Cg.get () in let isr = initial_service_roots cg in let isr_names = Kernel_function.Set.fold (fun kf acc -> Datatype.String.Set.add (Kernel_function.get_name kf) acc) isr Datatype.String.Set.empty in let sg = S.compute cg isr_names in State.mark_as_computed (); StateHook.apply sg; sg let get () = State.memo compute let compute () = ignore (compute ()) module Subgraph = Subgraph.Make (G) (S.Service_graph.Datatype) (struct let self = State.self let name = State.name let get = get let vertex = S.vertex end) let dump () = let sg = Subgraph.get () in Service_graph.frama_c_display false; Options.dump S.output_graph sg (* Local Variables: compile-command: "make -C ../../.." End: *)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>