file.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil
open Visitor

type cpp_opt_kind = Gnu | Not_gnu | Unknown

type file =
  | NeedCPP of
      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, specific to this file (that is,
                       obtained via a JCDB, or -cpp-extra-args-per-file,
                       but _not_ those via -cpp-extra-args), to be given
                       to the C preprocessor. *)
      * 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 *)

module D =
  Datatype.Make
    (struct
      include Datatype.Serializable_undefined
      type t = file
      let name = "File"
      let reprs =
        [ NeedCPP(Filepath.Normalized.empty, "", [], Unknown);
          NoCPP Filepath.Normalized.empty;
          External(Filepath.Normalized.empty, "")
        ]
      let structural_descr = Structural_descr.t_abstract
      let mem_project = Datatype.never_any_project
      let copy = Datatype.identity (* immutable strings *)
    end)
include D

let check_suffixes = Hashtbl.create 17
let new_file_type = Hashtbl.add check_suffixes
let get_suffixes () =
  Hashtbl.fold
    (fun s _ acc -> s :: acc)
    check_suffixes
    [ ".c"; ".i"; ".h" ]

let get_filepath = function NeedCPP (s, _, _, _) | NoCPP s | External (s, _) -> s
let get_name s = Filepath.Normalized.to_pretty_string (get_filepath s)

(* ************************************************************************* *)
(** {2 Preprocessor command} *)
(* ************************************************************************* *)

(* Do not trust custom command-line to be gnu like by default, but give
   them a chance, with a warning indicating that things may go wrong. *)
let cpp_opt_kind () =
  if Kernel.CppGnuLike.is_set () then
    if Kernel.CppGnuLike.get () then Gnu else Not_gnu
  else Unknown

let is_cpp_gnu_like () =
  let open System_config.Preprocessor in
  let cpp_cmd = Kernel.CppCommand.get () in
  match cpp_cmd = "", is_default, is_gnu_like with
  | true, true, true -> Gnu
  | true, true, false -> Not_gnu
  | _, _, _ -> cpp_opt_kind ()

(* the preprocessor command is:
   If the program has an explicit argument -cpp-command "XX -Y"
   (quotes are required by the shell)
   then XX -Y
   else use the command in [System_config.Preprocessor.command].*)
let get_preprocessor_command () =
  let cmdline = Kernel.CppCommand.get() in
  if cmdline <> "" then cmdline else System_config.Preprocessor.command

let from_filename ?cpp f =
  let cpp =
    let cpp_command = Kernel.CppCommand.get() in
    if cpp_command <> "" then cpp_command
    else if cpp = None then get_preprocessor_command ()
    else Option.get cpp
  in
  let extra_for_this_file =
    let extra_by_file =
      try Kernel.CppExtraArgsPerFile.find f
      with Not_found -> ""
    in
    let jcdb_flags = Json_compilation_database.get_flags f in
    if extra_by_file <> "" && jcdb_flags <> [] then
      Kernel.warning ~wkey:Kernel.wkey_jcdb
        "found flags for file %a@ both in -cpp-extra-args-per-file and@ \
         in the json compilation database;@ the latter will be ignored"
        Filepath.Normalized.pretty f;
    if extra_by_file <> "" then [extra_by_file] else jcdb_flags
  in
  if Filename.check_suffix (f:>string) ".i" then begin
    NoCPP f
  end else
    let suf =
      try
        let suf_idx = String.rindex (f:>string) '.' in
        String.sub (f:>string) suf_idx (String.length (f:>string) - suf_idx)
      with Not_found -> (* raised by String.rindex if '.' \notin f *)
        ""
    in
    if Hashtbl.mem check_suffixes suf then
      External (f, suf)
    else if cpp <> "" then begin
      if not System_config.Preprocessor.keep_comments then
        Kernel.warning ~once:true
          "Default preprocessor does not keep comments. Any ACSL annotations \
           on non-preprocessed files will be discarded.";
      NeedCPP (f, cpp, extra_for_this_file, is_cpp_gnu_like ())
    end else
      Kernel.abort "No working preprocessor found. You can only analyze \
                    preprocessed .i files."

(* ************************************************************************* *)
(** {2 Internal states} *)
(* ************************************************************************* *)

module Files : sig
  val get: unit -> t list
  val register: t list -> unit
  val pre_register: t -> unit
  val is_computed: unit -> bool
  val reset: unit -> unit
  val pre_register_state: State.t
