diff --git a/Changelog b/Changelog
index 613f2a54569cd4de76a8584a99daa7c7aa480e5f..0fbed0851ebd3ce5581ae4b3a0a7a1cc40c70e2a 100644
--- a/Changelog
+++ b/Changelog
@@ -19,6 +19,10 @@ Open Source Release <next-release>
 ###############################################################################
 
 o   Kernel    [2024-07-30] mapNoCopy moved to Extlib and deprecated in Cil
+o   Eva       [2024-07-31] Export profiling information about the analysis
+              performance via the new module Eva_perf in Eva.mli.
+-   Ivette    [2024-07-26] New flamegraph component to visualize Eva analysis
+              time by C functions, in the "Eva Summary" view by default.
 -   Kernel    [2024-05-20] New ACSL extension loop unfold (replaces loop pragma UNROLL)
 -!  Kernel    [2024-05-20] Removed loop pragma UNROLL annotations
 o!  Kernel    [2024-05-20] Renamed module Unroll_loop into Unfold_loop
diff --git a/ivette/src/frama-c/plugins/eva/Flamegraph.tsx b/ivette/src/frama-c/plugins/eva/Flamegraph.tsx
index 41f01b1f881070e9da2616a5f707b34e51590433..e033ba703c347be11f1fb42855a672346e917d7f 100644
--- a/ivette/src/frama-c/plugins/eva/Flamegraph.tsx
+++ b/ivette/src/frama-c/plugins/eva/Flamegraph.tsx
@@ -23,7 +23,6 @@
 import React from 'react';
 import { IconButton } from 'dome/controls/buttons';
 import * as Ivette from 'ivette';
-import * as Ast from 'frama-c/kernel/api/ast';
 import * as States from 'frama-c/states';
 import * as Eva from 'frama-c/plugins/eva/api/general';
 import { FlameGraph } from 'react-flame-graph';
