diff --git a/Makefile b/Makefile
index 8ea18cfabc8ee2ee552292fa7fc2615a07b696c7..49b29bb737853c53dbacb402a7853791203c3a1a 100644
--- a/Makefile
+++ b/Makefile
@@ -839,7 +839,7 @@ endif
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
- utils/value_perf utils/eva_annotations \
+ utils/eva_audit utils/value_perf utils/eva_annotations \
utils/value_util utils/red_statuses \
utils/mark_noresults \
utils/widen_hints_ext utils/widen \
diff --git a/doc/value/main.tex b/doc/value/main.tex
index a1e9c8363d968adcd504324032e94b471bb1bc52..dac4374ae5f2379dcc3cc12637a44b3d7b220cbd 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -2033,6 +2033,50 @@ by the Report plugin.
The summary display can be disabled by using option
\lstinline|-eva-msg-key=-summary|.
+\subsection{Audit messages ({\em experimental})}
+
+Using options \lstinline|-audit-prepare| and \lstinline|-audit-check|, the
+user can produce and check some information relevant for auditing purposes.
+
+\lstinline|-audit-prepare <file>| outputs the following information:
+
+\begin{itemize}
+\item the list of all source files used during parsing: not only those
+ given in the command line, but also those in \lstinline|#include|
+ directives, recursively. This usually includes Frama-C's standard library.
+ For each file, its MD5 checksum is also printed;
+\item the list of {\em enabled} and {\em disabled} warning categories,
+ for the kernel as well as for \Eva{}. Warning categories are considered
+ disabled when set to one of the following actions: {\em inactive},
+ {\em feedback}, and {\em feedback-once}. All other actions are considered
+ as enabled;
+\item the list of Eva's {\em correctness parameters}, along with their values
+ at the moment when Eva is run.
+\end{itemize}
+
+The information is written to \lstinline|<file>|, in JSON format, unless it
+is the special value \lstinline|-| (given as \lstinline|-audit-prepare=-|),
+in which case the information is printed to the standard output in text format.
+
+The complementary option \lstinline|-audit-check file| takes a JSON file
+produced by \lstinline|-audit-prepare| and checks if all checksums, warning
+category statuses and correctness parameters match. Any discrepancies are
+reported and result in an error by default.
+
+The main intent of these options is to help users perform audit-related
+tasks concerning an analysis performed with Eva. It also helps fine-tuning
+analyses without affecting its correctness; for instance, since it omits
+information related to parameters which do not affect correctness, the user
+is free to adjust them to improve the speed and precision of the analysis.
+
+Note that these options are still in experimental stage, and should not be
+blindly relied upon for strict auditing purposes. For instance, they do
+not record information related to syntactic transformations performed by
+plugins such as \textsf{Variadic}, which can have an indirect impact on
+its correctness.
+
+Please contact the Frama-C development team if you intend to use these
+options in a production setting.
\section{About these alarms the user is supposed to check\ldots}
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 412e563ceb435794e2ffdfa97b05aa111af3a4ed..12f47d738bde8c22fc84e36987e7250514c3f6bb 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1386,6 +1386,8 @@ src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_audit.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index ec61b34cb9f1eea70091b98cd29963cbfe82d93f..6cd0cc0cecf3212337ddc80ec4ea9b66baa0ffb8 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -87,9 +87,8 @@ let get_suffixes () =
check_suffixes
[ ".c"; ".i"; ".h" ]
-let get_name s =
- let file = match s with NeedCPP (s,_,_,_) | NoCPP s | External (s,_) -> s in
- Filepath.Normalized.to_pretty_string file
+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} *)
@@ -407,6 +406,12 @@ let pretty_machdep ?fmt ?machdep () =
(** {2 Initializations} *)
(* ************************************************************************* *)
+let create_temp_file ?debug name suffix =
+ 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_parser) then
Extlib.safe_remove (f :> string)
@@ -462,14 +467,7 @@ let build_cpp_cmd = function
opt;
[opt]
in
- let ppf =
- try
- Datatype.Filepath.of_string
- (Extlib.temp_file_cleanup_at_exit ~debug
- (Filename.basename (f :> string)) ".i")
- with Extlib.Temp_file_error s ->
- Kernel.abort "cannot create temporary file: %s" s
- in
+ let ppf = create_temp_file ~debug (Filename.basename (f :> string)) ".i" in
(* Hypothesis: the preprocessor is POSIX compliant,
hence understands -I and -D. *)
let include_args =
@@ -1605,19 +1603,160 @@ let init_cil () =
Logic_env.Builtins.apply ();
Logic_env.prepare_tables ()
+let re_included_file = Str.regexp "^[.]+ \\(.*\\)$"
+
+let file_hash file =
+ Digest.to_hex (Digest.file file)
+
+let add_source_if_new tbl (fp : Filepath.Normalized.t) =
+ if not (Hashtbl.mem tbl fp) then
+ Hashtbl.replace tbl fp (file_hash (fp:>string))
+
+(* Inserts, into the hashtbl of (Filepath.Normalized.t, Digest.t), [tbl],
+ the included sources listed in [file],
+ which contains the output of 'gcc -H -MM'. *)
+let add_included_sources tbl file =
+ let ic = open_in file in
+ try
+ while true; do
+ let line = input_line ic in
+ if Str.string_match re_included_file line 0 then
+ let f = Str.matched_group 1 line in
+ add_source_if_new tbl (Filepath.Normalized.of_string f)
+ done;
+ assert false
+ with End_of_file ->
+ close_in ic
+
+let print_all_sources out all_sources_tbl =
+ let elems =
+ Hashtbl.fold (fun f hash acc ->
+ (Filepath.Normalized.to_pretty_string f, hash) :: acc)
+ all_sources_tbl []
+ in
+ let sorted_elems =
+ List.sort (fun (f1, _) (f2, _) -> Extlib.compare_ignore_case f1 f2) elems
+ in
+ if Filepath.Normalized.is_special_stdout out then begin
+ (* text format, to stdout *)
+ Kernel.feedback "Audit: all used sources, with md5 hashes:@\n%a"
+ (Pretty_utils.pp_list ~sep:"@\n"
+ (Pretty_utils.pp_pair ~sep:": "
+ Format.pp_print_string Format.pp_print_string)) sorted_elems
+ end else begin
+ (* json format, into file [out] *)
+ let json =
+ `Assoc
+ [("sources",
+ `Assoc (List.map (fun (f, hash) -> f, `String hash) sorted_elems)
+ )]
+ in
+ Json.merge_object out json
+ end
+
+let compute_sources_table cpp_commands =
+ let all_sources_tbl = Hashtbl.create 7 in
+ let process_file (file, cmd_opt) =
+ add_source_if_new all_sources_tbl (get_filepath file);
+ match cmd_opt with
+ | None -> ()
+ | Some (cpp_cmd, _ppf, _sl) ->
+ let tmp_file = create_temp_file "audit_produce_sources" ".txt" in
+ let tmp_file = (tmp_file :> string) in
+ let cmd_for_sources = cpp_cmd ^ " -H -MM >/dev/null 2>" ^ tmp_file in
+ let exit_code = Sys.command cmd_for_sources in
+ if exit_code = 0
+ then add_included_sources all_sources_tbl tmp_file
+ else
+ let cause_frama_c_compliant =
+ if Kernel.CppGnuLike.get () then "" else
+ Format.asprintf
+ "\nPlease ensure preprocessor is Frama-C compliant \
+ (see option %s)" Kernel.CppGnuLike.option_name
+ in
+ Kernel.abort "error running command to obtain included sources \
+ (exit code %d):@\n%s%s"
+ exit_code cmd_for_sources cause_frama_c_compliant;
+ in
+ List.iter process_file cpp_commands;
+ all_sources_tbl
+
+let source_hashes_of_json path =
+ try
+ let json = Json.from_file path in
+ let open Yojson.Basic.Util in
+ json |> member "sources" |> to_assoc |>
+ List.map (fun (k, h) -> k, to_string h)
+ with
+ | Yojson.Json_error msg ->
+ Kernel.abort "error reading %a: %s"
+ Filepath.Normalized.pretty path msg
+ | Yojson.Basic.Util.Type_error (msg, v) ->
+ Kernel.abort "error reading %a: %s - %s"
+ Filepath.Normalized.pretty path msg
+ (Yojson.Basic.pretty_to_string v)
+
+let check_source_hashes expected actual_table =
+ let checked, diffs =
+ Hashtbl.fold (fun fp hash (acc_checked, acc_diffs) ->
+ let fp = Filepath.Normalized.to_pretty_string fp in
+ let expected_hash = List.assoc_opt fp expected in
+ let checked = Datatype.String.Set.add fp acc_checked in
+ let diffs =
+ if Some hash = expected_hash then acc_diffs
+ else (fp, hash, expected_hash) :: acc_diffs
+ in
+ checked, diffs
+ ) actual_table (Datatype.String.Set.empty, [])
+ in
+ if diffs <> [] then begin
+ let diffs =
+ List.sort (fun (fp1, _, _) (fp2, _, _) ->
+ Extlib.compare_ignore_case fp1 fp2) diffs
+ in
+ List.iter (fun (fp, got, expected) ->
+ Kernel.warning ~wkey:Kernel.wkey_audit
+ "different hashes for %s: got %s, expected %s"
+ fp got (Option.value ~default:("<none> (not in list)") expected)
+ ) diffs
+ end;
+ let expected_names = List.map fst expected in
+ let missing =
+ List.filter (fun fp -> not (Datatype.String.Set.mem fp checked))
+ expected_names
+ in
+ if missing <> [] then begin
+ let missing = List.sort Extlib.compare_ignore_case missing in
+ Kernel.warning ~wkey:Kernel.wkey_audit
+ "missing files:@\n%a"
+ (Pretty_utils.pp_list ~sep:"@\n" Format.pp_print_string) missing
+ end
+
+let print_and_exit cpp_commands =
+ let print_cpp_cmd (cpp_cmd, _ppf, _) =
+ Kernel.result "Preprocessing command:@.%s" cpp_cmd
+ in
+ List.iter (fun (_f, ocmd) -> Option.iter print_cpp_cmd ocmd) cpp_commands;
+ raise Cmdline.Exit
+
let prepare_from_c_files () =
init_cil ();
let files = Files.get () in (* Allow pre-registration of prolog files *)
let cpp_commands = List.map (fun f -> (f, build_cpp_cmd f)) files in
- if Kernel.PrintCppCommands.get () then begin
- List.iter (fun (_f, opt_cpp_cmd) ->
- match opt_cpp_cmd with
- | None -> ()
- | Some (cpp_cmd, _ppf, _) ->
- Kernel.result
- "Preprocessing command:@.%s" cpp_cmd
- ) cpp_commands;
- raise Cmdline.Exit
+ if Kernel.PrintCppCommands.get () then print_and_exit cpp_commands;
+ let audit_check_path = Kernel.AuditCheck.get () in
+ if not (Filepath.Normalized.is_unknown audit_check_path) then begin
+ let all_sources_tbl = compute_sources_table cpp_commands in
+ let expected_hashes = source_hashes_of_json audit_check_path in
+ check_source_hashes expected_hashes all_sources_tbl
+ end;
+ let audit_path = Kernel.AuditPrepare.get () in
+ if not (Filepath.Normalized.is_unknown audit_path) then begin
+ let all_sources_tbl = compute_sources_table cpp_commands in
+ print_all_sources audit_path all_sources_tbl;
+ if not (Filepath.Normalized.is_special_stdout audit_path) then
+ Kernel.feedback "Audit: sources list written to: %a@."
+ Filepath.Normalized.pretty audit_path;
end;
let cil, cabs_files = files_to_cabs_cil files cpp_commands in
prepare_cil_file cil;
@@ -1763,8 +1902,7 @@ let create_rebuilt_project_from_visitor
let name = "frama_c_project_" ^ prj_name ^ "_" in
let ext = if preprocess then ".c" else ".i" in
let debug = Kernel.Debug.get () > 0 in
- let tmp_fname = Extlib.temp_file_cleanup_at_exit ~debug name ext in
- Filepath.Normalized.of_string tmp_fname
+ create_temp_file ~debug name ext
in
let cout = open_out (f :> string) in
let fmt = Format.formatter_of_out_channel cout in
@@ -1776,7 +1914,7 @@ let create_rebuilt_project_from_visitor
in
Project.on prj redo ();
prj
- with Extlib.Temp_file_error s | Sys_error s ->
+ with Sys_error s ->
Kernel.abort "cannot create temporary file: %s" s
(*
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 4444276b7a8545a8c79636a82ec4e0651db45579..e21274bd4b33a08bc8ebb31782b30d56a9ebff6d 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -194,6 +194,9 @@ let wkey_acsl_extension = register_warn_category "acsl-extension"
let wkey_cmdline = register_warn_category "cmdline"
+let wkey_audit = register_warn_category "audit"
+let () = set_warn_status wkey_audit Log.Werror
+
(* ************************************************************************* *)
(** {2 Specialised functors for building kernel parameters} *)
(* ************************************************************************* *)
@@ -1040,6 +1043,41 @@ module PrintCppCommands =
and exits."
end)
+let () = Parameter_customize.set_group parsing
+let () = Parameter_customize.do_not_reset_on_copy ()
+module AuditPrepare =
+ P.Filepath
+ (struct
+ let option_name = "-audit-prepare"
+ let arg_name = "path"
+ let existence = Filepath.Indifferent
+ let file_kind = "json"
+ let help = "produces audit-related information, such as the list of all \
+ source files used during parsing (including those in include \
+ directives) with checksums. Some plug-ins may produce \
+ additional audit-related information. \
+ Prints the information as JSON to the specified file, or \
+ if the file is '-', prints as text to the standard output. \
+ Requires -cpp-frama-c-compliant."
+ end)
+
+let () = Parameter_customize.set_group parsing
+let () = Parameter_customize.do_not_reset_on_copy ()
+module AuditCheck =
+ P.Filepath
+ (struct
+ let option_name = "-audit-check"
+ let arg_name = "path"
+ let existence = Filepath.Must_exist
+ let file_kind = "json"
+ let help = "reads an audit JSON file (produced by -audit-prepare) and \
+ checks compliance w.r.t. it; e.g., if the source files \
+ were declared and have the expected checksum. \
+ Raises a warning (with warning key 'audit') in case of \
+ failed checks. \
+ Requires -cpp-frama-c-compliant."
+ end)
+
let () = Parameter_customize.set_group parsing
let () = Parameter_customize.do_not_reset_on_copy ()
module FramaCStdLib =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index bb6247d651b2769ba236ffb8aa07aa6f9e3e5634..a6e7e409bca45d77489b1e2576724809180c2e6e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -186,6 +186,9 @@ val wkey_acsl_extension: warn_category
val wkey_cmdline: warn_category
(** Command-line related warning, e.g. for invalid options given by the user *)
+val wkey_audit: warn_category
+(** Warning related to options '-audit-*'. *)
+
(* ************************************************************************* *)
(** {2 Functors for late option registration} *)
(** Kernel_function-related options cannot be registered in this module:
@@ -414,6 +417,12 @@ module CppGnuLike: Parameter_sig.Bool
module PrintCppCommands: Parameter_sig.Bool
(** Behavior of option "-print-cpp-commands" *)
+module AuditPrepare: Parameter_sig.Filepath
+(** Behavior of option "-audit-prepare" *)
+
+module AuditCheck: Parameter_sig.Filepath
+(** Behavior of option "-audit-check" *)
+
module FramaCStdLib: Parameter_sig.Bool
(** Behavior of option "-frama-c-stdlib" *)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 5cb98e37e081c78603150f34bbf50b2e184901ba..93fd504680369faf45e68100017c4acf5552ea39 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -173,6 +173,10 @@ let reset_analyzer () =
let force_compute () =
Ast.compute ();
Value_parameters.configure_precision ();
+ if not (Filepath.Normalized.is_unknown (Kernel.AuditCheck.get ()))
+ then Eva_audit.check_configuration (Kernel.AuditCheck.get ());
+ if not (Filepath.Normalized.is_unknown (Kernel.AuditPrepare.get ()))
+ then Eva_audit.print_configuration (Kernel.AuditPrepare.get ());
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
let module Analyzer = (val snd !ref_analyzer) in
diff --git a/src/plugins/value/utils/eva_audit.ml b/src/plugins/value/utils/eva_audit.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f7e10c46cf07a9449a120bde4371bba451f75233
--- /dev/null
+++ b/src/plugins/value/utils/eva_audit.ml
@@ -0,0 +1,146 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let get_correctness_parameters () =
+ let get param =
+ let name = param.Typed_parameter.name in
+ let value = Typed_parameter.get_value param in
+ (name, value)
+ in
+ List.map get (Value_parameters.parameters_correctness)
+
+let parameters_of_json json =
+ try
+ let open Yojson.Basic.Util in
+ let params =
+ json |> member "eva" |> member "correctness-parameters" |> to_assoc
+ in
+ List.map (fun (key, value) -> (key, to_string value)) params
+ with
+ | Yojson.Json_error msg ->
+ Kernel.abort "error reading JSON file: %s" msg
+ | Yojson.Basic.Util.Type_error (msg, v) ->
+ Kernel.abort "error reading JSON file: %s - %s" msg
+ (Yojson.Basic.pretty_to_string v)
+
+let print_correctness_parameters path =
+ let parameters = get_correctness_parameters () in
+ if Filepath.Normalized.is_special_stdout path then begin
+ Value_parameters.feedback "Correctness parameters of the analysis:";
+ let print (name, value) = Value_parameters.printf " %s: %s" name value in
+ List.iter print parameters
+ end else begin
+ let json = List.map (fun (name, value) -> name, `String value) parameters in
+ let params_json = `Assoc [("correctness-parameters", `Assoc json)] in
+ let eva_json = `Assoc [("eva", params_json)] in
+ Json.merge_object path eva_json
+ end
+
+let check_correctness_parameters json =
+ let parameters = get_correctness_parameters () in
+ let expected_parameters = parameters_of_json json in
+ (* Note: we could compare lengths and use a two-list iterator on sorted lists,
+ but in case of divergence, the error messages would be less clear. *)
+ List.iter (fun (exp_p, exp_v) ->
+ try
+ let v = List.assoc exp_p parameters in
+ if exp_v <> v then
+ Kernel.warning ~wkey:Kernel.wkey_audit
+ "correctness parameter %s: expected value %s, but got %s" exp_p
+ exp_v v
+ with Not_found ->
+ Kernel.warning ~wkey:Kernel.wkey_audit
+ "expected correctness parameter %s, but not found" exp_p
+ ) expected_parameters
+
+let compute_warning_status (module Plugin: Log.Messages) =
+ let warning_categories = Plugin.get_all_warn_categories_status () in
+ let is_active = function
+ | Log.Winactive | Wfeedback_once | Wfeedback -> false
+ | Wonce | Wactive | Werror_once | Werror | Wabort -> true
+ in
+ let is_enabled (_key, status) = is_active status in
+ let enabled, disabled = List.partition is_enabled warning_categories in
+ let pp_fst = List.map (fun (c, s) -> Plugin.wkey_name c, s) in
+ (pp_fst enabled, pp_fst disabled)
+
+let json_of_warning_statuses wkeys key_name =
+ let json_of_wkey = List.map (fun (c, _) -> `String c) in
+ (key_name, `List (json_of_wkey wkeys))
+
+let enabled_warning_of_json name json =
+ try
+ let open Yojson.Basic.Util in
+ json |> member name |> member "warning-categories" |>
+ member "enabled" |> to_list |> filter_string
+ with
+ | Yojson.Json_error msg ->
+ Kernel.abort "error reading JSON file: %s" msg
+ | Yojson.Basic.Util.Type_error (msg, v) ->
+ Kernel.abort "error reading JSON file: %s - %s" msg
+ (Yojson.Basic.pretty_to_string v)
+
+let print_warning_status path name (module Plugin: Log.Messages) =
+ let enabled, disabled = compute_warning_status (module Plugin) in
+ if Filepath.Normalized.is_special_stdout path then
+ begin
+ let pp_categories =
+ Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string
+ in
+ Value_parameters.feedback "Audit: %s warning categories:" name;
+ Value_parameters.printf " Enabled: @[%a@]"
+ pp_categories (List.map fst enabled);
+ Value_parameters.printf " Disabled: @[%a@]"
+ pp_categories (List.map fst disabled)
+ end
+ else begin
+ let enabled_json = json_of_warning_statuses enabled "enabled"
+ and disabled_json = json_of_warning_statuses disabled "disabled" in
+ let warning_json = `Assoc [enabled_json; disabled_json] in
+ let name = Stdlib.String.lowercase_ascii name in
+ let json = `Assoc [(name, `Assoc [("warning-categories", warning_json)])] in
+ Json.merge_object path json
+ end
+
+let check_warning_status json name (module Plugin: Log.Messages) =
+ let name = Stdlib.String.lowercase_ascii name in
+ let enabled, _disabled = compute_warning_status (module Plugin) in
+ let enabled = List.map fst enabled in
+ let expected_enabled = enabled_warning_of_json name json in
+ let diff l1 l2 = List.filter (fun k -> not (List.mem k l2)) l1 in
+ let should_be_enabled = diff expected_enabled enabled in
+ if should_be_enabled <> [] then
+ Kernel.warning ~wkey:Kernel.wkey_audit
+ "the following warning categories were expected to be enabled,@ \
+ but are disabled: %a"
+ (Pretty_utils.pp_list ~sep:", " Format.pp_print_string) should_be_enabled
+
+let check_configuration path =
+ let json = Json.from_file path in
+ check_correctness_parameters json;
+ check_warning_status json "Kernel" (module Kernel);
+ check_warning_status json "Eva" (module Value_parameters)
+
+let print_configuration path =
+ print_correctness_parameters path;
+ print_warning_status path "Kernel" (module Kernel);
+ print_warning_status path "Eva" (module Value_parameters)
diff --git a/src/plugins/value/utils/eva_audit.mli b/src/plugins/value/utils/eva_audit.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7cd6bff0d6ef912d07cb6db454a0c80c9b5458e9
--- /dev/null
+++ b/src/plugins/value/utils/eva_audit.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* 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 check_configuration: Filepath.Normalized.t -> unit
+val print_configuration: Filepath.Normalized.t -> unit
diff --git a/tests/value/audit-in.json b/tests/value/audit-in.json
new file mode 100644
index 0000000000000000000000000000000000000000..d6abf18d0ffb9f05e82b0d158058b8715f36f417
--- /dev/null
+++ b/tests/value/audit-in.json
@@ -0,0 +1,77 @@
+{
+ "sources": {
+ "tests/value/audit.c": "01010101010101010101010101010101",
+ "tests/value/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e",
+ "tests/value/non_existing_file.h": "1234567890abcdef1234567890abcdef"
+ },
+ "kernel": {
+ "warning-categories": {
+ "enabled": [
+ "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:38",
+ "acsl-extension", "annot", "annot:missing-spec", "annot-error",
+ "audit", "check", "check:volatile", "cmdline", "ghost",
+ "ghost:bad-use", "inline", "linker",
+ "linker:drop-conflicting-unused", "parser",
+ "parser:conditional-feature", "pp", "pp:compilation-db", "typing",
+ "typing:implicit-conv-void-ptr",
+ "typing:implicit-function-declaration",
+ "typing:incompatible-pointer-types",
+ "typing:incompatible-types-call", "typing:inconsistent-specifier",
+ "typing:int-conversion", "typing:no-proto"
+ ],
+ "disabled": [
+ "CERT:EXP:10", "acsl-float-compare", "ghost:already-ghost",
+ "parser:decimal-float", "transient-block"
+ ]
+ }
+ },
+ "eva": {
+ "correctness-parameters": {
+ "-absolute-valid-range": "",
+ "-eva-all-rounding-modes-constants": "false",
+ "-eva-alloc-returns-null": "true",
+ "-eva-builtin": "",
+ "-eva-builtins-auto": "true",
+ "-eva-context-depth": "2",
+ "-eva-context-valid-pointers": "false",
+ "-eva-context-width": "2",
+ "-eva-ignore-recursive-calls": "false",
+ "-eva-initialization-padding-globals": "yes",
+ "-eva-initialized-locals": "false",
+ "-eva-new-initial-state": "0",
+ "-eva-reduce-on-logic-alarms": "false",
+ "-eva-undefined-pointer-comparison-propagate-all": "false",
+ "-eva-use-spec": "",
+ "-eva-warn-copy-indeterminate": "",
+ "-eva-warn-pointer-subtraction": "true",
+ "-eva-warn-signed-converted-downcast": "false",
+ "-eva-warn-undefined-pointer-comparison": "pointer",
+ "-initialized-padding-locals": "true",
+ "-lib-entry": "false",
+ "-main": "main",
+ "-safe-arrays": "true",
+ "-unspecified-access": "false",
+ "-warn-invalid-bool": "true",
+ "-warn-invalid-pointer": "false",
+ "-warn-left-shift-negative": "true",
+ "-warn-pointer-downcast": "true",
+ "-warn-right-shift-negative": "false",
+ "-warn-signed-downcast": "false",
+ "-warn-signed-overflow": "true",
+ "-warn-special-float": "non-finite",
+ "-warn-unsigned-downcast": "false",
+ "-warn-unsigned-overflow": "false"
+ },
+ "warning-categories": {
+ "enabled": [
+ "*", "alarm", "builtins", "builtins:missing-spec",
+ "builtins:override", "experimental", "libc", "libc:unsupported-spec",
+ "locals-escaping", "malloc", "malloc:imprecise", "signed-overflow"
+ ],
+ "disabled": [
+ "garbled-mix", "invalid-assigns", "loop-unroll", "malloc:weak",
+ "missing-loop-unroll", "missing-loop-unroll:for"
+ ]
+ }
+ }
+}
diff --git a/tests/value/audit.c b/tests/value/audit.c
new file mode 100644
index 0000000000000000000000000000000000000000..7b3e27c0eb13ce8bf3de6099b21131006f9de2be
--- /dev/null
+++ b/tests/value/audit.c
@@ -0,0 +1,11 @@
+/* run.config
+ LOG: audit-out.json
+ STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_DIR@/result/audit-out.json -kernel-warn-key audit=active"
+*/
+
+#include "audit_included.h"
+#include "audit_included_but_not_listed.h"
+
+void main() {
+ float f = 2.1; // to trigger a syntactic warning
+}
diff --git a/tests/value/audit_included.h b/tests/value/audit_included.h
new file mode 100644
index 0000000000000000000000000000000000000000..d4b481cc2ee4f9d292b6ea835cb8d09ef16780b7
--- /dev/null
+++ b/tests/value/audit_included.h
@@ -0,0 +1 @@
+// This file is included by audit.c
diff --git a/tests/value/audit_included_but_not_listed.h b/tests/value/audit_included_but_not_listed.h
new file mode 100644
index 0000000000000000000000000000000000000000..d4b481cc2ee4f9d292b6ea835cb8d09ef16780b7
--- /dev/null
+++ b/tests/value/audit_included_but_not_listed.h
@@ -0,0 +1 @@
+// This file is included by audit.c
diff --git a/tests/value/oracle/audit-out.json b/tests/value/oracle/audit-out.json
new file mode 100644
index 0000000000000000000000000000000000000000..f9aa254ce113486f162682dd6cebdc83f2a6768d
--- /dev/null
+++ b/tests/value/oracle/audit-out.json
@@ -0,0 +1,78 @@
+{
+ "eva": {
+ "correctness-parameters": {
+ "-absolute-valid-range": "",
+ "-eva-all-rounding-modes-constants": "false",
+ "-eva-alloc-returns-null": "true",
+ "-eva-builtin": "",
+ "-eva-builtins-auto": "true",
+ "-eva-context-depth": "2",
+ "-eva-context-valid-pointers": "false",
+ "-eva-context-width": "2",
+ "-eva-ignore-recursive-calls": "false",
+ "-eva-initialization-padding-globals": "yes",
+ "-eva-initialized-locals": "false",
+ "-eva-new-initial-state": "0",
+ "-eva-reduce-on-logic-alarms": "false",
+ "-eva-undefined-pointer-comparison-propagate-all": "false",
+ "-eva-use-spec": "",
+ "-eva-warn-copy-indeterminate": "",
+ "-eva-warn-pointer-subtraction": "true",
+ "-eva-warn-signed-converted-downcast": "false",
+ "-eva-warn-undefined-pointer-comparison": "pointer",
+ "-initialized-padding-locals": "true",
+ "-lib-entry": "false",
+ "-main": "main",
+ "-safe-arrays": "true",
+ "-unspecified-access": "false",
+ "-warn-invalid-bool": "true",
+ "-warn-invalid-pointer": "false",
+ "-warn-left-shift-negative": "true",
+ "-warn-pointer-downcast": "true",
+ "-warn-right-shift-negative": "false",
+ "-warn-signed-downcast": "false",
+ "-warn-signed-overflow": "true",
+ "-warn-special-float": "non-finite",
+ "-warn-unsigned-downcast": "false",
+ "-warn-unsigned-overflow": "false"
+ },
+ "warning-categories": {
+ "enabled": [
+ "*", "alarm", "builtins", "builtins:missing-spec",
+ "builtins:override", "experimental", "libc", "libc:unsupported-spec",
+ "locals-escaping", "malloc", "malloc:imprecise", "signed-overflow"
+ ],
+ "disabled": [
+ "garbled-mix", "invalid-assigns", "loop-unroll", "malloc:weak",
+ "missing-loop-unroll", "missing-loop-unroll:for"
+ ]
+ }
+ },
+ "kernel": {
+ "warning-categories": {
+ "enabled": [
+ "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:38",
+ "acsl-extension", "annot", "annot:missing-spec", "annot:multi-from",
+ "annot-error", "audit", "check", "check:volatile", "cmdline",
+ "ghost", "ghost:bad-use", "inline", "linker",
+ "linker:drop-conflicting-unused", "parser",
+ "parser:conditional-feature", "pp", "pp:compilation-db", "typing",
+ "typing:implicit-conv-void-ptr",
+ "typing:implicit-function-declaration",
+ "typing:incompatible-pointer-types",
+ "typing:incompatible-types-call", "typing:inconsistent-specifier",
+ "typing:int-conversion", "typing:no-proto"
+ ],
+ "disabled": [
+ "CERT:EXP:10", "acsl-float-compare", "ghost:already-ghost",
+ "parser:decimal-float", "transient-block"
+ ]
+ }
+ },
+ "sources": {
+ "tests/value/audit.c": "08f73691217888d926a0ee15cbe18159",
+ "tests/value/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e",
+ "tests/value/audit_included_but_not_listed.h":
+ "c2cc488143a476f69cf2ed04c3439e6e"
+ }
+}
diff --git a/tests/value/oracle/audit.res.oracle b/tests/value/oracle/audit.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..338a77c21a7297b49c9f9bf0e4c7faba157e6082
--- /dev/null
+++ b/tests/value/oracle/audit.res.oracle
@@ -0,0 +1,34 @@
+[kernel:audit] Warning:
+ different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101
+[kernel:audit] Warning:
+ different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list)
+[kernel:audit] Warning:
+ missing files:
+ tests/value/non_existing_file.h
+[kernel] Audit: sources list written to: tests/value/result/audit-out.json
+[kernel] Parsing tests/value/audit.c (with preprocessing)
+[kernel:parser:decimal-float] tests/value/audit.c:10: Warning:
+ Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ f ∈ {2.09999990463}
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ f
+[inout] Inputs for function main:
+ \nothing
+[kernel] Wrote: tests/value/result/audit-out.json