ptests/ptests.ml

@@ -71,6 +71,20 @@ let str_global_replace regex repl s =
   let res = Str.global_replace regex repl s in
   Mutex.unlock str_mutex; res
 
+(* The match may start after [pos] (instead of [str_string_match]) *)
+let str_string_contains regexp s pos =
+  Mutex.lock str_mutex;
+  let res = try
+      ignore (Str.search_forward regexp s pos) ;
+      true
+    with Not_found -> false
+  in
+  Mutex.unlock str_mutex; res
+
+let str_string_contains_option opt =
+  let re = Str.regexp ("\\( \\|^\\)"^ opt ^ "\\( \\|=\\|$\\)") in
+  str_string_contains re
+
 let str_string_match regex s n =
   Mutex.lock str_mutex;
   let res = Str.string_match regex s n in
@@ -344,7 +358,7 @@ let macro_options = ref "@PTEST_PRE_OPTIONS@ @PTEST_OPT@ @PTEST_POST_OPTIONS@"
 let macro_default_options = ref "-journal-disable -check -no-autoload-plugins"
 
 let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
-let macro_frama_c      = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
+let macro_frama_c     = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
 let default_toplevel = ref "@frama-c@"
 
 (* Those variables are read from a ptests_config file *)
@@ -771,7 +785,11 @@ struct
       let has_frama_c_exe = ref false in
       if !verbosity >= 4 then lock_printf "%% Expand: %s@." s;
       if !verbosity >= 5 then print_macros macros;
+      let nb_loops = ref 0 in
       let rec aux s =
+        if !nb_loops > 100 then
+          fail "Possible infinite recursion in macro expands"
+        else incr nb_loops ;
         let expand_macro = function
           | Str.Text s -> s
           | Str.Delim s ->
@@ -812,14 +830,9 @@ struct
 
   let expand_directive =
     let deprecated_opts = "(-load-module|-load-script)" in
-    let re = Str.regexp "\\(-load-module\\|-load-script\\)" in
+    let contains_deprecated_opts = str_string_contains_option "\\(-load-module\\|-load-script\\)" in
     fun ~file macros s ->
-      Mutex.lock str_mutex;
-      let contains =
-        try ignore (Str.search_forward re s 0); true
-        with Not_found -> false
-      in
-      Mutex.unlock str_mutex;
+      let contains = contains_deprecated_opts s 0 in
       if contains then lock_eprintf "%s: DEPRECATED direct use of %s option: %s@.Please use PLUGIN, MODULE, SCRIPT or LIBS directive instead of the deprecated option.@." file deprecated_opts s;
       expand macros s
 
@@ -1576,23 +1589,21 @@ end = struct
     let process_macros s = Macros.expand macros s in
     let toplevel =
       let toplevel = log_default_filter cmd.toplevel in
-      let in_toplevel,toplevel= Macros.does_expand macros toplevel in
-      if not cmd.execnow then begin
-        let has_ptest_file, options =
-          if in_toplevel.has_ptest_opt then in_toplevel.has_ptest_file, []
-          else
-            let in_option,options= Macros.does_expand macros cmd.options in
-            (in_option.has_ptest_file || in_toplevel.has_ptest_file),
-            (if in_toplevel.has_frama_c_exe then
-               [ process_macros "@PTEST_PRE_OPTIONS@" ;
-                 options ;
-                 process_macros "@PTEST_POST_OPTIONS@" ;
-               ]
-             else [ options ])
+      let in_toplevel,toplevel = Macros.does_expand macros toplevel in
+      if cmd.execnow || in_toplevel.has_ptest_opt then toplevel
+      else begin
+        let has_ptest_file,options =
+          let in_option,options = Macros.does_expand macros cmd.options in
+          (in_option.has_ptest_file || in_toplevel.has_ptest_file),
+          (if in_toplevel.has_frama_c_exe then
+             [ process_macros "@PTEST_PRE_OPTIONS@" ;
+               options ;
+               process_macros "@PTEST_POST_OPTIONS@" ;
+             ]
+           else [ options ])
         in
         String.concat " " (toplevel::(if has_ptest_file then options else ptest_file::options))
       end