end = struct

  module S =
    State_builder.List_ref
      (D)
      (struct
        let dependencies =
          [ Kernel.CppCommand.self;
            Kernel.CppExtraArgs.self;
            Kernel.CppExtraArgsPerFile.self;
            Kernel.JsonCompilationDatabase.self;
            Kernel.Files.self ]
        let name = "Files for preprocessing"
      end)

  module Pre_files =
    State_builder.List_ref
      (D)
      (struct
        let dependencies = []
        let name = "Built-ins headers and source"
      end)

  let () =
    State_dependency_graph.add_dependencies
      ~from:S.self
      [ Ast.self; Ast.UntypedFiles.self; Cabshelper.Comments.self ]

  let () =
    State_dependency_graph.add_dependencies
      ~from:Pre_files.self
      [ Ast.self;
        Ast.UntypedFiles.self;
        Cabshelper.Comments.self;
        Cil_builtins.Frama_c_builtins.self ]

  let () =
    Ast.add_linked_state Cabshelper.Comments.self

  let pre_register_state = Pre_files.self

  (* Allow to register files in advance, e.g. prolog files for plugins *)
  let pre_register file =
    let prev_files = Pre_files.get () in Pre_files.set (prev_files @ [file])

  let register files =
    if S.is_computed () then
      raise (Ast.Bad_Initialization "[File.register] Too many initializations");
    let prev_files = S.get () in
    S.set (prev_files @ files);
    S.mark_as_computed ()

  let get () = Pre_files.get () @ S.get ()
  let is_computed () = S.is_computed ()

  let reset () =
    let selection = State_selection.with_dependencies S.self in
    (* Keep built-in files set *)
    Project.clear ~selection ()
end

let get_all = Files.get
let pre_register = Files.pre_register


(* ************************************************************************* *)
(** {2 Machdep} *)
(* ************************************************************************* *)

(* not exported, see [pretty_machdep] below. *)
let print_machdep fmt (m : Machdep.mach) =
  begin
    Format.fprintf fmt "Machine: %s@\n" m.version ;
    let pp_size_error fmt v =
      if v < 0
      then Format.pp_print_string fmt "error"
      else Format.fprintf fmt "%2d" v
    in
    let pp_size_bits fmt v =
      if v >= 0 then Format.fprintf fmt "%d bits, " (v*8)
    in
    let pp_align_error fmt v =
      if v < 0
      then Format.pp_print_string fmt "alignof error"
      else Format.fprintf fmt "aligned on %d bits" (v*8)
    in
    List.iter
      (fun (name,size,align) ->
         Format.fprintf fmt
           "   sizeof %11s = %a (%a%a)@\n"
           name pp_size_error size pp_size_bits size pp_align_error align)
      [
        "short",  m.sizeof_short, m.alignof_short ;
        "int",    m.sizeof_int,   m.alignof_int ;
        "long",   m.sizeof_long,  m.alignof_long ;
        "long long", m.sizeof_longlong,  m.alignof_longlong ;
        "float",  m.sizeof_float,  m.alignof_float ;
        "double", m.sizeof_double, m.alignof_double ;
        "long double", m.sizeof_longdouble, m.alignof_longdouble ;
        "pointer", m.sizeof_ptr, m.alignof_ptr ;
        "void", m.sizeof_void, m.sizeof_void ;
        "function", m.sizeof_fun, m.alignof_fun ;
      ] ;
    List.iter
      (fun (name,typeof) ->
         Format.fprintf fmt "   typeof %11s = %s@\n" name typeof)
      [
        "sizeof(T)", m.size_t ;
        "wchar_t", m.wchar_t ;
        "ptrdiff_t", m.ptrdiff_t ;
      ] ;
    Format.fprintf fmt "   char is %s@\n"
      (if m.char_is_unsigned then "unsigned" else "signed");
    Format.fprintf fmt "   machine is %s endian@\n"
      (if m.little_endian then "little" else "big") ;
    Format.fprintf fmt "   compiler %s builtin __va_list@\n"
      (if m.has__builtin_va_list then "has" else "has not") ;
  end

let machdep_dir () = Kernel.Share.get_dir "machdeps"

let regexp_machdep = Str.regexp "^machdep_\\([^.]*\\).yaml$"

let default_machdep_file machdep =
  let filename = "machdep_" ^ machdep ^ ".yaml" in
  Filepath.Normalized.concat (machdep_dir()) filename

let is_default_machdep machdep =
  Filepath.Normalized.is_file (default_machdep_file machdep)

let mem_machdep s = is_default_machdep s || Sys.file_exists s

let default_machdeps () =
  Array.fold_right
    (fun s acc ->
       if Str.string_match regexp_machdep s 0 then
         Str.matched_group 1 s :: acc
       else acc)
    (Sys.readdir (machdep_dir() :> string))
    []