@@ -34,34 +33,36 @@ import { useFlipSettings } from 'dome';
 
 // --- Flamegraph Table ---
 interface Flamegraph {
-  kfKey?: string;
   name: string;
   value: number;
-  children?: Flamegraph[];
+  children: Flamegraph[];
+  info?: Eva.flamegraphData;
 }
 
 const addNodeToFlamegraph = (
   flamegraph: Flamegraph,
   cs: string[],
-  row: Eva.evaFlamegraphData,
+  row: Eva.flamegraphData,
 ): void => {
-  // Accumulate times for all nodes crossed
-  flamegraph.value += row.time;
+  /* Accumulate times for all nodes crossed. We do not rely on [row.totalTime]
+     as during the analysis, the flamegraph is incomplete and the total time
+     of some callstacks may be inconsistent. So we rebuild the total time of
+     each callstack from the selfTime of all available callstacks. */
+  flamegraph.value += row.selfTime;
   // updating last node
   if(cs.length === 0) {
-    flamegraph.kfKey = row.kfkey;
-    return;
+    flamegraph.info = row;
+  } else {
+    // Search/create next node
+    let nextNode = flamegraph.children.find((elt) => elt.name === cs[0]);
+    if (!nextNode) {
+      nextNode = { name: cs[0], value: 0, children: [] };
+      flamegraph.children.unshift(nextNode);
+    }
+    cs.shift();
+    // Treatment of the next node
+    addNodeToFlamegraph(nextNode, cs, row);
   }
-  // Search/create next node
-  if (!flamegraph.children) flamegraph.children = [];
-  let nextNode = flamegraph.children.find((elt) => elt.name === cs[0]);
-  if (!nextNode) {
-    nextNode = { name: cs[0], value: 0 };
-    flamegraph.children.unshift(nextNode);
-  }
-  cs.shift();
-  // Treatment of the next node
-  addNodeToFlamegraph(nextNode, cs, row);
 };
 
 interface EvaFlamegraphProps {
@@ -78,9 +79,15 @@ function round(f: number, decimal: number): number {
 
 /* Returns text to be shown about a node in a flamegraph. */
 function nodeInfoText(flameGraph:Flamegraph, node:Flamegraph): string {
+  if (node.info === undefined) return "";
   const percentage = round(100 * node.value / flameGraph.value, 1);
-  const value = round(node.value, 2);
-  const infos = node.name + " : " + value + "s : " + percentage + "%";
+  const total = round(node.value, 2);
+  const self = round(node.info.selfTime, 2);
+  const infos =
+    `${node.name}:\n`
+    + `  callstack analyzed ${node.info.nbCalls} times\n`
+    + `  total time (including called functions): ${total}s.,  ${percentage}%\n`
+    + `  time for ${node.name} only: ${self}s.`;
   return infos;
 }
 
@@ -91,7 +98,7 @@ function EvaFlamegraph(props: EvaFlamegraphProps): JSX.Element {
 
   /* eslint-disable-next-line @typescript-eslint/no-explicit-any */
   const changeScope = (node:any): void => {
-    if (useScope) States.setCurrentScope(node.source.kfKey as Ast.decl);
+    if (useScope) States.setCurrentScope(node.source.info.kfDecl);
   };
 
   return (
@@ -120,23 +127,21 @@ function EvaFlamegraph(props: EvaFlamegraphProps): JSX.Element {
 export function FlamegraphComponent(): JSX.Element {
   const [useScope, flipUseScope] =
     useFlipSettings("eva.flamegraph.scope", true);
-  const model = States.useSyncArrayData(Eva.evaFlamegraph);
+  const model = States.useSyncArrayData(Eva.flamegraph);
 
   const flameGraph = React.useMemo<Flamegraph | null>(() => {
     if(model.length === 0 ) return null;
-    const flame: Flamegraph = {
-      name: model[0].funlist.split(":")[0],
-      value: 0
-    };
+    const mainName = model[0].stackNames[0];
+    const flame: Flamegraph = { name: mainName, value: 0, children: [] };
     model.forEach(row => {
-      const cs = row.funlist.split(":");
+      const cs = row.stackNames;
       cs.shift();
       addNodeToFlamegraph(flame, cs, row);
     });
     return flame;
   }, [model]);
 
-  const isWaitingForData = !flameGraph || !flameGraph.children;
+  const isWaitingForData = flameGraph === null;
 
   return (
     <>
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index ce5eb30dbab5659ea3483db89c6d6ad16931becb..ecaf272f15592eeff77c2c86e1666c42caddf6b4 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -760,145 +760,103 @@ export const getStates: Server.GetRequest<
   [ string, string, string ][]
   >= getStates_internal;
 
-/** Kernel function stack identifier */
-export type kfstack = Json.index<'#kfstack'>;
-
-/** Decoder for `kfstack` */
-export const jKfstack: Json.Decoder<kfstack> =
-  Json.jIndex<'#kfstack'>('#kfstack');
-
-/** Natural order for `kfstack` */
-export const byKfstack: Compare.Order<kfstack> = Compare.number;
-
-/** Default value for `kfstack` */
-export const kfstackDefault: kfstack =
-  Json.jIndex<'#kfstack'>('#kfstack')(-1);
-
-/** Kernel function list infos */
-export type calllink = { callee: decl, caller?: decl };
-
-/** Decoder for `calllink` */
-export const jCalllink: Json.Decoder<calllink> =
-  Json.jObject({ callee: jDecl, caller: Json.jOption(jDecl),});
-
-/** Natural order for `calllink` */
-export const byCalllink: Compare.Order<calllink> =
-  Compare.byFields
-    <{ callee: decl, caller?: decl }>({
-    callee: byDecl,
-    caller: Compare.defined(byDecl),
-  });
-
-/** Default value for `calllink` */
-export const calllinkDefault: calllink =
-  { callee: declDefault, caller: undefined };
-
-/** Data for array rows [`evaFlamegraph`](#evaflamegraph)  */
-export interface evaFlamegraphData {
+/** Data for array rows [`flamegraph`](#flamegraph)  */
+export interface flamegraphData {
   /** Entry identifier. */
-  key: Json.key<'#evaFlamegraph'>;
-  /** Caller list identifier */
-  stack: kfstack;
-  /** Computation time for the kernel function stack */
-  time: number;
-  /** Kernel function description */
-  title: string;
-  /** Function name */
-  name: string;
-  /** Function list */
-  funlist: string;
-  /** Kernel function key */
-  kfkey: string;
+  key: Json.key<'#flamegraph'>;
+  /** Callstack as functions name list, starting from main */
+  stackNames: string[];
+  /** Number of times the callstack has been analyzed */
+  nbCalls: number;
+  /** Computation time for the callstack itself */
+  selfTime: number;
+  /** Total computation time, including functions called */
+  totalTime: number;
+  /** Declaration of the top function */
+  kfDecl: decl;
 }
 
-/** Decoder for `evaFlamegraphData` */
-export const jEvaFlamegraphData: Json.Decoder<evaFlamegraphData> =
+/** Decoder for `flamegraphData` */
+export const jFlamegraphData: Json.Decoder<flamegraphData> =
   Json.jObject({
-    key: Json.jKey<'#evaFlamegraph'>('#evaFlamegraph'),
-    stack: jKfstack,
-    time: Json.jNumber,
-    title: Json.jString,
-    name: Json.jString,
-    funlist: Json.jString,
-    kfkey: Json.jString,
+    key: Json.jKey<'#flamegraph'>('#flamegraph'),
+    stackNames: Json.jArray(Json.jString),
+    nbCalls: Json.jNumber,
+    selfTime: Json.jNumber,
+    totalTime: Json.jNumber,
+    kfDecl: jDecl,
   });
 
-/** Natural order for `evaFlamegraphData` */
-export const byEvaFlamegraphData: Compare.Order<evaFlamegraphData> =
+/** Natural order for `flamegraphData` */
+export const byFlamegraphData: Compare.Order<flamegraphData> =
   Compare.byFields
-    <{ key: Json.key<'#evaFlamegraph'>, stack: kfstack, time: number,
-       title: string, name: string, funlist: string, kfkey: string }>({
+    <{ key: Json.key<'#flamegraph'>, stackNames: string[], nbCalls: number,
+       selfTime: number, totalTime: number, kfDecl: decl }>({
     key: Compare.string,
-    stack: byKfstack,
-    time: Compare.number,
-    title: Compare.string,
-    name: Compare.string,
-    funlist: Compare.string,
-    kfkey: Compare.string,
+    stackNames: Compare.array(Compare.string),
+    nbCalls: Compare.number,
+    selfTime: Compare.number,
+    totalTime: Compare.number,
+    kfDecl: byDecl,
   });
 
-/** Signal for array [`evaFlamegraph`](#evaflamegraph)  */
-export const signalEvaFlamegraph: Server.Signal = {
-  name: 'plugins.eva.general.signalEvaFlamegraph',
+/** Signal for array [`flamegraph`](#flamegraph)  */
+export const signalFlamegraph: Server.Signal = {
+  name: 'plugins.eva.general.signalFlamegraph',
 };
 
-const reloadEvaFlamegraph_internal: Server.GetRequest<null,null> = {
+const reloadFlamegraph_internal: Server.GetRequest<null,null> = {
   kind: Server.RqKind.GET,
-  name: 'plugins.eva.general.reloadEvaFlamegraph',
+  name: 'plugins.eva.general.reloadFlamegraph',
   input: Json.jNull,
   output: Json.jNull,
   fallback: null,
   signals: [],
 };
-/** Force full reload for array [`evaFlamegraph`](#evaflamegraph)  */
-export const reloadEvaFlamegraph: Server.GetRequest<null,null>= reloadEvaFlamegraph_internal;
+/** Force full reload for array [`flamegraph`](#flamegraph)  */
+export const reloadFlamegraph: Server.GetRequest<null,null>= reloadFlamegraph_internal;
 
-const fetchEvaFlamegraph_internal: Server.GetRequest<
+const fetchFlamegraph_internal: Server.GetRequest<
   number,
-  { reload: boolean, removed: Json.key<'#evaFlamegraph'>[],
-    updated: evaFlamegraphData[], pending: number }
+  { reload: boolean, removed: Json.key<'#flamegraph'>[],
+    updated: flamegraphData[], pending: number }
   > = {
   kind: Server.RqKind.GET,
-  name: 'plugins.eva.general.fetchEvaFlamegraph',
+  name: 'plugins.eva.general.fetchFlamegraph',
   input: Json.jNumber,
   output: Json.jObject({
             reload: Json.jBoolean,
-            removed: Json.jArray(
-                       Json.jKey<'#evaFlamegraph'>('#evaFlamegraph')),
-            updated: Json.jArray(jEvaFlamegraphData),
+            removed: Json.jArray(Json.jKey<'#flamegraph'>('#flamegraph')),
+            updated: Json.jArray(jFlamegraphData),
             pending: Json.jNumber,
           }),
   fallback: { reload: false, removed: [], updated: [], pending: 0 },
   signals: [],
 };
-/** Data fetcher for array [`evaFlamegraph`](#evaflamegraph)  */
-export const fetchEvaFlamegraph: Server.GetRequest<
+/** Data fetcher for array [`flamegraph`](#flamegraph)  */
+export const fetchFlamegraph: Server.GetRequest<
   number,
-  { reload: boolean, removed: Json.key<'#evaFlamegraph'>[],
-    updated: evaFlamegraphData[], pending: number }
-  >= fetchEvaFlamegraph_internal;
+  { reload: boolean, removed: Json.key<'#flamegraph'>[],
+    updated: flamegraphData[], pending: number }
+  >= fetchFlamegraph_internal;
 
-const evaFlamegraph_internal: State.Array<
-  Json.key<'#evaFlamegraph'>,
-  evaFlamegraphData
+const flamegraph_internal: State.Array<
+  Json.key<'#flamegraph'>,
+  flamegraphData
   > = {
-  name: 'plugins.eva.general.evaFlamegraph',
-  getkey: ((d:evaFlamegraphData) => d.key),
-  signal: signalEvaFlamegraph,
-  fetch: fetchEvaFlamegraph,
-  reload: reloadEvaFlamegraph,
-  order: byEvaFlamegraphData,
+  name: 'plugins.eva.general.flamegraph',
+  getkey: ((d:flamegraphData) => d.key),
+  signal: signalFlamegraph,
+  fetch: fetchFlamegraph,
+  reload: reloadFlamegraph,
+  order: byFlamegraphData,
 };
-/** Data for Eva flamegraph */
-export const evaFlamegraph: State.Array<
-  Json.key<'#evaFlamegraph'>,
-  evaFlamegraphData
-  > = evaFlamegraph_internal;
-
-/** Default value for `evaFlamegraphData` */
-export const evaFlamegraphDataDefault: evaFlamegraphData =
-  { key: Json.jKey<'#evaFlamegraph'>('#evaFlamegraph')(''),
-    stack: kfstackDefault, time: 0, title: '', name: '', funlist: '',
-    kfkey: '' };
+/** Data for flamegraph: execution times by callstack */
+export const flamegraph: State.Array<Json.key<'#flamegraph'>,flamegraphData> = flamegraph_internal;
+
+/** Default value for `flamegraphData` */
+export const flamegraphDataDefault: flamegraphData =
+  { key: Json.jKey<'#flamegraph'>('#flamegraph')(''), stackNames: [],
+    nbCalls: 0, selfTime: 0, totalTime: 0, kfDecl: declDefault };
 
 /* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index 3b7861ae8effa376b882369b1e46db2f6c1b25b2..4a991f514f8d86572a577cc71bb77fef3bb118a8 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -346,8 +346,9 @@ tr:first-of-type > .eva-table-callsite-box {
 .flame-details {
   padding: 3px 10px;
   position: absolute;
-  bottom : 0;
+  bottom: 0;
   background-color: var(--background-report);
+  white-space: pre-wrap;
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index eb0c7aaecbdee05569a5ae9011f86b9cdc18cdf5..aa4bb6a684b379d0379aec601585f5930e713cef 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -816,6 +816,45 @@ module Cvalue_callbacks: sig
   val register_call_results_hook: call_results_hook -> unit
 end
 
+module Eva_perf: sig
+  (** Statistics about the analysis performance. *)
+
+  (** Statistic about the analysis time of a function or a callstack. *)
+  type stat = {
+    nb_calls: int;
+    (** How many times the given function or callstack has been analyzed. *)
+    self_duration: float;
+    (** Time spent analyzing the function or callstack itself. *)
+    total_duration: float;
+    (** Total time, including the analysis of other functions called. *)
+    called: Kernel_function.Hptset.t;
+    (** Set of functions called from this function or callstack. *)
+  }
+
+  type 'a by_fun = (Cil_types.kernel_function * 'a) list
+
+  (** Returns a list of the functions with the longest total analysis time,
+      sorted by decreasing analysis time. Each function [f] is associated to
+      its stat and the unsorted list of stats of all function calls from [f]. *)
+  val compute_stat_by_fun: unit -> (stat * stat by_fun) by_fun
+
+  (** Statistics about each analyzed callstack. *)
+  module StatByCallstack : sig
+    type callstack = Cil_types.kernel_function list
+
+    (** Get the current analysis statistic for a callstack. *)
+    val get: callstack -> stat
+
+    (** Iterate on the statistic of every analyzed callstack. *)
+    val iter: (callstack -> stat -> unit) -> unit
+
+    (** Set a hook on statistics computation *)
+    val add_hook_on_change:
+      ((callstack, stat) State_builder.hashtbl_event -> unit) -> unit
+
+  end
+end
+
 module Logic_inout: sig
   (** Functions used by the Inout and From plugins to interpret predicate
       and assigns clauses. This API may change according to these plugins
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index afcf9ac7c2036366833b2bdd636faeb4ee5dd3c4..1f44c023b73701dede5ade8337c197c52ded326f 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -870,96 +870,43 @@ let () = Request.register ~package
     get_states
 
 
+(* ----- Flamegraph and execution times ------------------------------------- *)
 
-(* ----- Flamegraph --------------------------------------------------------- *)
+let callstack_to_string kf_list =
+  let pp_list = Pretty_utils.pp_list ~sep:":" Kernel_function.pretty in
+  Format.asprintf "%a" pp_list (List.rev kf_list)
 
-module Jkfstack :
-sig
-  include Data.S with type t = Eva_perf.KfList.t
-  val get : Eva_perf.KfList.t -> int
-end = Data.Index
-    (Eva_perf.KfList.Map)
-    (struct
-      let package = package
-      let name = "kfstack"
-      let descr = Markdown.plain "Kernel function stack identifier"
-    end)
-
-module Jkfs : Request.Output with type t = Eva_perf.KfList.t = struct
-
-  type t = Eva_perf.KfList.t
+let _evaFlamegraph =
+  let model = States.model () in
 
-  let jcalllink = Server.Data.declare ~package
-      ~name:"calllink" ~descr:(Markdown.plain "Kernel function list infos")
-      (Jrecord [
-          "callee" , Kernel_ast.Decl.jtype ;
-          "caller" , Joption Kernel_ast.Decl.jtype ;
-        ])
+  States.column model ~name:"stackNames"
+    ~descr:(Markdown.plain "Callstack as functions name list, starting from main")
+    ~data:(module Data.Jlist (Data.Jstring))
+    ~get:(fun (cs, _) -> List.rev_map Kernel_function.get_name cs);
 
-  let jtype = Package.(Jarray jcalllink)
+  States.column model ~name:"nbCalls"
+    ~descr:(Markdown.plain "Number of times the callstack has been analyzed")
+    ~data:(module Data.Jint)
+    ~get:(fun (_cs, stat) -> stat.Eva_perf.nb_calls);
 
-  let jkfstack ~jcaller ~jcallee =
-    `Assoc [
-      "callee", jcallee ;
-      "caller", jcaller ;
-    ]
+  States.column model ~name:"selfTime"
+    ~descr:(Markdown.plain "Computation time for the callstack itself")
+    ~data:(module Data.Jfloat)
+    ~get:(fun (_cs, stat) -> stat.Eva_perf.self_duration);
 
-  let to_json (cl : t) =
-    let aux (acc, jcaller) callee =
-      let jcallee = Kernel_ast.Decl.to_json (SFunction callee) in
-      jkfstack ~jcaller ~jcallee :: acc, jcallee
-    in
-    match cl with
-    | [] -> `List []
-    | entry :: r ->
-      let entry_point = Kernel_ast.Decl.to_json (SFunction entry) in
-      let l, _last_callee =
-        List.fold_left aux
-          ([`Assoc [ "callee", entry_point ]], entry_point)
-          (List.rev r)
-      in `List l
+  States.column model ~name:"totalTime"
+    ~descr:(Markdown.plain "Total computation time, including functions called")
+    ~data:(module Data.Jfloat)
+    ~get:(fun (_cs, stat) -> stat.Eva_perf.total_duration);
 
-end
+  States.column model ~name:"kfDecl"
+    ~descr:(Markdown.plain "Declaration of the top function")
+    ~data:(module Kernel_ast.Decl)
+    ~get:(fun (cs, _) -> Printer_tag.SFunction (List.hd cs));
 
-let _evaFlamegraph =
-  let model = States.model () in
-  (* This field is useful for interacting with other components,
-     eg. the currently selected callstack in EVA values *)
-  States.column model ~name:"stack"
-    ~descr:(Markdown.plain "Caller list identifier")
-    ~data:(module Jkfstack) ~get:fst ;
-  (* This field contains the computation time *)
-  States.column model ~name:"time"
-    ~descr:(Markdown.plain "Computation time for the kernel function stack")
-    ~data:(module Data.Jfloat)
-    ~get:(fun (_cs, (_start, duration)) -> duration);
-  (* This field might be useful to display tooltips on the flames *)
-  States.column model ~name:"title"
-    ~descr:(Markdown.plain "Kernel function description")
-    ~data:(module Data.Jstring)
-    ~get:(fun (cl,_) -> Pretty_utils.to_string Eva_perf.KfList.pretty cl);
-  (* This field contains the name of the function on top of the
-     kernel function stack *)
-  States.column model ~name:"name"
-    ~descr:(Markdown.plain "Function name")
-    ~data:(module Data.Jstring)
-    ~get:(fun (cl,_) -> Kernel_function.get_name (List.(hd (rev cl))));
-  (* This field contains the list of the function names *)
-  States.column model ~name:"funlist"
-    ~descr:(Markdown.plain "Function list")
-    ~data:(module Data.Jstring)
-    ~get:(fun (cl,_) ->
-        Pretty_utils.to_string (Eva_perf.KfList.pretty ~sep:":") cl);
-  (* This field contains the declaration of the function on top of the
-     kernel function stack *)
-  States.column model ~name:"kfkey"
-    ~descr:(Markdown.plain "Kernel function key")
-    ~data:(module Data.Jstring)
-    ~get:(fun (cl,_) -> Kernel_ast.Decl.index (SFunction (List.(hd (rev cl)))));
-  (* Add/remove other fields if necessary... *)
   States.register_framac_array
     ~package
-    ~name:"evaFlamegraph"
-    ~descr:(Markdown.plain "Data for Eva flamegraph")
-    ~key:(fun cl -> Format.sprintf "#%06d" @@ Jkfstack.get cl)
-    model (module Eva_perf.EvaFlamegraph)
+    ~name:"flamegraph"
+    ~descr:(Markdown.plain "Data for flamegraph: execution times by callstack")
+    ~key:callstack_to_string
+    model (module Eva_perf.StatByCallstack)
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 70707bc2619a4f9d5a7dc9488f7f4473c6a7332b..56e7f073e57e6a8ff904701fcdfbac34b40d3b4f 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -122,7 +122,6 @@
   engine/analysis.mli types/callstack.mli types/deps.mli
   utils/results.mli parameters.mli
   utils/eva_annotations.mli eval.mli types/assigns.mli ast/eva_ast.mli
-  domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/logic_inout.mli
-  utils/eva_results.mli
-  utils/unit_tests.mli)
+  domains/cvalue/builtins.mli utils/cvalue_callbacks.mli utils/eva_perf.mli
+  legacy/logic_inout.mli utils/eva_results.mli utils/unit_tests.mli)
  (action (run ./gen_api/gen_api.exe %{deps})))
diff --git a/src/plugins/eva/gen_api/gen_api.ml b/src/plugins/eva/gen_api/gen_api.ml
index fc15a52ca1f355f4bc2af92c55e39bfbbc2a7edc..d43320fefb3bde41d7966e8eeeb96d5660906755 100644
--- a/src/plugins/eva/gen_api/gen_api.ml
+++ b/src/plugins/eva/gen_api/gen_api.ml
@@ -35,14 +35,18 @@ let file_contents filename =
   contents
 
 let extract_exported_interface s =
-  let regexp =
-    Str.regexp "\\[@@@ api_start\\]\\(\\(.\\|\n\\)*\\)\\[@@@ api_end\\]"
+  let regexp_start = Str.regexp_string "[@@@ api_start]" in
+  let regexp_end = Str.regexp " *\\[@@@ api_end\\]" in
+  let find_first_api i =
+    let _i = Str.search_forward regexp_start s i in
+    let api_start = Str.match_end () in
+    let api_end = Str.search_forward regexp_end s api_start in
+    let api = String.sub s api_start (api_end - api_start) in
+    api, Str.match_end ()
   in
   let rec iter acc i =
-    match Str.search_forward regexp s i with
-    | i ->
-      let subpart = Str.matched_group 1 s in
-      iter (acc ^ subpart) (i + String.length subpart)
+    match find_first_api i with
+    | subpart, i -> iter (acc ^ subpart) i
     | exception Not_found -> acc
   in
   String.trim (iter "" 0)
diff --git a/src/plugins/eva/utils/eva_perf.ml b/src/plugins/eva/utils/eva_perf.ml
index 8486714a22a6f306595cca4741db4e6328497a3f..1a308c7666de6dc6e2968254a2efc265b620d878 100644
--- a/src/plugins/eva/utils/eva_perf.ml
+++ b/src/plugins/eva/utils/eva_perf.ml
@@ -20,459 +20,317 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
-(****************************************************************)
-(* Configuration *)
-
 (* Period between two consecutive displays, in seconds. *)
-let display_interval = 60.0;;
+let display_interval = 60.0
 
 (* Do not show functions that execute for less than that percent of
-   the total running time.  The value is 1/60, i.e. does not display
+   the total running time. The value is 1/60, i.e. it only displays
    functions that execute for longer than 3s after it has run for
-   3 minutes.
-*)
-let does_not_account_smaller_than = 1.667
+   3 minutes. *)
+let threshold = 1.667 /. 100.
 
 (* OCaml time is not always increasing, so we use max to fix this. *)
 let duration a b = max (b -. a) 0.0
 
-(****************************************************************)
-(* The metrics being computed and displayed. *)
-
-(* Performance information regarding a called function. *)
-module Call_info = struct
-  type t = {
-    (* How many times the function was called. *)
-    mutable nb_calls: int;
-
-    (* The accumulated execution time for past calls. *)
-    mutable total_duration: float;
-
-    (* If we are executing the function, since when. It is a list
-       because of the recursive calls. *)
-    mutable since: float list;
-  }
-  ;;
-
-  let create() = { nb_calls = 0; total_duration = 0.0; since = [] };;
-
-  (* Represents the calls to the main function.  *)
-  let main = create();;
-
-  (* Also accounts for currently executing time. *)
-  let total_duration current_time call_info =
-    let additional_time = match call_info.since with
-      | [] -> 0.0
-      | since::_ -> duration since current_time
-    in
-    assert (additional_time >= 0.0);
-    additional_time +. call_info.total_duration
-  ;;
-
-
-  let print fmt kf call_info current_time =
-    let bullet = match call_info.since with
-      | [] -> "+"
-      | _::_ -> "*"
-    in
-    Format.fprintf fmt "%s %a: executed: %dx total: %.3fs\n" bullet
-      Kernel_function.pretty kf call_info.nb_calls (total_duration current_time call_info)
-  ;;
-
-  (* Sorts call_infos by decreasing execution time.  *)
-  let cmp current_time ci1 ci2 =
-    - (Stdlib.compare (total_duration current_time ci1) (total_duration current_time ci2))
-  ;;
-
-  (* From an iteration, filter and sort by call_info, and returns the
-     sorted list. *)
-  let filter_and_sort iter get_ci _parent_duration current_time =
-    let analysis_total_time = total_duration current_time main in
-    let threshold = analysis_total_time *. (does_not_account_smaller_than /. 100.0) in
-    let list = ref [] in
-    iter (fun elt ->
-        let ci = get_ci elt in
-        if total_duration current_time ci > threshold
-        then list := elt::!list);
-    let sorted_list = List.fast_sort
-        (fun elt1 elt2 -> (cmp current_time) (get_ci elt1) (get_ci elt2)) !list
-    in
-    sorted_list
-  ;;
-
-  (* before/after pair. *)
-  let before_call t since =
-    t.since <- since::t.since
-  ;;
-
-  let after_call t to_ =
-    let since = List.hd t.since in
-    let duration = duration since to_ in
-    assert (duration >= 0.0);
-    t.total_duration <- t.total_duration +. duration;
-    t.nb_calls <- t.nb_calls + 1;
-    t.since <- List.tl t.since
-  ;;
-
-
-end
-
-(****************************************************************)
-(* Flat and DAG views of performance. *)
-
-(* Note: since need to be stored only in the flat view. *)
+(* -------------------------------------------------------------------------- *)
+(*                                 Flamegraph                                 *)
+(* -------------------------------------------------------------------------- *)
 
-type flat_perf_info = {
-  (* The grand total performance information for the function. *)
-  call_info: Call_info.t;
+(* Ref to the formatter to be written if option [-eva-flamegraph] is set. *)
+let flamegraph_output = ref None
 
-  (* For DAG-view: the per-caller performance information. *)
-  called_functions: Call_info.t Kernel_function.Hashtbl.t;
-}
-;;
-
-let flat_perf_create() = {
-  call_info = Call_info.create();
-  called_functions = Kernel_function.Hashtbl.create 17;
-};;
-
-let flat = Kernel_function.Hashtbl.create 17;;
-
-let flat_print current_time fmt =
-  Format.fprintf fmt "Long running functions (does not include current running time):\n";
-  Format.fprintf fmt "===============================================================\n";
-  let each_flat_entry (kf, pi) =
-    Call_info.print fmt kf pi.call_info current_time;
-    Format.fprintf fmt "    ";
-    let caller_duration = Call_info.total_duration current_time pi.call_info in
-    let total_sub = ref 0.0 in
-    let total_others = ref 0.0 in
-    let nb_others = ref 0 in
-    let each_called_entry kf ci =
-      let callee_duration = Call_info.total_duration current_time ci in
-      total_sub := !total_sub +. callee_duration;
-      let percentage = (100.0 *. (callee_duration /. caller_duration)) in
-      if percentage > 5.0
-      then
-        Format.fprintf fmt "| %a %dx %.3fs (%.1f%%) "
-          Kernel_function.pretty kf ci.Call_info.nb_calls
-          callee_duration percentage
-      else
-        (total_others := !total_others +. callee_duration;
-         incr nb_others)
-    in
-    Kernel_function.Hashtbl.iter_sorted_by_value
-      ~cmp:(Call_info.cmp current_time) each_called_entry pi.called_functions;
-    (if !nb_others > 0
-     then Format.fprintf fmt "| %d others: %.3fs (%.1f%%) "
-         !nb_others !total_others (100.0 *. !total_others /. caller_duration));
-    let self_duration = duration !total_sub caller_duration in
-    Format.fprintf fmt "| self: %.3fs (%.1f%%)|\n"
-      self_duration
-      (100.0 *. (self_duration /. caller_duration))
+(* Sets the reference above according to -eva-flamegraph. *)
+let initialize_flamegraph () =
+  if not (Parameters.ValPerfFlamegraphs.is_empty ()) then
+    try
+      let file = Parameters.ValPerfFlamegraphs.get () in
+      let out_channel = open_out (file :> string) in
+      let formatter = Format.formatter_of_out_channel out_channel in
+      flamegraph_output := Some formatter;
+    with e ->
+      Self.error "cannot open flamegraph file: %s" (Printexc.to_string e);
+      flamegraph_output := None (* to be on the safe side *)
+
+(* Adds [duration] for the callstack [kf_list] into the flamegraph file. *)
+let update_flamegraph kf_list duration =
+  let print fmt =
+    let pp_callstack = Pretty_utils.pp_list ~sep:";" Kernel_function.pretty in
+    Format.fprintf fmt "%a %.3f\n%!"
+      pp_callstack (List.rev kf_list) (duration *. 1000.)
   in
-  let flat_entries = Call_info.filter_and_sort
-      (fun f -> Kernel_function.Hashtbl.iter (fun k v -> f(k,v)) flat)
-      (fun (_,v) -> v.call_info)
-      (Call_info.total_duration current_time Call_info.main)
-      current_time in
-  List.iter each_flat_entry flat_entries
-;;
-
+  Option.iter print !flamegraph_output
 
+(* -------------------------------------------------------------------------- *)
+(*                      Save execution time by callstack                      *)
+(* -------------------------------------------------------------------------- *)
 
-(****************************************************************)
-(* Per-callstack performance. *)
-
-module Call_site = Datatype.Pair(Kernel_function)(Cil_datatype.Kinstr)
+(* Statistic about the analysis of a function or a callstack. *)
+type stat = {
+  nb_calls: int; (* How many times the function has been analyzed. *)
+  self_duration: float; (* Time spent analyzing the function itself. *)
+  total_duration: float; (* Total time, including functions called. *)
+  called: Kernel_function.Hptset.t; (* Set of functions called. *)
+}
 
-module Imperative_callstack_trie(M:sig type t val default:unit -> t end) = struct
+let empty_stat =
+  { nb_calls = 0; self_duration = 0.; total_duration = 0.;
+    called = Kernel_function.Hptset.empty; }
 
-  module Hashtbl = Hashtbl.Make(Call_site)
+module Stat = Datatype.Make (struct
+    include Datatype.Serializable_undefined
+    type t = stat
+    let name = "Eva_perf.Stat"
+    let reprs = [ empty_stat ]
+  end)
 
-  type elt = {
-    mutable self: M.t ;
-    subtree: t
-  }
+module KfList =
+  Datatype.List_with_collections (Kernel_function)
+    (struct let module_name = "Eva_perf.KfList" end)
 
-  and t = elt Hashtbl.t
-  ;;
+module StatByCallstack = struct
+  module Info = struct
+    let name = "Eva_perf.StatByCallstack"
+    let dependencies = [ Self.state ]
+    let size = 32;
+  end
 
-  let empty() = Hashtbl.create 7;;
-  let reset t = Hashtbl.clear t;;
-  let create_node init =
-    { self = init; subtree = empty() }
+  include State_builder.Hashtbl (KfList.Hashtbl) (Stat) (Info)
 
-  let rec find_subtree t callstack res = match callstack with
-    | [] ->
-      (match res with
-       | None -> failwith "Called findsubtree with an empty callstack"
-       | Some x -> x)
-    | a::b ->
-      let subnode =
-        try Hashtbl.find t a
-        with Not_found -> let n = create_node (M.default()) in
-          Hashtbl.add t a n;
-          n
-      in find_subtree subnode.subtree b (Some subnode)
+  type callstack = KfList.t
 
-  let find_subtree t callstack =
-    find_subtree t (Callstack.to_call_list callstack) None
+  let get kf_list =
+    try find kf_list
+    with Not_found -> empty_stat
 
-  let find t callstack = (find_subtree t callstack).self
+  let add_total stat total =
+    { stat with nb_calls = stat.nb_calls + 1;
+                total_duration = stat.total_duration +. total; }
 
-  let _add t callstack smth =
-    let node = find_subtree t callstack in
-    node.self <- smth
-  ;;
+  let add_called stat called =
+    { stat with called = Kernel_function.Hptset.add called stat.called }
 
-  let _update t callstack f =
-    let node = find_subtree t callstack in
-    node.self <- f node.self
-  ;;
+  let add ?called ?total ~self kf_list =
+    let stat = get kf_list in
+    let stat = { stat with self_duration = stat.self_duration +. self } in
+    let stat = Option.fold total ~none:stat ~some:(add_total stat) in
+    let stat = Option.fold called ~none:stat ~some:(add_called stat) in
+    replace kf_list stat
 end
 
-type perf_info = {
-  call_info_per_stack: Call_info.t;
-}
+(* Reference to the time at which the analysis of each function from the current
+   callstack started. The most recent function is the head of the list.
+   Set when starting the analysis of a function, used when leaving the function
+   to compute the total time the analysis has taken. *)
+let stack_timestamp = ref []
+
+(* Set and used whenever the current analyzed function changes, to compute the
+   time spent analyzing each function. *)
+let last_timestamp = ref 0.
+
+let duration_since_last_timestamp current_time =
+  let duration = duration !last_timestamp current_time in
+  last_timestamp := current_time;
+  duration
+
+(* Called at the start of the analysis of a callstack. *)
+let register_start callstack current_time =
+  let kf = Callstack.top_kf callstack in
+  let kf_list = List.map fst !stack_timestamp in
+  stack_timestamp := (kf, current_time) :: !stack_timestamp;
+  match kf_list with
+  | [] ->
+    last_timestamp := current_time;
+    initialize_flamegraph ()
+  | kf_list ->
+    let last_duration = duration_since_last_timestamp current_time in
+    StatByCallstack.add ~called:kf ~self:last_duration kf_list;
+    update_flamegraph kf_list last_duration
+
+(* Called at the end of the analysis of a callstack. *)
+let register_stop _callstack current_time =
+  let kf_list = List.map fst !stack_timestamp in
+  match !stack_timestamp with
+  | [] -> assert false
+  | (_kf, start) :: tl ->
+    stack_timestamp := tl;
+    let last_duration = duration_since_last_timestamp current_time in
+    let total = duration start current_time in
+    StatByCallstack.add ~total ~self:last_duration kf_list;
+    update_flamegraph kf_list last_duration
 
-module Perf_by_callstack = Imperative_callstack_trie(struct
-    type t = perf_info
-    let default() =
-      { call_info_per_stack = Call_info.create() }
-  end)
+(* -------------------------------------------------------------------------- *)
+(*                    Compute execution time by function                      *)
+(* -------------------------------------------------------------------------- *)
 
-(* Head of the tree. Only the subtree field il really used.  *)
-let perf = Perf_by_callstack.empty();;
-let last_time_displayed = ref 0.0;;
-
-
-let print_indentation fmt n =
-  for _i = 0 to n-1 do Format.fprintf fmt "| " done;
-;;
-
-let rec display_node fmt kf indentation node curtime =
-  print_indentation fmt indentation;
-  Call_info.print fmt kf node.Perf_by_callstack.self.call_info_per_stack curtime;
-  display_subtree fmt (indentation+1) node.Perf_by_callstack.subtree
-    (Call_info.total_duration
-       curtime node.Perf_by_callstack.self.call_info_per_stack)
-    curtime
-
-and display_subtree fmt indentation subtree parent_duration curtime =
-  let entries = Call_info.filter_and_sort
-      (fun f -> Perf_by_callstack.Hashtbl.iter (fun k v -> f(k,v)) subtree)
-      (fun (_,node) -> node.Perf_by_callstack.self.call_info_per_stack)
-      parent_duration
-      curtime
+(* Returns the total duration of the analysis. *)
+let analysis_duration current_time =
+  match !stack_timestamp with
+  | [] ->
+    (* No analysis ongoing: use the duration of the main function. *)
+    let main, _ = Globals.entry_point () in
+    let stat = StatByCallstack.get [main] in
+    stat.total_duration
+  | list ->
+    (* Analysis in progress: diff between analysis start and current time. *)
+    let analysis_start = List.rev list |> List.hd |> snd in
+    duration analysis_start current_time
+
+(* Updates the total duration of [stat] by the current executing time if the
+   analysis of [kf] is ongoing. *)
+let complete_duration kf stat current_time =
+  let eq_kf t = Kernel_function.equal kf (fst t) in
+  match List.find_opt eq_kf !stack_timestamp with
+  | None -> stat
+  | Some (_kf, since) ->
+    let total_duration = stat.total_duration +. (duration since current_time) in
+    { stat with total_duration }
+
+(* Filters and sorts the [list] of pairs (kf, stat) according to total time. *)
+let filter_and_sort ~total_duration ~current_time list =
+  let limit = total_duration *. threshold in
+  let complete (kf, stat) = kf, complete_duration kf stat current_time in
+  let list = List.map complete list in
+  let filter (_kf, stat) = stat.total_duration > limit in
+  let filtered, others = List.partition filter list in
+  let cmp s1 s2 = Float.compare s2.total_duration s1.total_duration in
+  List.fast_sort (fun (_, s1) (_, s2) -> cmp s1 s2) filtered, others
+
+let merge_stat s1 s2 =
+  { nb_calls = s1.nb_calls + s2.nb_calls;
+    self_duration = s1.self_duration +. s2.self_duration;
+    total_duration = s1.total_duration +. s2.total_duration;
+    called = Kernel_function.Hptset.union s1.called s2.called; }
+
+(* Use recorded stats in StatByCallstack to compute stat by functions,
+   regardless of the callstack. Returns a list of the functions with the
+   longest total analysis time. Each function is associated to its stat
+   and those of all called functions. *)
+let compute_stat_by_fun ~total_duration ~current_time =
+  let module KfHashtbl = Kernel_function.Hashtbl in
+  let stat_by_fun = KfHashtbl.create 60 in
+  let stat_by_caller = KfHashtbl.create 60 in
+  let find_calls caller =
+    KfHashtbl.memo stat_by_caller caller (fun _ -> KfHashtbl.create 32)
   in
-  List.iter (fun ((kf,_),node) -> display_node fmt kf indentation node curtime) entries;
-;;
-
-let display fmt =
-  if Parameters.ValShowPerf.get()
-  then begin
-    Format.fprintf fmt "####### Value execution feedback #########\n";
-    let current_time = (Sys.time()) in
-    flat_print current_time fmt;
-    Format.fprintf fmt "\n";
-    Format.fprintf fmt "Execution time per callstack (includes current running time):\n";
-    Format.fprintf fmt "=============================================================\n";
-    display_subtree fmt 0 perf
-      (Call_info.total_duration current_time Call_info.main) current_time;
-    Format.fprintf fmt "################\n"
-  end
-;;
-
-let caller_callee_callinfo callstack =
-  match Callstack.top_caller callstack with
-  | Some caller_kf ->
-    let callee_kf = Callstack.top_kf callstack in
-    let caller_flat = Kernel_function.Hashtbl.find flat caller_kf in
-    (try
-       Kernel_function.Hashtbl.find caller_flat.called_functions callee_kf
-     with Not_found ->
-       let call_info = Call_info.create() in
-       Kernel_function.Hashtbl.add caller_flat.called_functions callee_kf call_info;
-       call_info)
-  | None -> Call_info.main
-;;
-
-let start_doing_perf callstack =
-  if Parameters.ValShowPerf.get()
-  then begin
-    let time = Sys.time() in
-    let kf = Callstack.top_kf callstack in
-    let flat_info =
-      try Kernel_function.Hashtbl.find flat kf
-      with Not_found ->
-        let flatp = flat_perf_create() in
-        Kernel_function.Hashtbl.add flat kf flatp; flatp
-    in
-
-    Call_info.before_call flat_info.call_info time;
-    Call_info.before_call (caller_callee_callinfo callstack) time;
-    let node = Perf_by_callstack.find perf callstack in
-    Call_info.before_call node.call_info_per_stack time;
-
-    if (duration !last_time_displayed time) > display_interval
-    then (last_time_displayed := time; Kernel.feedback "%t" display)
-  end
-;;
-
-let stop_doing_perf callstack =
-  if Parameters.ValShowPerf.get()
-  then begin
-    let time = Sys.time() in
-    let kf = Callstack.top_kf callstack in
-    let flat_info = Kernel_function.Hashtbl.find flat kf in
-    Call_info.after_call flat_info.call_info time;
-    let node = Perf_by_callstack.find perf callstack in
-    Call_info.after_call node.call_info_per_stack time;
-    Call_info.after_call (caller_callee_callinfo callstack) time;
-  end
-;;
-
-let reset_perf () =
-  let reset_callinfo ci =
-    ci.Call_info.nb_calls <- 0;
-    ci.Call_info.total_duration <- 0.0;
-    ci.Call_info.since <- []
+  let find_stat hashtbl kf = KfHashtbl.find_def hashtbl kf empty_stat in
+  let add_stat hashtbl kf new_stat =
+    let old_stat = find_stat hashtbl kf in
+    let stat = merge_stat old_stat new_stat in
+    KfHashtbl.replace hashtbl kf stat
   in
-  reset_callinfo Call_info.main;
-  Kernel_function.Hashtbl.clear flat;
-  last_time_displayed := 0.0;
-  Perf_by_callstack.reset perf
-;;
+  let process kf_list stat =
+    match kf_list with
+    | [] -> ()
+    | [ kf ] -> add_stat stat_by_fun kf stat
+    | kf :: caller :: _ ->
+      add_stat stat_by_fun kf stat;
+      add_stat (find_calls caller) kf stat;
+  in
+  StatByCallstack.iter process;
+  let list = KfHashtbl.to_seq stat_by_fun |> List.of_seq in
+  let filtered_sorted, _ = filter_and_sort ~total_duration ~current_time list in
+  let get_calls kf = find_calls kf |> KfHashtbl.to_seq |> List.of_seq in
+  List.map (fun (kf, stat) -> kf, (stat, get_calls kf)) filtered_sorted
 
 (* -------------------------------------------------------------------------- *)
-(* --- Flamegraphs                                                        --- *)
+(*                         Print execution feedback                           *)
 (* -------------------------------------------------------------------------- *)
 
-(* Set to [Some _] if option [-eva-flamegraph] is set and [main] is
-   currently being analyzed and the file is ok. Otherwise, set to [None]. *)
-let oc_fmt_flamegraph = ref None
-
-(* We cannot use a Callstack here because we ignore the call statements. *)
-module KfList = struct
-  include Datatype.List_with_collections(Cil_datatype.Kf)
-      (struct
-        let module_name = "Eva.KfList"
-      end)
-  let pretty ?(sep=format_of_string ";") fmt l =
-    Pretty_utils.pp_flowlist ~left:"" ~sep ~right:""
-      (fun fmt kf -> Kernel_function.pretty fmt kf)
-      fmt l
-end
-
-(* A mapping from callstacks to (time_of_last_call, total_duration).
-   [time_of_last_call] is the timestamp of the last time that the leaf function
-   in the callstack was called.
-   [total_duration] is the accumulated total amount of time spent in the
-   callstack.
-*)
-module EvaFlamegraph =
-  State_builder.Hashtbl
-    (KfList.Hashtbl)
-    (Datatype.Pair(Datatype.Float)(Datatype.Float))
-    (struct
-      let name = "Eva.Flamegraph"
-      let dependencies = [ Ast.self ]
-      let size = 20
-    end)
-
-(* update the [self_total_time] information for the function being analyzed,
-   assuming that the current time is [time] *)
-let update_self_total_time cl time =
-  try
-    let (start_caller, total) = EvaFlamegraph.find cl in
-    let d = duration start_caller time in
-    let new_total = d +. total in
-    EvaFlamegraph.replace cl (time, new_total);
-    new_total
-  with Not_found ->
-    Self.fatal
-      "EvaFlamegraph: caller list not found: %a"
-      (KfList.pretty ~sep:";") cl
-
-let start_call_flamegraph_main cl =
-  (* Analysis of main *)
-  EvaFlamegraph.clear ();
-  EvaFlamegraph.add cl (Sys.time (), 0.0);
-  if not (Parameters.ValPerfFlamegraphs.is_empty ()) then begin
-    let file = Parameters.ValPerfFlamegraphs.get () in
-    try
-      let oc = open_out (file:>string) in
-      oc_fmt_flamegraph := Some (oc, Format.formatter_of_out_channel oc);
-    with e ->
-      Self.error "cannot open flamegraph file: %s"
-        (Printexc.to_string e);
-      oc_fmt_flamegraph := None (* to be on the safe side  *)
-  end
-
-(* called when a new function is being analyzed *)
-let start_call_flamegraph ~prev cs =
-  let cl = Callstack.to_kf_list cs in
-  let prev = Option.map Callstack.to_kf_list prev in
-  match prev with
-  | None -> start_call_flamegraph_main cl
-  | Some prev ->
-    let time = Sys.time () in
-    ignore (update_self_total_time prev time);
-    let (_start, total) =
-      try EvaFlamegraph.find cl with Not_found -> (0.0, 0.0)
+(* Prints info on the analysis time of function [kf] given by [stat].
+   [calls] is the list of called functions with their own statistics. *)
+let print_function fmt current_time (kf, (stat, calls)) =
+  let total_duration = stat.total_duration in
+  Format.fprintf fmt "* %a: executed: %dx total: %.3fs@,"
+    Kernel_function.pretty kf stat.nb_calls total_duration;
+  let print_called_functions fmt =
+    let sorted, others = filter_and_sort ~total_duration ~current_time calls in
+    let nb_others = List.length others in
+    let others_duration =
+      List.fold_left (fun acc (_, stat) -> acc +. stat.total_duration) 0. others
     in
-    EvaFlamegraph.replace cl (time, total)
-;;
-
-(* called when the analysis of a function ends. This function is at the top
-   of [callstack] *)
-let end_call_flamegraph cs =
-  let cl = Callstack.to_kf_list cs in
-  let time = Sys.time () in
-  let total = update_self_total_time cl time in (* update current function *)
-  begin
-    match !oc_fmt_flamegraph with
-    | None -> ()
-    | Some (_, fmt) -> (* Flamegraphs are being written to a file *)
-      Format.fprintf fmt "%a %.3f\n%!"
-        (KfList.pretty ~sep:";") cl (total *. 1000.)
-  end
-
-let reset_flamegraph () =
-  EvaFlamegraph.clear ();
-  match !oc_fmt_flamegraph with
-  | None -> ()
-  | Some (oc, _) ->
-    close_out oc; oc_fmt_flamegraph := None
+    let percent duration = 100. *. duration /. total_duration in
+    let pp_duration fmt d = Format.fprintf fmt "%.3fs (%.1f%%)" d (percent d) in
+    let print_called (kf, stat) =
+      Format.fprintf fmt "| %a %dx %a@ "
+        Kernel_function.pretty kf stat.nb_calls pp_duration stat.total_duration;
+    in
+    List.iter print_called sorted;
+    if nb_others > 0 then
+      Format.fprintf fmt "| %d others: %a@ " nb_others pp_duration others_duration;
+    Format.fprintf fmt "| self: %a" pp_duration stat.self_duration
+  in
+  Format.fprintf fmt "  @[<hov>%t@]@," print_called_functions
+
+(* Prints info on the functions with the longest analysis time. *)
+let print_flat ~total_duration ~current_time fmt =
+  let list = compute_stat_by_fun ~total_duration ~current_time in
+  List.iter (print_function fmt current_time) list
+
+(* Prints execution time as a tree from the main function. *)
+let print_tree ~total_duration ~current_time fmt =
+  let rec print indent previous_callstack (kf, stat) =
+    for _i = 0 to indent-1 do Format.fprintf fmt "| " done;
+    Format.fprintf fmt "* %a: executed: %dx total: %.3fs@,"
+      Kernel_function.pretty kf stat.nb_calls stat.total_duration;
+    let callstack = kf :: previous_callstack in
+    let called = Kernel_function.Hptset.elements stat.called in
+    let find_stat kf = kf, StatByCallstack.get (kf :: callstack) in
+    let calls = List.map find_stat called in
+    let sorted, _ = filter_and_sort ~total_duration ~current_time calls in
+    List.iter (print (indent+1) callstack) sorted
+  in
+  let main, _ = Globals.entry_point () in
+  let stat = StatByCallstack.get [main] in
+  print 0 [] (main, complete_duration main stat current_time)
+
+let show_perf current_time fmt =
+  let total_duration = analysis_duration current_time in
+  Format.fprintf fmt
+    "@[<v> ######## Eva execution feedback ######## \
+     @,Long running functions:\
+     @,================================================================@,";
+  print_flat ~total_duration ~current_time fmt;
+  Format.fprintf fmt
+    "@,Execution time per callstack:\
+     @,================================================================@,";
+  print_tree ~total_duration ~current_time fmt;
+  Format.fprintf fmt " @,@]"
 
 (* -------------------------------------------------------------------------- *)
-(* --- Exported interface                                                 --- *)
+(*                            Exported functions                              *)
 (* -------------------------------------------------------------------------- *)
 
-let start_call ~prev cs =
-  start_doing_perf cs;
-  start_call_flamegraph ~prev cs
+let start callstack =
+  let current_time = Sys.time () in
+  register_start callstack current_time
 
-let end_call callgraph =
-  stop_doing_perf callgraph;
-  end_call_flamegraph callgraph
+let last_time_displayed = ref 0.0
 
-let reset () =
-  reset_perf ();
-  reset_flamegraph ()
+let stop callstack =
+  let current_time = Sys.time () in
+  register_stop callstack current_time;
+  if Parameters.ValShowPerf.get ()
+  && (duration !last_time_displayed current_time) > display_interval
+  then begin
+    last_time_displayed := current_time;
+    Self.feedback "%t" (show_perf current_time)
+  end
 
+let display fmt =
+  if Parameters.ValShowPerf.get ()
+  then show_perf (Sys.time ()) fmt
 
-(* TODO: Output files with more graphical outputs, such as
+let reset () =
+  StatByCallstack.clear ();
+  flamegraph_output := None;
+  stack_timestamp := [];
+  last_timestamp := 0.;
+  last_time_displayed := 0.
 
-   Gprof2dot-like output: (directory output the dot)
-   http://code.google.com/p/jrfonseca/wiki/Gprof2Dot
 
-   The latter would be useful to see when imbricated loops multiply
-   the number of calls to leaf functions.
+type 'a by_fun = (Cil_types.kernel_function * 'a) list
 
-   TODO: Also account for the memexec hit rate; and for the individual
-   execution time of derived plugins.
-*)
+let compute_stat_by_fun () : (stat * stat by_fun) by_fun =
+  let current_time = Sys.time () in
+  let total_duration = analysis_duration current_time in
+  compute_stat_by_fun ~total_duration ~current_time
diff --git a/src/plugins/eva/utils/eva_perf.mli b/src/plugins/eva/utils/eva_perf.mli
index 20a78d8f2586145482bded1d76791a6f3c1f2f99..26b934dcb007288e77862e43b3e8571a8aa525e0 100644
--- a/src/plugins/eva/utils/eva_perf.mli
+++ b/src/plugins/eva/utils/eva_perf.mli
@@ -20,28 +20,64 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Call [start_call] when starting analyzing a new function call.
-    The new function is on the top of the call stack.*)
-val start_call: prev:Callstack.t option -> Callstack.t -> unit
+(** Call [start] when starting analyzing a new callstack. *)
+val start: Callstack.t -> unit
 
-(** Call [end_call] when finishing analyzing a function. The
-    function must still be on the top of the call stack. *)
-val end_call: Callstack.t -> unit
+(** Call [stop] when finishing analyzing a callstack. *)
+val stop: Callstack.t -> unit
+
+(** Reset the internal state of the module. *)
+val reset: unit -> unit
 
 (** Display a complete summary of performance informations. Can be
     called during the analysis. *)
 val display: Format.formatter -> unit
 
-(** Reset the internal state of the module; to call at the very
-    beginning of the analysis. *)
-val reset: unit -> unit
+[@@@ api_start]
+(** Statistics about the analysis performance. *)
+
+(** Statistic about the analysis time of a function or a callstack. *)
+type stat = {
+  nb_calls: int;
+  (** How many times the given function or callstack has been analyzed. *)
+  self_duration: float;
+  (** Time spent analyzing the function or callstack itself. *)
+  total_duration: float;
+  (** Total time, including the analysis of other functions called. *)
+  called: Kernel_function.Hptset.t;
+  (** Set of functions called from this function or callstack. *)
+}
+
+type 'a by_fun = (Cil_types.kernel_function * 'a) list
+
+(** Returns a list of the functions with the longest total analysis time,
+    sorted by decreasing analysis time. Each function [f] is associated to
+    its stat and the unsorted list of stats of all function calls from [f]. *)
+val compute_stat_by_fun: unit -> (stat * stat by_fun) by_fun
+
+(** Statistics about each analyzed callstack. *)
+module StatByCallstack : sig
+  type callstack = Cil_types.kernel_function list
+
+  (** Get the current analysis statistic for a callstack. *)
+  val get: callstack -> stat
+
+  (** Iterate on the statistic of every analyzed callstack. *)
+  val iter: (callstack -> stat -> unit) -> unit
+
+  (** Set a hook on statistics computation *)
+  val add_hook_on_change:
+    ((callstack, stat) State_builder.hashtbl_event -> unit) -> unit
+  [@@@ api_end]
+
+  (** Sub-signature of [State_builder.Hashtbl] required by the server
+      to build synchronized arrays. *)
 
-module KfList : sig
-  include Datatype.S_with_collections with type t = Kernel_function.t list
-  val pretty : ?sep:Pretty_utils.sformat -> Format.formatter ->
-    Kernel_function.t list -> unit
+  type key = Cil_types.kernel_function list
+  type data = stat
+  module Datatype: Datatype.S
+  val add_hook_on_update: (Datatype.t -> unit) -> unit
+  [@@@ api_start]
 end
 
-module EvaFlamegraph :
-  State_builder.Hashtbl with type key = KfList.t
-                         and type data = float * float
+[@@@ api_end]
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index eafb7d948df2fca06a4cc9932f78d69d51e04f4d..c155a98f54ee96cc2359f9dc393173b0db11fa40 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -30,14 +30,14 @@ let clear_call_stack () =
   match !current_callstack with
   | None -> ()
   | Some cs ->
-    Eva_perf.end_call cs;
+    Eva_perf.stop cs;
     current_callstack := None
 
 let init_call_stack kf =
   assert (!current_callstack = None);
   let cs = Callstack.init kf in
   current_callstack := Some cs;
-  Eva_perf.start_call ~prev:None cs;
+  Eva_perf.start cs;
   cs
 
 let current_call_stack_opt () = !current_callstack
@@ -55,11 +55,11 @@ let push_call_stack kf stmt =
   let cs = current_call_stack () in
   let new_cs = Callstack.push kf stmt cs in
   current_callstack := Some new_cs;
-  Eva_perf.start_call ~prev:(Some cs) new_cs
+  Eva_perf.start new_cs
 
 let pop_call_stack () =
   let cs = current_call_stack () in
-  Eva_perf.end_call cs;
+  Eva_perf.stop cs;
   current_callstack := Callstack.pop cs
 
 let pp_callstack fmt =