-      else toplevel
     in
     let toplevel = get_ptest_toplevel cmd (dune_feature_cmd toplevel) in
     { cmd with

share/libc/stdio.c

@@ -21,6 +21,7 @@
 /**************************************************************************/
 
 #include "__fc_builtin.h"
+#include "stdbool.h"
 #include "stdio.h"
 #include "stdlib.h"
 #include "stdint.h" // for SIZE_MAX
@@ -37,6 +38,26 @@ FILE * __fc_stderr = &__fc_initial_stderr;
 FILE __fc_initial_stdin = {.__fc_FILE_id=0}; 
 FILE * __fc_stdin = &__fc_initial_stdin;
 
+// Returns 1 iff mode contains a valid mode string for fopen() and
+// related functions; that is, one of the following:
+// "r","w","a","rb","wb","ab","r+","w+","a+",
+// "rb+","r+b","wb+","w+b","ab+","a+b".
+/*@
+  requires valid_mode: valid_read_string(mode);
+ */
+static bool is_valid_mode(char const *mode) {
+  if (!(mode[0] != 'r' || mode[0] != 'w' || mode[0] != 'a')) return false;
+  // single-char mode string; ok
+  if (!mode[1]) return true;
+  // two- or three-char mode string
+  if (!(mode[1] != 'b' || mode[1] != '+')) return false;
+  // two-char mode string; ok
+  if (!mode[2]) return true;
+  if (mode[2] == mode[1] || !(mode[2] != 'b' || mode[2] != '+')) return false;
+  // a three-char mode string is ok; everything else is not
+  return !mode[3];
+}
+
 // inefficient but POSIX-conforming implementation of getline
 ssize_t getline(char **lineptr, size_t *n, FILE *stream) {
   if (!lineptr || !n || !stream) {
@@ -111,5 +132,43 @@ int asprintf(char **strp, const char *fmt, ...) {
   return len;
 }
 
+// TODO: this stub does not ensure that, when fclose is called on the
+// stream, the memory allocated here will be freed.
+// (there is currently no metadata field in FILE for this information).
+FILE *fmemopen(void *restrict buf, size_t size,
+               const char *restrict mode) {
+  if (!is_valid_mode(mode)) {
+    errno = EINVAL;
+    return NULL;
+  }
+  if (!buf) {
+    if (size == 0) {
+      // Some implementations may not support this; non-deterministically
+      // return an error
+      if (Frama_C_interval(0, 1)) {
+        errno = EINVAL;
+        return NULL;
+      }
+    }
+    if (mode[1] != '+' && (mode[1] && mode[2] != '+')) {
+      // null buffer requires an update ('+') mode
+      errno = EINVAL;
+      return NULL;
+    }
+    buf = malloc(size);
+    if (!buf) {
+      errno = ENOMEM;
+      return NULL;
+    }
+  }
+  // Code to emulate a possible exhaustion of open streams; there is currently
+  // no metadata in the FILE structure to indicate when a stream is available.
+  if (Frama_C_interval(0, 1)) {
+    // emulate 'too many open streams'
+    errno = EMFILE;
+    return NULL;
+  }
+  return &__fc_fopen[Frama_C_interval(0, __FC_FOPEN_MAX-1)];
+}
 
 __POP_FC_STDLIB

share/libc/stdio.h

@@ -583,6 +583,24 @@ extern int pclose(FILE *stream);
 ssize_t getline(char **lineptr, size_t *n, FILE *stream);
 #endif
 
+// POSIX extension
+/*@
+  requires valid_or_null_buff: buf == \null || \valid((char*)buf + (0 .. size-1));
+  requires valid_mode: valid_read_string(mode);
+  assigns __fc_errno \from indirect: buf, indirect: size,
+                           indirect: mode[0..strlen(mode)];
+  assigns \result \from __fc_p_fopen,
+  indirect: buf, indirect: size, indirect: mode[0..strlen(mode)];
+  ensures result_error_or_valid:
+    \result == \null || \result \in &__fc_fopen[0 .. __FC_FOPEN_MAX-1];
+  ensures errno_set:
+    __fc_errno == \old(errno) ||
+    __fc_errno \in {EINVAL, EMFILE, ENOMEM};
+  allocates buf;
+*/
+extern FILE *fmemopen(void *restrict buf, size_t size,
+                      const char *restrict mode);
+
 // Non-POSIX; allocates memory, so requires 'stdio.c' to be included
 
 #include "__fc_alloc_axiomatic.h"

src/kernel_internals/parsing/errorloc.ml

@@ -46,13 +46,11 @@
 (***** Handling parsing errors ********)
 type parseinfo = {
   lexbuf : Lexing.lexbuf;
-  inchan : in_channel;
   mutable current_working_directory : string option;
 }
 
 let dummyinfo = {
   lexbuf    = Lexing.from_string "";
-  inchan    = stdin;
   current_working_directory = None;
 }
 
@@ -66,28 +64,26 @@ let startParsing fname =
        You want to open %S and %S is still open"
       fname (Lexing.lexeme_start_p !current.lexbuf).Lexing.pos_fname
   end;
-  let inchan =
-    try open_in_bin fname
-    with Sys_error s ->
-      Kernel.abort "Cannot find input file %S: %s" fname s
-  in
-  let lexbuf = Lexing.from_channel inchan in
-  let filename = Filepath.normalize fname in
-  let i = { lexbuf; inchan; current_working_directory = None } in
-  (* Initialize lexer buffer. *)
-  lexbuf.Lexing.lex_curr_p <-
-    { Lexing.pos_fname = filename;
-      Lexing.pos_lnum  = 1;
-      Lexing.pos_bol   = 0;
-      Lexing.pos_cnum  = 0
-    };
-  current := i;
-  lexbuf
+  let scan_references = Kernel.EagerLoadSources.get () in
+  match Parse_env.open_source ~scan_references fname with
+  | Error msg -> Kernel.fatal "%s" msg
+  | Ok in_str ->
+    let lexbuf = Lexing.from_string in_str in
+    let filename = Filepath.normalize fname in
+    let i = { lexbuf; current_working_directory = None } in
+    (* Initialize lexer buffer. *)
+    lexbuf.Lexing.lex_curr_p <-
+      { Lexing.pos_fname = filename;
+        Lexing.pos_lnum  = 1;
+        Lexing.pos_bol   = 0;
+        Lexing.pos_cnum  = 0
+      };
+    current := i;
+    lexbuf
 
 let finishParsing () =
   let i = !current in
   assert (i != dummyinfo);
-  close_in i.inchan;
   current := dummyinfo
 
 

src/kernel_internals/parsing/logic_preprocess.mll

@@ -531,18 +531,25 @@ parse
   let file suffix cpp filename =
     reset ();
     let debug = Kernel.is_debug_key_enabled Kernel.dkey_parser in
-    let inchan = open_in_bin filename in
-    let lex = Lexing.from_channel inchan in
-    let ppname =
-      Extlib.temp_file_cleanup_at_exit ~debug
-        (Filename.basename filename) ".pp"
-    in
-    let ppfile = open_out ppname in
-    main lex;
-    preprocess_annots suffix cpp ppfile;
-    close_in inchan;
-    close_out ppfile;
-    Datatype.Filepath.of_string ppname
+    let scan_references = Kernel.EagerLoadSources.get () in
+    match Parse_env.open_source ~scan_references filename with
+    | Error msg -> Kernel.abort "logic_preprocess: %s" msg
+    | Ok source ->
+      let lex = Lexing.from_string source in
+      let ppname =
+        Extlib.temp_file_cleanup_at_exit ~debug
+          (Filename.basename filename) ".pp"
+      in
+      let fp_of_string = Filepath.Normalized.of_string in
+      let workdir_opt = Parse_env.get_workdir (fp_of_string filename) in
+      Option.iter
+        (fun workdir -> Parse_env.set_workdir (fp_of_string ppname) workdir)
+        workdir_opt;
+      let ppfile = open_out ppname in
+      main lex;
+      preprocess_annots suffix cpp ppfile;
+      close_out ppfile;
+      Datatype.Filepath.of_string ppname
 }
 
 (*

src/kernel_internals/parsing/parse_env.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2021                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* maps filepaths to bools (true iff the file existed at the moment
+   the reference was read *)
+let referenced_files = Hashtbl.create 7
+
+module SourceFiles =
+  State_builder.Hashtbl(Datatype.Filepath.Hashtbl)(Datatype.String)
+    (struct
+      let name = "SourceFiles"
+      let dependencies = [ Kernel.Files.self ]
+      let size = 1
+    end)
+
+(* maps .i/.pp files to their workdir (when a JCDB is used) *)
+module PreprocessingWorkdir =
+  State_builder.Hashtbl(Datatype.Filepath.Hashtbl)(Datatype.String)
+    (struct
+      let name = "PreprocessingWorkdir"
+      let dependencies =
+        [ Kernel.Files.self; Kernel.JsonCompilationDatabase.self ]
+      let size = 2
+    end)
+
+let set_workdir file workdir =
+  PreprocessingWorkdir.replace file workdir
+
+let get_workdir file =
+  try
+    Some (PreprocessingWorkdir.find file)
+  with Not_found -> None
+
+let store_referenced_source fname =
+  let fp = Datatype.Filepath.of_string fname in
+  if not (Hashtbl.mem referenced_files fp) then begin
+    try
+      let inchan = open_in_bin (fp :> string) in
+      let contents = really_input_string inchan (in_channel_length inchan) in
+      close_in inchan;
+      SourceFiles.replace fp contents;
+      Hashtbl.add referenced_files fp true
+    with Sys_error s ->
+      Kernel.warning ~once:true ~wkey:Kernel.wkey_file_not_found
+        "Cannot find referenced file %S (%s), ignoring" fname s;
+      Hashtbl.add referenced_files fp false
+  end
+
+let scan_source_for_references ~workdir contents =
+  let re_hash =
+    Str.regexp "^#[ \\t]*\\(line\\)?[ \\t]*[0-9]+[ \\t]+\"\\([^<>]*\\)\"[ \\t]+[0-9]*[ \\t]*$"
+  in
+  let lines = String.split_on_char '\n' contents in
+  List.iter (fun line ->
+      if Str.string_match re_hash line 0 then
+        let file = Str.matched_group 2 line in
+        let file =
+          if String.contains file '"' then
+            (* Special case: the filename contains double quotes;
+               when this happens, the matched regex contains an extra backslash
+               that must be removed. In other words, we must undo the quoting
+               introduced by the C preprocessor. *)
+            Str.global_replace (Str.regexp "\\\\\"") "\"" file
+          else file
+        in
+        let file = if Filename.is_relative file && workdir <> None then
+            (Option.get workdir) ^ "/" ^ file
+          else file
+        in
+        store_referenced_source file
+    ) lines
+
+let open_source ~scan_references fname =
+  let fp = Datatype.Filepath.of_string fname in
+  try
+    let s = SourceFiles.find fp in
+    Ok s
+  with Not_found ->
+  try
+    Kernel.feedback ~dkey:Kernel.dkey_file_source
+      "opening source file: %S" fname;
+    let inchan = open_in_bin (fp :> string) in
+    let contents = really_input_string inchan (in_channel_length inchan) in
+    close_in inchan;
+    SourceFiles.replace fp contents;
+    let workdir =
+      try
+        Some (PreprocessingWorkdir.find fp)
+      with Not_found ->
+        None
+    in
+    if scan_references then
+      scan_source_for_references ~workdir contents;
+    Ok contents
+  with Sys_error s ->
+    Error s

src/kernel_internals/parsing/parse_env.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2021                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+val open_source : scan_references:bool -> string -> (string, string) result
+
+val set_workdir : Filepath.Normalized.t -> string -> unit
+
+val get_workdir : Filepath.Normalized.t -> string option

src/kernel_internals/typing/cabs2cil.ml

@@ -3399,9 +3399,13 @@ let rec setOneInit this o preinit =
           let l = Array.length !pArray in
           if l <= idx then begin
             let growBy = max (max 32 (idx + 1 - l)) (l / 2) in
-            let newarray = Array.make (growBy + idx) NoInitPre in
-            Array.blit !pArray 0 newarray 0 l;
-            pArray := newarray
+            try
+              let newarray = Array.make (growBy + idx) NoInitPre in
+              Array.blit !pArray 0 newarray 0 l;
+              pArray := newarray
+            with Invalid_argument _ | Out_of_memory ->
+              Kernel.abort ~current:true
+                "array length too large for Frama-C: %d" (idx)
           end
         end;
         pMaxIdx, pArray

src/kernel_services/ast_data/annotations.ml

@@ -365,14 +365,7 @@ let code_annot_emitter ?filter stmt =
   try
     let tbl = Code_annots.find stmt in
     let filter e l acc =
-      let e =
-        try Emitter.Usable_emitter.get e
-        with Not_found ->
-          (* in some cases, e.g. when loading a state with a different set
-             of plugins loaded, the original emitter might not be available,
-             leading to discarding annotations. Let the kernel adopt them. *)
-          Emitter.orphan
-      in
+      let e = Emitter.Usable_emitter.get e in
       match filter with
       | None -> List.map (fun a -> a, e) l @ acc
       | Some f ->

src/kernel_services/ast_queries/file.ml

@@ -35,13 +35,14 @@ let pretty_cpp_opt_kind fmt =
 
 type file =
   | NeedCPP of
-      Filepath.Normalized.t (* filename of the [.c] to preprocess *)
+      Filepath.Normalized.t (* Filename of the [.c] to preprocess. *)
       * string (* Preprocessing command, as given by -cpp-command, or
-                  the default value, but without extra arguments *)
-      * string list (* Extra arguments to be given to the preprocessing
-                       command, as given by -cpp-extra-args-per-file or
-                       a JSON Compilation Database. *)
-      * cpp_opt_kind
+                  the default value, but without extra arguments. *)
+      * string list (* Extra arguments (already included in the command)
+                       which must also be given to the logic preprocessor
+                       (since Frama-C may preprocess twice each source). *)
+      * cpp_opt_kind (* Whether the preprocessor is known to be compatible with
+                        GCC-style options (mostly, -D and -I). *)
   | NoCPP of Filepath.Normalized.t (** filename of a preprocessed [.c] *)
   | External of Filepath.Normalized.t * string
   (* file * name of plug-in that handles it *)
@@ -460,10 +461,9 @@ let adjust_pwd fp cpp_command =
       | None -> cwd
       | Some d -> (d:>string)
     in
-    if cwd <> dir then
-      "cd " ^ dir ^ " && " ^ cpp_command
-    else cpp_command
-  else cpp_command
+    if cwd <> dir then Some dir, "cd " ^ dir ^ " && " ^ cpp_command
+    else None, cpp_command
+  else None, cpp_command
 
 let build_cpp_cmd = function
   | NoCPP _ | External _ -> None
@@ -543,7 +543,9 @@ let build_cpp_cmd = function
         include_args define_args
     in
     let cpp_command = replace_in_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) in
-    let cpp_command_with_chdir = adjust_pwd f cpp_command in
+    let workdir, cpp_command_with_chdir = adjust_pwd f cpp_command in
+    if workdir <> None then
+      Parse_env.set_workdir ppf (Option.get workdir);
     Kernel.feedback ~dkey:Kernel.dkey_pp
       "preprocessing with \"%s\""
       cpp_command_with_chdir;

src/kernel_services/ast_queries/file.mli

@@ -32,7 +32,7 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown
 type file =
   | NeedCPP of Filepath.Normalized.t * string * string list * cpp_opt_kind
   (** File which needs preprocessing.
-      NeedCPP(filepath, cmd, extra, cpp_opt_kind):
+      NeedCPP(filepath, cmd, extra, workdir, cpp_opt_kind):
       - filepath: source file to be preprocessed;
       - cmd: preprocessing command, before replacement of '%'-arguments;
       - extra: list of extra arguments (e.g. from a JCDB);

src/kernel_services/plugin_entry_points/db.mli

@@ -37,7 +37,7 @@
    - {!File}: Cil file initialization
    - {!Globals}: global variables, functions and annotations
    - {!Annotations}: annotations associated with a statement
-   - {!Properties_status}: status of annotations
+   - {!Property_status}: status of annotations
    - {!Kernel_function}: C functions as seen by Frama-C
    - {!Stmts_graph}: the statement graph
    - {!Loop}: (natural) loops

src/kernel_services/plugin_entry_points/emitter.ml

@@ -23,10 +23,6 @@
 (* Modules [Hashtbl] and [Kernel] are not usable here. Thus use above modules
    instead. *)
 
-(**************************************************************************)
-(** {2 Datatype} *)
-(**************************************************************************)
-
 type kind = Property_status | Alarm | Code_annot | Funspec | Global_annot
 
 type emitter =
@@ -35,6 +31,59 @@ type emitter =
     tuning_parameters: Typed_parameter.t list;
     correctness_parameters: Typed_parameter.t list }
 
+(**************************************************************************)
+(** {2 Implementation for Plug-in Developers} *)
+(**************************************************************************)
+
+let names: unit Datatype.String.Hashtbl.t = Datatype.String.Hashtbl.create 7
+
+let create name kinds ~correctness ~tuning =
+  if Datatype.String.Hashtbl.mem names name then
+    Kernel.fatal "emitter %s already exists with the same parameters" name;
+  let e =
+    { name = name;
+      kinds = kinds;
+      correctness_parameters = correctness;
+      tuning_parameters = tuning }
+  in
+  Datatype.String.Hashtbl.add names name ();
+  e
+
+let dummy = create "dummy" [] ~correctness:[] ~tuning:[]
+
+let get_name e = e.name
+
+let correctness_parameters e =
+  List.map (fun p -> p.Typed_parameter.name) e.correctness_parameters
+
+let tuning_parameters e =
+  List.map (fun p -> p.Typed_parameter.name) e.tuning_parameters
+
+let end_user =
+  create
+    "End-User"
+    [ Property_status; Code_annot; Funspec; Global_annot ]
+    ~correctness:[]
+    ~tuning:[]
+
+let kernel =
+  create
+    "Frama-C kernel"
+    [ Property_status; Funspec ]
+    ~correctness:[]
+    ~tuning:[]
+
+let orphan =
+  create
+    "Orphan"
+    [ Code_annot; Funspec; Global_annot ]
+    ~correctness:[]
+    ~tuning:[]
+
+(**************************************************************************)
+(** {2 Datatype} *)
+(**************************************************************************)
+
 module D =
   Datatype.Make_with_collections
     (struct
@@ -106,7 +155,7 @@ module Usable_emitter = struct
         let mem_project = Datatype.never_any_project
       end)
 
-  let get e =
+  let unsafe_get e =
     let get_params map =
       Datatype.String.Map.fold
         (fun s _ acc -> Typed_parameter.get s :: acc)
@@ -118,6 +167,13 @@ module Usable_emitter = struct
       correctness_parameters = get_params e.correctness_values;
       tuning_parameters = get_params e.tuning_values }
 