let pretty_machdeps fmt =
  List.iter (fun s -> Format.fprintf fmt "@ %s" s) (default_machdeps())

let machdep_help () =
  let m = Kernel.Machdep.get () in
  if m = "help" then begin
    Kernel.feedback
      "@[supported machines are%t@ (default is x86_64).@]"
      pretty_machdeps;
    raise Cmdline.Exit
  end else
    Cmdline.nop

let () = Cmdline.run_after_exiting_stage machdep_help

let set_machdep () =
  let m = Kernel.Machdep.get () in
  if not (mem_machdep m) then
    Kernel.abort "@[unsupported machine '%s'.@ Either use a predefined name among %t,@ or an YAML machdep file.@]" m pretty_machdeps

let () = Cmdline.run_after_configuring_stage set_machdep

(* Local to this module. Use Machine module instead. *)
let get_machdep () =
  let m = Kernel.Machdep.get () in
  let file =
    if is_default_machdep m then default_machdep_file m
    else Filepath.Normalized.of_string ~existence:Must_exist m
  in
  let res =
    Result.bind
      (Yaml_unix.of_file (Fpath.v (file:>string)))
      Machdep.mach_of_yaml
  in
  match res with
  | Ok machdep -> machdep
  | Error (`Msg s) ->
    Kernel.abort "Error during machdep parsing: %s" s

(* Macros that are defined by gcc even in presence of -undef.
   Specifically use -U on the command line to silence them.
*)
let unsupported_libc_macros =
  [
    "__STDC_IEC_559_COMPLEX__";
    "__STDC_IEC_60559_COMPLEX__";
    "__STDC_ISO_10646__";
    "__STDC_UTF16__";
    "__STDC_UTF32__";
  ]

let unsupported_float_type_macros acc name =
  List.fold_left
    (fun acc s -> Datatype.String.Set.add ("__" ^ name ^ "_" ^ s ^ "__") acc)
    acc
    [ "DECIMAL_DIG"; "DENORM_MIN"; "DIG"; "HAS_DENORM"; "HAS_INFINITY";
      "HAS_QUIET_NAN"; "IS_IEC_60559"; "MANT_DIG";
      "MAX"; "MAX_10_EXP"; "MAX_EXP";
      "MIN"; "MIN_10_EXP"; "MIN_EXP";
      "NORM_MAX"; "EPSILON";
    ]

let unsupported_float_types =
  List.fold_left unsupported_float_type_macros
    Datatype.String.Set.empty
    [ "BFLT16"; "FLT16"; "FLT128"; "LDBL"; ]

let known_bad_macros =
  Datatype.String.Set.add_seq
    (List.to_seq
       (["__GCC_IEC_559_COMPLEX"; "__SIZEOF_INT128__"; "__SSE__"; "__SSE2__" ]
        @ unsupported_libc_macros))
    unsupported_float_types

let print_machdep_header () =
  if Kernel.PrintMachdepHeader.get () then begin
    let censored_macros = known_bad_macros in
    Machdep.gen_all_defines
      Format.std_formatter ~censored_macros (get_machdep());
    raise Cmdline.Exit
  end else Cmdline.nop

let () = Cmdline.run_after_exiting_stage print_machdep_header

let list_available_machdeps = default_machdeps

let pretty_machdep ?fmt ?machdep () =
  let machine = match machdep with None -> get_machdep () | Some m -> m in
  match fmt with
  | None -> Log.print_on_output (fun fmt -> print_machdep fmt machine)
  | Some fmt -> print_machdep fmt machine

(* ************************************************************************* *)
(** {2 Initializations} *)
(* ************************************************************************* *)

let create_temp_file name suffix =
  let debug = Kernel.is_debug_key_enabled Kernel.dkey_pp_keep_temp_files in
  let of_string = Filepath.Normalized.of_string in
  try of_string (Extlib.temp_file_cleanup_at_exit ~debug name suffix)
  with Extlib.Temp_file_error s ->
    Kernel.abort "cannot create temporary file: %s" s

let safe_remove_file (f : Datatype.Filepath.t) =
  if not (Kernel.is_debug_key_enabled Kernel.dkey_pp_keep_temp_files) then
    Extlib.safe_remove (f :> string)

let cpp_name cmd =
  let cmd = List.hd (String.split_on_char ' ' cmd) in
  Filename.basename cmd

let replace_in_cpp_cmd cmdl supp_args in_file out_file =
  (* using Filename.quote for filenames which contain space or shell
     metacharacters *)
  let in_file = Filename.quote in_file
  and out_file = Filename.quote out_file in
  let substitute s =
    match Str.matched_string s with
    | "%%" -> "%"
    | "%args" -> supp_args
    | "%1" | "%i" | "%input" -> in_file
    | "%2" | "%o" | "%output" -> out_file
    | s -> s (* Unrecognized parameters are left intact *)
  in
  let regexp = Str.regexp "%%\\|%[a-z0-9]+" in
  try
    ignore (Str.search_forward regexp cmdl 0); (* Try to find one match *)
    Str.global_substitute regexp substitute cmdl
  with Not_found ->
    Format.sprintf "%s %s %s -o %s" cmdl supp_args in_file out_file

(* Note: using Pretty_utils.pp_list without forcing '~pre' and '~suf' to
   be empty strings can lead to issues when the commands are too long and
   Format's pretty-printer decides to insert newlines.
   This concatenation function serves as a reminder to avoid using them.
*)
let concat_strs ?(pre="") ?(sep=" ") l =
  if l = [] then ""
  else pre ^ (String.concat sep l)

let adjust_pwd fp cpp_command =
  if Kernel.JsonCompilationDatabase.is_set () then
    let cwd = Filepath.pwd () in
    let dir =
      match Json_compilation_database.get_dir fp with
      | None -> cwd
      | Some d -> d
    in
    if cwd <> dir then Some dir, "cd " ^ (dir :> string) ^ " && " ^ cpp_command
    else None, cpp_command
  else None, cpp_command

(* Prevent gcc/clang from emitting warnings during preprocessing,
   related to builtin macro definitions from machdeps.
   Returns a (possibly empty) list of flags to be added to the command line. *)
let silence_cpp_machdep_warnings cmdl =
  let exe = cpp_name cmdl in
  if exe = "clang" || exe = "gcc" then
    (* NB: For gcc, only old versions (still found in Ubuntu 18.04,
       supported until 2028, though) activate builtin-macro-redefined.
       This is also the case for newer clangs, while older ones will
       complain about the unknown warning (gcc does not seem to care,
       so that it is safe to keep the unknown-warning-option in every
       case). *)
    ["-Wno-builtin-macro-redefined"; "-Wno-unknown-warning-option"]
  else
    []

let censored_macros cpp_args =
  List.fold_left
    (fun acc arg ->
       let open Option.Operators in
       let none = acc in
       let some = Fun.flip Datatype.String.Set.add acc in
       (let+ name = Extlib.string_del_prefix "-U" arg in
        Extlib.strip_underscore name)
       |> Option.fold ~none ~some)
    known_bad_macros
    (List.(flatten (map (String.split_on_char ' ') cpp_args)))

let build_cpp_cmd = function
  | NoCPP _ | External _ -> None
  | NeedCPP (f, cmdl, extra_for_this_file, is_gnu_like) ->
    let extra_args = extra_for_this_file @ Kernel.CppExtraArgs.get () in
    if not (Filepath.exists f) then
      Kernel.abort "source file %a does not exist"
        Filepath.Normalized.pretty f;
    let add_if_gnu opt =
      match is_gnu_like with
      | Gnu -> [opt]
      | Not_gnu -> []
      | Unknown ->
        Kernel.warning
          ~once:true
          "your preprocessor is not known to handle option `%s'. \
           If preprocessing fails because of it, please add \
           -no-cpp-frama-c-compliant option to Frama-C's command-line. \
           If you do not want to see this warning again, explicitly use \
           option -cpp-frama-c-compliant."
          opt;
        [opt]
    in
    let ppf = create_temp_file (Filename.basename (f :> string)) ".i" in
    (* Hypothesis: the preprocessor is POSIX compliant,
       hence understands -I and -D. *)
    let fc_include_args =
      if Kernel.FramaCStdLib.get () then
        begin
          let censored_macros = censored_macros extra_args in
          let machdep_dir =
            Machdep.generate_machdep_header ~censored_macros (get_machdep())
          in
          [(machdep_dir:>string); (System_config.Share.libc:>string)]
        end
      else []
    in
    let fc_define_args = ["__FRAMAC__"] in
    let machdep_no_warn = silence_cpp_machdep_warnings cmdl in
    let clang_no_warn =
      (* Clang complains when -nostdlibinc is not used ... *)
      if cpp_name cmdl = "clang"
      then [ "-Wno-unused-command-line-argument" ]
      else []
    in
    let nostdinc_arg =
      if Kernel.FramaCStdLib.get() then add_if_gnu "-nostdinc"
      else []
    in
    let no_builtin_macros =
      if Kernel.FramaCStdLib.get () then add_if_gnu "-undef"
      else []
    in
    let output_defines_arg =
      let open Kernel in
      match ReadAnnot.get (), PreprocessAnnot.is_set (), PreprocessAnnot.get () with
      | true, true, true -> ["-dD"] (* keep '#defines' in preprocessed output *)
      | true, true, false -> []
      | true, false, _ -> add_if_gnu "-dD"
      | _, _, _ -> []
    in
    let gnu_implicit_args =
      output_defines_arg @ nostdinc_arg @ no_builtin_macros
    in
    let string_of_supp_args extra includes undef defines =
      Format.asprintf "%s%s%s%s"
        (concat_strs ~pre:"-I" ~sep:" -I" includes)
        (concat_strs ~pre:" -U" ~sep:" -U" undef)
        (concat_strs ~pre:" -D" ~sep:" -D" defines)
        (concat_strs ~pre:" " ~sep:" " extra)
    in
    let supp_args =
      string_of_supp_args
        (gnu_implicit_args @ machdep_no_warn @ clang_no_warn @ extra_args)
        fc_include_args
        unsupported_libc_macros
        fc_define_args
    in
    let cpp_command =
      replace_in_cpp_cmd cmdl supp_args (f:>string) (ppf:>string)
    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) :> string);
    Kernel.feedback ~dkey:Kernel.dkey_pp
      "preprocessing with \"%s\""
      cpp_command_with_chdir;
    Some (cpp_command_with_chdir, ppf)

