diff --git a/.gitignore b/.gitignore
index ff935dfef44e08ebbb11a4f7154ac69cc577441b..b458e734ce8fc11f52dd8058aeef29319dba8dfc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,6 +52,7 @@ autom4te.cache
 /tests/crowbar/mutable
 /tests/crowbar/output-*
 /tests/crowbar/test_ghost_cfg
+/tests/fc_script/compile_commands.json
 /tests/journal/intra.byte
 /tests/misc/my_visitor_plugin/my_visitor.opt
 /tests/misc/my_visitor.sav
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 1be1e161e81026b4b4d255c1605fdd11f083defa..29c9a4cd9dde7ab4f822819bf4728be65fc70dd2 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1072,8 +1072,8 @@ the sequence above is read in order and defines a configuration level
   \texttt{CMD}\nscodeidx{Test!Directive}{CMD} is the last
   \texttt{CMD} directive of the preceding configuration level.
 \item \texttt{LOG} adds a file to be compared against an oracle in the
-  next \texttt{OPT} directive. Several files can be monitored from a single
-  \texttt{OPT} directive, through several \texttt{LOG} directives. 
+  next \texttt{OPT} or \texttt{STDOPT} directive. Several files can be monitored from a single
+  \texttt{OPT}/\texttt{STDOPT} directive, through several \texttt{LOG} directives. 
   These files must be generated in the result
   directory of the corresponding suite (and potentially alternative
   configuration).
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 40a4d2de7092bde02271d9a7337b0753b5152225..e307c4a3ff53dc881203ac54caa0558e0ab79a40 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -785,13 +785,12 @@ let config_options =
        let new_top =
          List.map
            (fun (cmd,opts, log, macros,_) ->
-              cmd, make_custom_opts opts s, log,
+              cmd, make_custom_opts opts s, log @ current.dc_default_log,
               current.dc_macros, current.dc_timeout)
            !current_default_cmds
        in
        { current with dc_toplevels = new_top @ current.dc_toplevels;
-                      dc_default_log = !current_default_log @
-                                       current.dc_default_log });
+                      dc_default_log = !current_default_log });
 
     "FILEREG",
     (fun _ s current -> { current with dc_test_regexp = s });
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index 6e8cc4b68f7771060214537bbe16865d7ea0904f..68210ab38d896d6da3b75e0dc1ddca83914a44fd 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -315,7 +315,10 @@ let dump () =
       let fmt = Format.formatter_of_out_channel chan in
       (match Metrics_base.get_file_type out with
             | Metrics_base.Html -> dump_acsl_stats_html fmt
-            | Metrics_base.Text -> dump_acsl_stats fmt);
+            | Metrics_base.Text -> dump_acsl_stats fmt
+            | Metrics_base.Json ->
+              raise (Log.FeatureRequest ("Metrics", "JSON format for ACSL metrics"))
+      );
       close_out chan
     with Sys_error s ->
       Metrics_parameters.abort "Cannot open file %s (%s)" out s
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index baf2ca5fd2b43f6e3bb9a1f82b6e8621948e722e..f39592a07eb42ec3a47de75bc6ac63ee797cdebc 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -248,6 +248,7 @@ let get_suffix filename =
 type output_type =
   | Html
   | Text
+  | Json
 ;;
 
 let get_file_type filename =
@@ -255,6 +256,7 @@ let get_file_type filename =
     match get_suffix filename with
       | "html" | "htm" -> Html
       | "txt" | "text" -> Text
+      | "json" -> Json
       | s ->
         Metrics_parameters.abort
           "Unknown file extension %s. Cannot produce output.@." s
@@ -285,6 +287,16 @@ let pretty_set fmt s =
     s;
   Format.fprintf fmt "@]"
 