+  (* In some cases, e.g. when loading a state with a different set
+     of plugins loaded, the original emitter might not be available,
+     leading to discarding annotations. Let the kernel adopt them. *)
+  let get e =
+    try unsafe_get e
+    with Not_found -> orphan
+
   let get_name e = e.u_name
   let get_unique_name e = Format.asprintf "%a" pretty e
 
@@ -134,55 +190,6 @@ module Usable_emitter = struct
 
 end
 
-(**************************************************************************)
-(** {2 Implementation for Plug-in Developers} *)
-(**************************************************************************)
-
-let names: unit Datatype.String.Hashtbl.t = Datatype.String.Hashtbl.create 7
-
-let create name kinds ~correctness ~tuning =
-  if Datatype.String.Hashtbl.mem names name then
-    Kernel.fatal "emitter %s already exists with the same parameters" name;
-  let e =
-    { name = name;
-      kinds = kinds;
-      correctness_parameters = correctness;
-      tuning_parameters = tuning }
-  in
-  Datatype.String.Hashtbl.add names name ();
-  e
-
-let dummy = create "dummy" [] ~correctness:[] ~tuning:[]
-
-let get_name e = e.name
-
-let correctness_parameters e =
-  List.map (fun p -> p.Typed_parameter.name) e.correctness_parameters
-
-let tuning_parameters e =
-  List.map (fun p -> p.Typed_parameter.name) e.tuning_parameters
-
-let end_user =
-  create
-    "End-User"
-    [ Property_status; Code_annot; Funspec; Global_annot ]
-    ~correctness:[]
-    ~tuning:[]
-
-let kernel =
-  create
-    "Frama-C kernel"
-    [ Property_status; Funspec ]
-    ~correctness:[]
-    ~tuning:[]
-
-let orphan =
-  create
-    "Orphan"
-    [ Code_annot; Funspec; Global_annot ]
-    ~correctness:[]
-    ~tuning:[]
-
 (**************************************************************************)
 (** {2 State of all known emitters} *)
 (**************************************************************************)