let abort_with_detailed_pp_message f cpp_command =
  let possible_cause =
    if Kernel.JsonCompilationDatabase.is_set () then
      if not (Json_compilation_database.has_entry f) then
        Format.asprintf "note: %s is set but \
                         contains no entries for '%a'.@ "
          Kernel.JsonCompilationDatabase.option_name
          Datatype.Filepath.pretty f
      else ""
    else
    if not (Kernel.CppExtraArgs.is_set ()) &&
       not (Kernel.CppExtraArgsPerFile.is_set ()) &&
       not (Kernel.CppCommand.is_set ()) then
      Format.asprintf
        "this is possibly due to missing preprocessor flags;@ \
         consider options %s, %s or %s.@ "
        Kernel.CppExtraArgs.option_name
        Kernel.JsonCompilationDatabase.option_name
        Kernel.CppCommand.option_name
    else ""
  in
  Kernel.abort
    "failed to run: %s\n(PWD: %a)@\n\
     %sSee chapter \"Preparing the Sources\" in the Frama-C user manual \
     for more details."
    cpp_command Filepath.Normalized.pretty (Filepath.pwd ()) possible_cause

let parse_cabs cpp_command = function
  | NoCPP f ->
    if not (Filepath.exists f) then
      Kernel.abort "preprocessed file %a does not exist"
        Filepath.Normalized.pretty f;
    Kernel.feedback "Parsing %a (no preprocessing)"
      Datatype.Filepath.pretty f;
    Frontc.parse f ()
  | NeedCPP (f, cmdl, _extra_for_this_file, is_gnu_like) ->
    let cpp_command, ppf = Option.get cpp_command in
    Kernel.feedback "Parsing %a (with preprocessing)"
      Datatype.Filepath.pretty f;
    if Sys.command cpp_command <> 0 then begin
      safe_remove_file ppf;
      abort_with_detailed_pp_message f cpp_command
    end else
      Kernel.debug ~dkey:Kernel.dkey_pp
        "Full preprocessing command: %s" cpp_command;
    let ppf =
      if Kernel.ReadAnnot.get() &&
         ((Kernel.PreprocessAnnot.is_set () &&
           Kernel.PreprocessAnnot.get())
          || (match is_gnu_like with
              | Gnu -> true
              | Not_gnu -> false
              | Unknown ->
                Kernel.warning
                  ~once:true
                  "trying to preprocess annotation with an unknown \
                   preprocessor."; true))
      then begin
        let clang_no_warn = silence_cpp_machdep_warnings cmdl in
        let cmdl =
          List.fold_left (fun acc s -> acc ^ " " ^ s) cmdl clang_no_warn
        in
        let ppf' =
          try Logic_preprocess.file ".c"
                (replace_in_cpp_cmd cmdl "")
                (ppf : Filepath.Normalized.t :> string)
          with Sys_error _ as e ->
            safe_remove_file ppf;
            Kernel.abort "preprocessing of annotations failed (%s)"
              (Printexc.to_string e)
        in
        safe_remove_file ppf ;
        ppf'
      end else ppf
    in
    let (cil,(_,defs)) = Frontc.parse ppf () in
    cil.fileName <- f;
    safe_remove_file ppf;
    (cil,(f,defs))
  | External (f,suf) ->
    if not (Filepath.exists f) then
      Kernel.abort "file %a does not exist."
        Filepath.Normalized.pretty f;
    Kernel.feedback "Parsing %a (external front-end)"
      Datatype.Filepath.pretty f;
    (match Hashtbl.find_opt check_suffixes suf with
     | Some parse -> parse (f:>string)
     | None ->
       Kernel.abort
         "could not find a suitable plugin for parsing %a."
         Filepath.Normalized.pretty f)