+let json_of_varinfo_map m =
+  let elems = VInfoMap.fold (fun f n acc ->
+      let calls = ("calls", `Int n) in
+      let address_taken = ("address_taken", `Bool f.vaddrof) in
+      let elem = `Assoc [(f.vname, `Assoc ([calls; address_taken]))] in
+      elem :: acc
+    ) m []
+  in
+  `List (List.rev elems)
+
 let pretty_extern_vars fmt s =
   Pretty_utils.pp_iter ~pre:"@[" ~suf:"@]" ~sep:";@ "
     VInfoSet.iter Printer.pp_varinfo fmt s
@@ -312,6 +324,16 @@ let pretty_entry_points  fmt fs =
   Format.fprintf fmt "@[<hov 1>%a@]" print fs;
 ;;
 
+let json_of_entry_points m =
+  `List
+    (List.rev
+       (VInfoMap.fold
+          (fun vi n acc ->
+             if is_entry_point vi n then `String vi.vname :: acc
+             else acc)
+          m [])
+    )
+
 (* Utilities for CIL ASTs *)
 
 let file_of_vinfodef fvinfo =
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index bd8b85522c181da835fdfc7c4e1fc0d628978db6..1b209bbd078e665182942b0bba4e0c18d96e3e21 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -108,6 +108,10 @@ val pretty_set : Format.formatter -> int VInfoMap.t -> unit
 
 val pretty_extern_vars: Format.formatter -> VInfoSet.t -> unit
 
+(** Build a JSON list with the varinfos in [m], each as a JSON object with
+    the varinfo name as key and additional attributes as values. *)
+val json_of_varinfo_map : int VInfoMap.t -> Yojson.t
+
 (** Handling entry points informations *)
 val number_entry_points : int VInfoMap.t -> int
 ;;
@@ -116,6 +120,8 @@ val pretty_entry_points :
   Format.formatter -> int VInfoMap.t -> unit
 ;;
 
+val json_of_entry_points : int VInfoMap.t -> Yojson.t
+
 (** Get the filename where the definition of a varinfo occurs *)
 val file_of_vinfodef: Cil_types.varinfo -> Datatype.Filepath.t;;
 
@@ -133,6 +139,7 @@ val get_filename: Cabs.definition -> Datatype.Filepath.t;;
 type output_type =
   | Html
   | Text
+  | Json
 ;;
 
 (** get_file_type [extension] sets the output type according to [extension].
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 88dc82d6538964a15a5d664d9bbb345c55e59d4d..8c737e2c13e7a7f25666c6870d107b7433be8568 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -662,6 +662,28 @@ let pp_funinfo fmt vis =
     Metrics_base.pretty_entry_points vis#fundef_calls
 ;;
 
+let json_of_funinfo vis =
+  let fundef =
+    ("defined-functions", json_of_varinfo_map vis#fundef_calls)
+  in
+  let funspec =
+    ("specified-only-functions", json_of_varinfo_map vis#funspec_calls)
+  in
+  let fundecl =
+    ("undefined-functions", json_of_varinfo_map vis#fundecl_calls)
+  in
+  let extern_vars =
+    VInfoSet.fold (fun vi acc -> `String vi.vname :: acc)
+      vis#extern_global_vars []
+  in
+  let extern =
+    ("extern-global-vars", `List (List.rev extern_vars))
+  in
+  let entry_points =
+    ("entry-points", json_of_entry_points vis#fundef_calls)
+  in
+  `Assoc [fundef; funspec; fundecl; extern; entry_points]
+
 let pp_with_funinfo fmt cil_visitor =
   Format.fprintf fmt "@[<v 0>%a@ %a@]"
     pp_funinfo cil_visitor
@@ -721,6 +743,9 @@ let compute_on_cilast ~libc =
         (match Metrics_base.get_file_type out_fname with
          | Html -> dump_html fmt cil_visitor
          | Text -> pp_with_funinfo fmt cil_visitor
+         | Json ->
+           let json = json_of_funinfo cil_visitor in
+           Yojson.pretty_print fmt json
         );
         close_out oc;
       with Sys_error _ ->
diff --git a/src/plugins/metrics/metrics_parameters.ml b/src/plugins/metrics/metrics_parameters.ml
index 9d9127573bcc5b44b29f991cfc1417418c0af55b..5d9bd963dbf2187682089cc8b9581ef220e9c366 100644
--- a/src/plugins/metrics/metrics_parameters.ml
+++ b/src/plugins/metrics/metrics_parameters.ml
@@ -49,7 +49,8 @@ module OutputFile =
       let option_name = "-metrics-output"
       let arg_name = "filename"
       let help = "print some metrics into the specified file; \
-                  the output format is recognized through the extension."
+                  the output format is recognized through the extension: \
+                  .text/.txt for text, .html/.htm for HTML, or .json for JSON."
      end)
 
 module ValueCoverage =
diff --git a/tests/metrics/libc.c b/tests/metrics/libc.c
index c9c41a18762157b7fe04cf2289fd0ee154a0fb75..83556b3d9b4e6b4042873d240ba90e708637d16c 100644
--- a/tests/metrics/libc.c
+++ b/tests/metrics/libc.c
@@ -1,6 +1,8 @@
 /* run.config
    STDOPT: #"-metrics-no-libc -metrics-eva-cover"
    STDOPT: #"-metrics-libc -metrics-eva-cover"
+   LOG: libc.json
+   STDOPT: #"-metrics-libc -metrics-output @PTEST_DIR@/result/libc.json"
 */
 #include <ctype.h>
 #include <stdio.h> // defines external variables
@@ -21,6 +23,8 @@ int g() { // called via fp
   return isalpha(42);
 }
 
+int h() { return 0; }
+
 int (*fp)() = g;
 
 int getopt(int argc, char * const argv[],
@@ -31,5 +35,6 @@ int getopt(int argc, char * const argv[],
 int main() {
   fp();
   getopt(0, 0, 0);
+  h();
   return isblank(0);
 }
diff --git a/tests/metrics/oracle/libc.0.res.oracle b/tests/metrics/oracle/libc.0.res.oracle
index 1742799970db9aaf042da8cb6a6a88c3b2064fb1..1353173e068a981eaaf29cb891c1cd3d0f2ab6bb 100644
--- a/tests/metrics/oracle/libc.0.res.oracle
+++ b/tests/metrics/oracle/libc.0.res.oracle
@@ -1,8 +1,8 @@
 [kernel] Parsing tests/metrics/libc.c (with preprocessing)
-[metrics] Defined functions (5)
+[metrics] Defined functions (6)
   =====================
    bar (0 call); f (0 call); foo (0 call); g (address taken) (0 call);
-   main (0 call); 
+   h (1 call); main (0 call); 
   
   Specified-only functions (0)
   ============================
@@ -22,18 +22,18 @@
   
   Global metrics
   ============== 
-  Sloc = 12
+  Sloc = 15
   Decision point = 0
   Global variables = 1
   If = 0
   Loop = 0
   Goto = 0
-  Assignment = 5
-  Exit point = 5
-  Function = 5
-  Function call = 5
+  Assignment = 6
+  Exit point = 6
+  Function = 6
+  Function call = 6
   Pointer dereferencing = 1
-  Cyclomatic complexity = 5
+  Cyclomatic complexity = 6
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -44,8 +44,8 @@
 [eva] done for function main
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  4 functions analyzed (out of 5): 80% coverage.
-  In these functions, 10 statements reached (out of 10): 100% coverage.
+  5 functions analyzed (out of 6): 83% coverage.
+  In these functions, 13 statements reached (out of 13): 100% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
@@ -58,15 +58,16 @@
   ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
-  Syntactically reachable functions = 4 (out of 5)
-  Semantically reached functions = 4
+  Syntactically reachable functions = 5 (out of 6)
+  Semantically reached functions = 5
   Coverage estimation = 100.0%
 [metrics] References to non-analyzed functions
   ------------------------------------
 [metrics] Statements analyzed by Eva
   --------------------------
-  10 stmts in analyzed functions, 10 stmts analyzed (100.0%)
+  13 stmts in analyzed functions, 13 stmts analyzed (100.0%)
   bar: 2 stmts out of 2 (100.0%)
   foo: 2 stmts out of 2 (100.0%)
   g: 2 stmts out of 2 (100.0%)
-  main: 4 stmts out of 4 (100.0%)
+  h: 2 stmts out of 2 (100.0%)
+  main: 5 stmts out of 5 (100.0%)
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index 690ea20f9c48ac4bf117fb98c399422473ffa09e..d92d25d82ea958fd39f5c38000f47e44e1bd1080 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -1,8 +1,8 @@
 [kernel] Parsing tests/metrics/libc.c (with preprocessing)
-[metrics] Defined functions (6)
+[metrics] Defined functions (7)
   =====================
    bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
-   getopt (1 call); main (0 call); 
+   getopt (1 call); h (1 call); main (0 call); 
   
   Specified-only functions (122)
   ==============================
@@ -55,18 +55,18 @@
   
   Global metrics
   ============== 
-  Sloc = 17
+  Sloc = 20
   Decision point = 0
   Global variables = 17
   If = 0
   Loop = 0
   Goto = 0
-  Assignment = 8
-  Exit point = 6
-  Function = 128
-  Function call = 7
+  Assignment = 9
+  Exit point = 7
+  Function = 129
+  Function call = 8
   Pointer dereferencing = 1
-  Cyclomatic complexity = 6
+  Cyclomatic complexity = 7
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -77,8 +77,8 @@
 [eva] done for function main
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  4 functions analyzed (out of 5): 80% coverage.
-  In these functions, 10 statements reached (out of 10): 100% coverage.
+  5 functions analyzed (out of 6): 83% coverage.
+  In these functions, 13 statements reached (out of 13): 100% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
@@ -91,16 +91,17 @@
   ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
-  Syntactically reachable functions = 7 (out of 128)
-  Semantically reached functions = 7
+  Syntactically reachable functions = 8 (out of 129)
+  Semantically reached functions = 8
   Coverage estimation = 100.0%
 [metrics] References to non-analyzed functions
   ------------------------------------
 [metrics] Statements analyzed by Eva
   --------------------------
-  15 stmts in analyzed functions, 15 stmts analyzed (100.0%)
+  18 stmts in analyzed functions, 18 stmts analyzed (100.0%)
   bar: 2 stmts out of 2 (100.0%)
   foo: 2 stmts out of 2 (100.0%)
   g: 2 stmts out of 2 (100.0%)
   getopt: 5 stmts out of 5 (100.0%)
-  main: 4 stmts out of 4 (100.0%)
+  h: 2 stmts out of 2 (100.0%)
+  main: 5 stmts out of 5 (100.0%)
diff --git a/tests/metrics/oracle/libc.2.res.oracle b/tests/metrics/oracle/libc.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..eeb5977dbc5fef0789c0e314ec2e68f5834bd8d2
--- /dev/null
+++ b/tests/metrics/oracle/libc.2.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/metrics/libc.c (with preprocessing)
diff --git a/tests/metrics/oracle/libc.3.res.oracle b/tests/metrics/oracle/libc.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..eeb5977dbc5fef0789c0e314ec2e68f5834bd8d2
--- /dev/null
+++ b/tests/metrics/oracle/libc.3.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/metrics/libc.c (with preprocessing)
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
new file mode 100644
index 0000000000000000000000000000000000000000..5f7f5afbe20178035e1de51267e1ba2ef1acce15
--- /dev/null
+++ b/tests/metrics/oracle/libc.json
@@ -0,0 +1,141 @@
+{
+  "defined-functions": [
+    { "bar": { "calls": 1, "address_taken": false } },
+    { "f": { "calls": 0, "address_taken": false } },
+    { "foo": { "calls": 1, "address_taken": false } },
+    { "g": { "calls": 0, "address_taken": true } },
+    { "getopt": { "calls": 1, "address_taken": false } },
+    { "h": { "calls": 1, "address_taken": false } },
+    { "main": { "calls": 0, "address_taken": false } }
+  ],
+  "specified-only-functions": [
+    { "_exit": { "calls": 0, "address_taken": false } },
+    { "access": { "calls": 0, "address_taken": false } },
+    { "chdir": { "calls": 0, "address_taken": false } },
+    { "chown": { "calls": 0, "address_taken": false } },
+    { "chroot": { "calls": 0, "address_taken": false } },
+    { "clearerr": { "calls": 0, "address_taken": false } },
+    { "clearerr_unlocked": { "calls": 0, "address_taken": false } },
+    { "close": { "calls": 0, "address_taken": false } },
+    { "dup": { "calls": 0, "address_taken": false } },
+    { "dup2": { "calls": 0, "address_taken": false } },
+    { "execl": { "calls": 0, "address_taken": false } },
+    { "execle": { "calls": 0, "address_taken": false } },
+    { "execlp": { "calls": 0, "address_taken": false } },
+    { "execv": { "calls": 0, "address_taken": false } },
+    { "execve": { "calls": 0, "address_taken": false } },
+    { "execvp": { "calls": 0, "address_taken": false } },
+    { "fclose": { "calls": 0, "address_taken": false } },
+    { "fdopen": { "calls": 0, "address_taken": false } },
+    { "feof": { "calls": 0, "address_taken": false } },
+    { "feof_unlocked": { "calls": 0, "address_taken": false } },
+    { "ferror": { "calls": 0, "address_taken": false } },
+    { "ferror_unlocked": { "calls": 0, "address_taken": false } },
+    { "fflush": { "calls": 0, "address_taken": false } },
+    { "fgetc": { "calls": 0, "address_taken": false } },
+    { "fgetpos": { "calls": 0, "address_taken": false } },
+    { "fgets": { "calls": 0, "address_taken": false } },
+    { "fileno": { "calls": 0, "address_taken": false } },
+    { "fileno_unlocked": { "calls": 0, "address_taken": false } },
+    { "flockfile": { "calls": 0, "address_taken": false } },
+    { "fopen": { "calls": 0, "address_taken": false } },
+    { "fork": { "calls": 0, "address_taken": false } },
+    { "fputc": { "calls": 0, "address_taken": false } },
+    { "fputs": { "calls": 0, "address_taken": false } },
+    { "fread": { "calls": 0, "address_taken": false } },
+    { "freopen": { "calls": 0, "address_taken": false } },
+    { "fseek": { "calls": 0, "address_taken": false } },
+    { "fseeko": { "calls": 0, "address_taken": false } },
+    { "fsetpos": { "calls": 0, "address_taken": false } },
+    { "ftell": { "calls": 0, "address_taken": false } },
+    { "ftello": { "calls": 0, "address_taken": false } },
+    { "ftrylockfile": { "calls": 0, "address_taken": false } },
+    { "funlockfile": { "calls": 0, "address_taken": false } },
+    { "fwrite": { "calls": 0, "address_taken": false } },
+    { "getc": { "calls": 0, "address_taken": false } },
+    { "getc_unlocked": { "calls": 0, "address_taken": false } },
+    { "getchar": { "calls": 1, "address_taken": false } },
+    { "getchar_unlocked": { "calls": 0, "address_taken": false } },
+    { "getcwd": { "calls": 0, "address_taken": false } },
+    { "getegid": { "calls": 0, "address_taken": false } },
+    { "geteuid": { "calls": 0, "address_taken": false } },
+    { "getgid": { "calls": 0, "address_taken": false } },
+    { "gethostname": { "calls": 0, "address_taken": false } },
+    { "getopt_long": { "calls": 0, "address_taken": false } },
+    { "getopt_long_only": { "calls": 0, "address_taken": false } },
+    { "getpgid": { "calls": 0, "address_taken": false } },
+    { "getpgrp": { "calls": 0, "address_taken": false } },
+    { "getpid": { "calls": 0, "address_taken": false } },
+    { "getppid": { "calls": 0, "address_taken": false } },
+    { "getresgid": { "calls": 0, "address_taken": false } },
+    { "getresuid": { "calls": 0, "address_taken": false } },
+    { "gets": { "calls": 0, "address_taken": false } },
+    { "getsid": { "calls": 0, "address_taken": false } },
+    { "getuid": { "calls": 0, "address_taken": false } },
+    { "isalnum": { "calls": 0, "address_taken": false } },
+    { "isalpha": { "calls": 1, "address_taken": false } },
+    { "isascii": { "calls": 0, "address_taken": false } },
+    { "isatty": { "calls": 0, "address_taken": false } },
+    { "isblank": { "calls": 1, "address_taken": false } },
+    { "iscntrl": { "calls": 0, "address_taken": false } },
+    { "isdigit": { "calls": 0, "address_taken": false } },
+    { "isgraph": { "calls": 0, "address_taken": false } },
+    { "islower": { "calls": 0, "address_taken": false } },
+    { "isprint": { "calls": 0, "address_taken": false } },
+    { "ispunct": { "calls": 0, "address_taken": false } },
+    { "isspace": { "calls": 0, "address_taken": false } },
+    { "isupper": { "calls": 0, "address_taken": false } },
+    { "isxdigit": { "calls": 0, "address_taken": false } },
+    { "lseek": { "calls": 0, "address_taken": false } },
+    { "pathconf": { "calls": 0, "address_taken": false } },
+    { "pclose": { "calls": 0, "address_taken": false } },
+    { "perror": { "calls": 0, "address_taken": false } },
+    { "pipe": { "calls": 0, "address_taken": false } },
+    { "popen": { "calls": 0, "address_taken": false } },
+    { "putc": { "calls": 0, "address_taken": false } },
+    { "putc_unlocked": { "calls": 0, "address_taken": false } },
+    { "putchar": { "calls": 0, "address_taken": false } },
+    { "putchar_unlocked": { "calls": 0, "address_taken": false } },
+    { "puts": { "calls": 0, "address_taken": false } },
+    { "read": { "calls": 0, "address_taken": false } },
+    { "remove": { "calls": 0, "address_taken": false } },
+    { "rename": { "calls": 0, "address_taken": false } },
+    { "rewind": { "calls": 0, "address_taken": false } },
+    { "setbuf": { "calls": 0, "address_taken": false } },
+    { "setegid": { "calls": 0, "address_taken": false } },
+    { "seteuid": { "calls": 0, "address_taken": false } },
+    { "setgid": { "calls": 0, "address_taken": false } },
+    { "sethostname": { "calls": 0, "address_taken": false } },
+    { "setpgid": { "calls": 0, "address_taken": false } },
+    { "setregid": { "calls": 0, "address_taken": false } },
+    { "setresgid": { "calls": 0, "address_taken": false } },
+    { "setresuid": { "calls": 0, "address_taken": false } },
+    { "setreuid": { "calls": 0, "address_taken": false } },
+    { "setsid": { "calls": 0, "address_taken": false } },
+    { "setuid": { "calls": 0, "address_taken": false } },
+    { "setvbuf": { "calls": 0, "address_taken": false } },
+    { "sync": { "calls": 0, "address_taken": false } },
+    { "sysconf": { "calls": 0, "address_taken": false } },
+    { "tmpfile": { "calls": 0, "address_taken": false } },
+    { "tmpnam": { "calls": 0, "address_taken": false } },
+    { "tolower": { "calls": 0, "address_taken": false } },
+    { "toupper": { "calls": 0, "address_taken": false } },
+    { "ttyname": { "calls": 0, "address_taken": false } },
+    { "ungetc": { "calls": 0, "address_taken": false } },
+    { "unlink": { "calls": 0, "address_taken": false } },
+    { "usleep": { "calls": 0, "address_taken": false } },
+    { "vfprintf": { "calls": 0, "address_taken": false } },
+    { "vfscanf": { "calls": 0, "address_taken": false } },
+    { "vprintf": { "calls": 0, "address_taken": false } },
+    { "vscanf": { "calls": 0, "address_taken": false } },
+    { "vsnprintf": { "calls": 0, "address_taken": false } },
+    { "vsprintf": { "calls": 0, "address_taken": false } },
+    { "write": { "calls": 0, "address_taken": false } }
+  ],
+  "undefined-functions": [],
+  "extern-global-vars": [
+    "Frama_C_entropy_source", "__fc_errno", "__fc_hostname", "__fc_stdin",
+    "__fc_stdout", "__fc_ttyname", "optarg", "opterr", "optind", "optopt"
+  ],
+  "entry-points": [ "f", "main" ]
+}
\ No newline at end of file