src/kernel_services/plugin_entry_points/kernel.ml

@@ -69,6 +69,8 @@ let dkey_file_print_one = register_category "file:print-one"
 
 let dkey_file_transform = register_category "file:transformation"
 
+let dkey_file_source = register_category "file:source"
+
 let dkey_filter = register_category "filter"
 
 let dkey_globals = register_category "globals"
@@ -205,6 +207,9 @@ let wkey_asm = register_warn_category "asm:clobber"
 
 let wkey_unnamed_typedef = register_warn_category "parser:unnamed-typedef"
 
+let wkey_file_not_found = register_warn_category "file:not-found"
+let () = set_warn_status wkey_file_not_found Log.Wfeedback
+
 (* ************************************************************************* *)
 (** {2 Specialised functors for building kernel parameters} *)
 (* ************************************************************************* *)
@@ -802,6 +807,15 @@ module BigIntsHex =
     let default = -1
   end)
 
+let () = Parameter_customize.set_group inout_source
+module EagerLoadSources =
+  False(struct
+    let module_name = "EagerLoadSources"
+    let option_name = "-eager-load-sources"
+    let help = "when loading a source, try to load all referenced sources \
+                in memory"
+  end)
+
 (* ************************************************************************* *)
 (** {2 Save/Load} *)
 (* ************************************************************************* *)