let to_cil_cabs cpp_cmds_and_args f =
  let cpp_command = List.assoc f cpp_cmds_and_args in
  let a,c = parse_cabs cpp_command f in
  Kernel.debug ~dkey:Kernel.dkey_file_print_one "result of parsing %s:@\n%a"
    (get_name f) Cil_printer.pp_file a;
  if Errorloc.had_errors () then
    Kernel.abort "@[stopping on@ file %S@ that@ has@ errors.%t@]"
      (get_name f)
      (fun fmt ->
         if Filename.check_suffix (get_name f :> string) ".c" &&
            not (Kernel.is_debug_key_enabled Kernel.dkey_pp)
         then
           Format.fprintf fmt "@ Add@ '-kernel-msg-key pp'@ \
                               for preprocessing command.");
  a, c

let () =
  let handle f =
    let preprocess =
      replace_in_cpp_cmd (get_preprocessor_command ()) "-nostdinc"
    in
    let ppf =
      try Logic_preprocess.file ".c" preprocess f
      with Sys_error _ as e ->
        Kernel.abort "preprocessing of annotations failed (%s)"
          (Printexc.to_string e)
    in
    let path = Datatype.Filepath.of_string f in
    let (cil,(_,defs)) = Frontc.parse ppf () in
    cil.fileName <- path;
    safe_remove_file ppf;
    (cil,(path,defs))
  in
  new_file_type ".ci" handle



(* Keep defined entry point even if not defined, and possibly
   other unused globals according to relevant command-line parameters.
   This function is meant to be passed to {!Rmtmps.removeUnused}. *)
let isRoot g =
  let keepFuncs = Kernel.KeepUnusedFunctions.get () in
  let keepTypes = Kernel.Keep_unused_types.get () in
  Rmtmps.isExportedRoot g ||
  match g with
  | GFun({svar = v; sspec = spec},_)
  | GFunDecl(spec,v,_) ->
    (* Always keep the declaration of the entry point... *)
    Kernel.MainFunction.get_plain_string () = v.vname
    (* ... and the declarations of unused functions according to
       the command-line option *)
    || keepFuncs = "all_debug"
    || (keepFuncs = "all" && not (Cil_builtins.Builtin_functions.mem v.vname))
    || (keepFuncs = "specified" && not (is_empty_funspec spec))
  | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _ ->
    keepTypes
  | _ -> false

let files_to_cabs_cil files cpp_commands =
  Kernel.feedback ~level:2 "parsing";
  (* Parsing and merging must occur in the very same order.
     Otherwise the order of files on the command line will not be consistently
     handled. *)
  let cil_cabs = List.fold_left (fun acc f -> to_cil_cabs cpp_commands f :: acc) [] files in
  let cil_files, cabs_files = List.split cil_cabs in
  (* fold_left reverses the list order.
     This is an issue with pre-registered files. *)
  let cil_files = List.rev cil_files in
  let cabs_files = List.rev cabs_files in
  Ast.UntypedFiles.set cabs_files;
  (* Perform symbolic merge of all files *)
  Kernel.feedback ~level:2 "symbolic link";
  let merged_file = Mergecil.merge cil_files "whole_program" in
  Logic_utils.complete_types merged_file;
  if Kernel.UnspecifiedAccess.get () then
    Undefined_sequence.check_sequences merged_file;
  merged_file, cabs_files

(* "Implicit" annotations are those added by the kernel with ACSL name
   'Frama_C_implicit_init'. Currently, this concerns statements that are
   generated to initialize local variables. *)
module Implicit_annotations =
  State_builder.Hashtbl
    (Property.Hashtbl)(Datatype.List(Property))
    (struct
      let name = "File.Implicit_annotations"
      let dependencies = [Annotations.code_annot_state]
      let size = 32
    end)

let () = Ast.add_linked_state Implicit_annotations.self

let () =
  Property_status.register_property_remove_hook
    (fun p ->
       if Implicit_annotations.mem p then begin
         Kernel.debug ~dkey:Kernel.dkey_file_annot
           "Removing implicit property %a" Property.pretty p;
         Implicit_annotations.remove p
       end)