src/kernel_services/plugin_entry_points/kernel.mli

@@ -67,6 +67,9 @@ val dkey_file_print_one: category
 
 val dkey_file_annot: category
 
+val dkey_file_source: category
+(** Messages related to operations on files during preprocessing/parsing. *)
+
 val dkey_filter: category
 
 val dkey_globals: category
@@ -201,6 +204,9 @@ val wkey_unnamed_typedef: warn_category
 (** Warning related to "unnamed typedef that does not introduce a struct
     or enumeration type". *)
 
+val wkey_file_not_found: warn_category
+(** Warnings related to missing files during preprocessing/parsing. *)
+
 (* ************************************************************************* *)
 (** {2 Functors for late option registration}                                *)
 (** Kernel_function-related options cannot be registered in this module:
@@ -343,6 +349,9 @@ module FloatHex: Parameter_sig.Bool
 module BigIntsHex: Parameter_sig.Int
 (** Behavior of option "-hexadecimal-big-integers" *)
 
+module EagerLoadSources: Parameter_sig.Bool
+(** Behavior of option "-eager-load-sources" *)
+
 (* ************************************************************************* *)
 (** {2 Save/Load} *)
 (* ************************************************************************* *)

src/plugins/e-acsl/Makefile.in

@@ -56,7 +56,13 @@ SRC_PROJECT_INITIALIZER:=\
   $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
 
 # analyses
+ANALYSES_CMI:= \
+	analyses_types
+ANALYSES_CMI:=$(addprefix src/analyses/, $(ANALYSES_CMI))
+
 SRC_ANALYSES:= \
+	analyses_datatype \
+	label \
 	rte \
 	lscope \
 	e_acsl_visitor \
@@ -66,7 +72,8 @@ SRC_ANALYSES:= \
 	typing \
 	literal_strings \
 	memory_tracking \
-	exit_points
+	exit_points \
+	analyses
 SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
 
 # code generator
@@ -79,7 +86,6 @@ SRC_CODE_GENERATOR:= \
 	smart_exp \
 	smart_stmt \
 	gmp \
-	label \
 	env \
 	assert \
 	rational \
@@ -128,6 +134,7 @@ PLUGIN_CMO:= src/local_config \
 	src/main
 PLUGIN_CMI:= \
 	$(LIBRARIES_CMI) \
+	$(ANALYSES_CMI) \
 	$(CODE_GENERATOR_CMI)
 PLUGIN_HAS_MLI:=yes
 PLUGIN_DISTRIBUTED:=yes
@@ -162,7 +169,7 @@ VERSION_FILE=$(FRAMAC_ROOT_SRCDIR)/VERSION
 
 EACSL_VERSION:=$(shell sed -e 's/\\(.*\\)/\\1/' $(VERSION_FILE))
 
-$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_FILE)
+$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile $(VERSION_FILE)
 	$(PRINT_MAKING) $@
 	$(RM) $@
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
@@ -180,6 +187,7 @@ ifeq (@MAY_RUN_TESTS@,yes)
 PLUGIN_TESTS_DIRS := \
 	examples \
 	bts \
+	concurrency \
 	constructs \
 	arith \
 	memory \
@@ -217,11 +225,13 @@ TEST_DEPENDENCIES += \
 	$(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmxs
 endif
 
+ifneq ("$(PLUGIN_ENABLE)","no")
 # Add the test dependencies to the test targets, but also to
 # `plugins_ptests_config` so that they are built along with the main target.
 plugins_ptests_config: $(TEST_DEPENDENCIES)
 E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
 tests:: $(TEST_DEPENDENCIES)
+endif
 
 $(EACSL_PLUGIN_DIR)/tests/test_config: \
 		$(EACSL_PLUGIN_DIR)/tests/test_config.in \
@@ -272,9 +282,11 @@ EACSL_DLMALLOC_FLAGS = \
   -DMSPACES=1 \
   -DONLY_MSPACES \
   -DMALLOC_ALIGNMENT=32 \
-  -DMSPACE_PREFIX="__e_acsl_"
+  -DMSPACE_PREFIX="__e_acsl_" \
+  -DUSE_LOCKS=1 \
+  -DUSE_SPIN_LOCKS=1
 
-$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC)
+$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC) $(EACSL_PLUGIN_DIR)/Makefile
 	$(MKDIR) $(EACSL_LIBDIR)
 	echo 'CC           $<'
 	$(CC) $< -c -O2 -g3 -o$(EACSL_DLMALLOC_OBJ) $(EACSL_DLMALLOC_FLAGS)