let emit_status p hyps =
  Kernel.debug ~dkey:Kernel.dkey_file_annot
    "Marking implicit property %a as true" Property.pretty p;
  Property_status.emit Emitter.kernel ~hyps p Property_status.True

let emit_all_statuses _ =
  Kernel.debug ~dkey:Kernel.dkey_file_annot "Marking properties";
  Implicit_annotations.iter emit_status

let () = Ast.apply_after_computed emit_all_statuses

let add_annotation kf st a =
  Annotations.add_code_annot ~keep_empty:false Emitter.end_user ~kf st a;
  (* Now check if the annotation is valid by construction
     (provided normalization is correct). *)
  match a.annot_content with
  | AStmtSpec
      ([],
       ({ spec_behavior = [ { b_name = "Frama_C_implicit_init" } as bhv]})) ->
    let props =
      Property.ip_post_cond_of_behavior kf (Kstmt st) ~active:[] bhv
    in
    List.iter (fun p -> Implicit_annotations.add p []) props
  | _ -> ()

let synchronize_source_annot has_new_stmt kf =
  match kf.fundec with
  | Definition (fd,_) ->
    let (visitor:cilVisitor) = object
      inherit nopCilVisitor as super
      val block_with_user_annots = ref None
      val user_annots_for_next_stmt = ref []
      method! vstmt st =
        super#pop_stmt st;
        let father = super#current_stmt in
        super#push_stmt st;
        let is_in_same_block () = match !block_with_user_annots,father with
          | None, None -> true
          | Some block, Some stmt_father when block == stmt_father -> true
          | _, _ -> false
        in
        let synchronize_user_annot a = add_annotation kf st a in
        let synchronize_previous_user_annots () =
          if !user_annots_for_next_stmt <> [] then begin
            if is_in_same_block () then begin
              let my_annots = !user_annots_for_next_stmt in
              let post_action st =
                let treat_annot (has_annot,st) (st_ann, annot) =
                  if Logic_utils.is_annot_next_stmt annot then begin
                    if has_annot || st.labels <> [] || st_ann.labels <> []
                    then begin
                      st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
                      has_new_stmt := true;
                      Annotations.add_code_annot
                        ~keep_empty:false Emitter.end_user ~kf st_ann annot;
                      (true, st_ann)
                    end else begin
                      add_annotation kf st annot;
                      (true,st)
                    end
                  end else begin
                    add_annotation kf st annot;
                    (true, st)
                  end
                in
                let (_,st) =
                  List.fold_left treat_annot (false,st) my_annots
                in
                st
              in
              block_with_user_annots:=None;
              user_annots_for_next_stmt:=[];
              ChangeDoChildrenPost(st,post_action)
            end
            else begin
              Kernel.warning ~current:true ~once:true
                "Ignoring previous annotation relative \
                 to next statement effects" ;
              block_with_user_annots := None ;
              user_annots_for_next_stmt := [];
              DoChildren
            end
          end else begin
            block_with_user_annots := None ;
            user_annots_for_next_stmt := [];
            DoChildren;
          end
        in
        let add_user_annot_for_next_stmt st annot =
          if !user_annots_for_next_stmt = [] then begin
            block_with_user_annots := father;
            user_annots_for_next_stmt := [st,annot]
          end else if is_in_same_block () then
            user_annots_for_next_stmt :=
              (st, annot)::!user_annots_for_next_stmt
          else begin
            Kernel.warning ~current:true ~once:true
              "Ignoring previous annotation relative to next statement \
               effects";
            block_with_user_annots := father;
            user_annots_for_next_stmt := [st, annot] ;
          end;
          ChangeTo (Cil.mkStmtOneInstr (Skip Cil_datatype.Location.unknown))
        in
        assert (!block_with_user_annots = None
                || !user_annots_for_next_stmt <> []);
        match st.skind with
        | Instr (Code_annot (annot,_)) ->
          (* Code annotation isn't considered as a real stmt.
             So, previous annotations should be relative to the next stmt.
             Only this [annot] may be synchronised to that stmt *)
          if Logic_utils.is_annot_next_stmt annot then
            (* Annotation relative to the effect of next statement *)
            add_user_annot_for_next_stmt st annot
          else
            (* Annotation relative to the current control point *)
            (match !user_annots_for_next_stmt with
             | [] -> synchronize_user_annot annot; DoChildren
             | _ ->
               (* we have an annotation relative to the next
                  real C statement somewhere above, and we have
                  not reached it yet. Just stack the current annotation.*)
               add_user_annot_for_next_stmt st annot)
        | Loop (annot, _, _, _, _) ->
          (* Synchronize previous annotations on that statement *)
          let res = synchronize_previous_user_annots () in
          (* Synchronize loop annotations on that statement *)
          List.iter synchronize_user_annot
            (List.sort (fun x y -> x.annot_id - y.annot_id) annot);
          res
        | _ ->
          (* Synchronize previous annotations on that statement *)
          synchronize_previous_user_annots () ;
    end
    in
    ignore (visitCilFunction visitor fd)
  | Declaration _ -> ()