@@ -283,10 +295,12 @@ $(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC)
 	echo 'RANLIB       $@'
 	ranlib $@
 
+ifneq ("$(PLUGIN_ENABLE)","no")
 all:: $(EACSL_DLMALLOC_LIB)
 
 clean::
 	$(RM) $(EACSL_DLMALLOC_LIB)
+endif
 
 ############
 # Cleaning #
@@ -352,7 +366,9 @@ EACSL_TEST_FILES = \
 	tests/temporal/test_config_dev \
 	tests/format/test_config \
 	tests/format/test_config_dev \
-	tests/E_ACSL_test.ml \
+	tests/concurrency/test_config \
+	tests/concurrency/test_config_dev \
+	tests/E_ACSL_test.ml
 
 EACSL_TESTS_C_FILES = \
   $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \

src/plugins/e-acsl/doc/Changelog

@@ -25,6 +25,7 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-  E-ACSL       [2022-01-28] Add Linux's pthread concurrency support.
 -* E-ACSL       [2021-12-03] Fix crash when creating an axiomatic with an
                 existing name in E-ACSL's RTL (frama-c/e-acsl#161).
 -* E-ACSL       [2021-12-01] Fix crash when binding a lambda-abstraction to a
@@ -34,10 +35,10 @@ Plugin E-ACSL <next-release>
 -* E-ACSL       [2021-11-23] Add support for VDSO segment on Linux.
 -* e-acsl-gcc   [2021-11-22] Fix e-acsl-gcc.sh detection of failures in
                 subcommands.
--  E-ACSL       [2021-11-03] Improve runtime debug logs: the %a modifier now
+-  runtime      [2021-11-03] Improve runtime debug logs: the %a modifier now
                 outputs in hexadecimal, the debug logs now all end in new lines,
                 the trace now outputs to stderr.
--* E-ACSL       [2021-11-03] Fix default stack size: E_ACSL_STACK_SIZE
+-* runtime      [2021-11-03] Fix default stack size: E_ACSL_STACK_SIZE
                 is now correctly used by the runtime, the default values
                 have been adjusted to what was effectively used.
 -* E-ACSL       [2021-11-03] Now the same Frama-C options are used when parsing

src/plugins/e-acsl/doc/userman/changes.tex

@@ -6,6 +6,12 @@ release. First we list changes of the last release.
 % Next version
 %\section*{E-ACSL \eacslpluginversion \eacslplugincodename}
 
+\section*{E-ACSL \eacslpluginversion \eacslplugincodename}
+
+\begin{itemize}
+\item New section \textbf{Concurrency Support}.
+\end{itemize}
+
 \section*{E-ACSL 24.0 Chromium}
 
 \begin{itemize}