let register_global = function
  | GFun (fundec, loc) ->
    let onerets = ref [] in
    let callback return goto = onerets := (return,goto) :: !onerets in
    (* ensure there is only one return *)
    Oneret.oneret ~callback fundec;
    (* Build the Control Flow Graph for all
         functions *)
    if Kernel.SimplifyCfg.get () then begin
      Cfg.prepareCFG ~keepSwitch:(Kernel.KeepSwitch.get ()) fundec;
      Cfg.clearCFGinfo fundec;
      Cfg.cfgFun fundec;
      (* prepareCFG may add additional labels that are not used in the end. *)
      Rmtmps.remove_unused_labels fundec;
    end;
    Globals.Functions.add (Definition(fundec,loc));
    let kf = Globals.Functions.get fundec.svar in
    (* Finally set property-status on oneret clauses *)
    List.iter
      (fun ((sret,b,pret),gotos) ->
         let ipreturns =
           Property.ip_of_ensures kf (Kstmt sret) b (Returns,pret) in
         let ipgotos = List.map
             (fun (sgot,agot) -> Property.ip_of_code_annot_single kf sgot agot)
             gotos in
         Implicit_annotations.add ipreturns ipgotos
      ) !onerets ;
  | GFunDecl (spec, f,loc) ->
    (* global prototypes *)
    let args =
      try Some (Cil.getFormalsDecl f) with Not_found -> None
    in
    (* Use a copy of the spec, as the original one will be erased by
       AST cleanup. *)
    let spec = { spec with spec_variant = spec.spec_variant } in
    Globals.Functions.add (Declaration(spec,f,args,loc))
  | GVarDecl (vi,_) when not vi.vdefined ->
    (* global variables declaration with no definitions *)
    Globals.Vars.add_decl vi
  | GVar (varinfo,initinfo,_) ->
    (* global variables definitions *)
    Globals.Vars.add varinfo initinfo;
  | GAnnot (annot,_loc) ->
    Annotations.add_global Emitter.end_user annot
  | _ -> ()

let computeCFG ~clear_id file =
  Cfg.clearFileCFG ~clear_id file;
  Cfg.computeFileCFG file

(* Remove (inplace) annotations that are physically in the AST (and that have
   been moved inside kernel tables) by turning them into Skip, then
   remove empty statements and blocks. *)
let cleanup file =
  let visitor = object(self)
    inherit Visitor.frama_c_inplace

    val mutable keep_stmt = Cil_datatype.Stmt.Set.empty

    val mutable changed = false

    method private remove_lexical_annotations stmt =
      match stmt.skind with
      | Instr(Code_annot(_,loc)) ->
        stmt.skind <- Instr(Skip(loc))
      | Loop (_::_, b1,l1,s1,s2) ->
        stmt.skind <- Loop ([], b1, l1, s1, s2)
      | _ -> ()

    method! vstmt_aux st =
      self#remove_lexical_annotations st;
      let loc = Cil_datatype.Stmt.loc st in
      if Annotations.has_code_annot st || st.labels <> [] || st.sattr <> [] then
        keep_stmt <- Cil_datatype.Stmt.Set.add st keep_stmt;
      match st.skind with
      | Block b ->
        (* queue is flushed afterwards*)
        let b' = Cil.visitCilBlock (self:>cilVisitor) b in
        (match b'.bstmts, b'.blocals, b'.bstatics with
         | [], [], [] -> changed <- true; st.skind <- (Instr (Skip loc))
         | _ -> if b != b' then st.skind <- Block b');
        SkipChildren
      | _ -> DoChildren

    method! vblock b =
      let optim b =
        b.bstmts <-
          List.filter
            (fun x ->
               not (Cil.is_skip x.skind)
               || Cil_datatype.Stmt.Set.mem x keep_stmt
               || (changed <- true; false)
            )
            b.bstmts;
        (* Now that annotations are in the table, we do not need to
           retain the block anymore.
        *)
        b.battrs <- List.filter
            (function
              | Attr(l,[]) when l = Cabs2cil.frama_c_keep_block -> false
              | _ -> true)
            b.battrs;
        b
      in
      (* uncomment if you don't want to consider scope of locals (see below) *)
      (* b.blocals <- [];*)
      ChangeDoChildrenPost(b,optim)