diff --git a/Makefile b/Makefile
index 58008950bb7de262a7fdac8788a8eb18e1dee6d3..344f46c5033ace000ddfe855e674f21575e1f985 100644
--- a/Makefile
+++ b/Makefile
@@ -856,7 +856,7 @@ endif
# - try to keep the legacy Value before Eva
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
utils/eva_audit utils/value_perf utils/eva_annotations \
- utils/value_util utils/red_statuses \
+ utils/eva_dynamic utils/value_util utils/red_statuses \
utils/mark_noresults \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
@@ -910,7 +910,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
utils/unit_tests
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
-PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server
+PLUGIN_DEPENDENCIES:=Server
# These files are used by the GUI, but do not depend on Lablgtk
VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \
diff --git a/configure.in b/configure.in
index 60f6dab2a2ca8ded43f37965ef3c099e0b52e3d8..a4895377d4a3705db3c720e0540419e69fdc1521 100644
--- a/configure.in
+++ b/configure.in
@@ -857,7 +857,8 @@ check_plugin(eva,src/plugins/value,
[support for value analysis],yes)
plugin_use(eva,gui)
plugin_use(eva,scope)
-plugin_require(eva,callgraph)
+plugin_use(eva,inout)
+plugin_use(eva,callgraph)
plugin_require(eva,server)
####################
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 8c8bf1b685894c8f968ab8958fc69db2f027aaec..4e8f0d8ddef50ed5ce934019dc0204bf6c676898 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1485,6 +1485,8 @@ 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/eva_dynamic.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_dynamic.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/summary.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/callgraph/uses.ml b/src/plugins/callgraph/uses.ml
index 2befdd59d1ab047dc12cfa9386e53166c8c8f991..728eae5ed726f01dcec646b1bdb66cb421682d6d 100644
--- a/src/plugins/callgraph/uses.ml
+++ b/src/plugins/callgraph/uses.ml
@@ -73,6 +73,15 @@ let iter_in_rev_order =
in
fun f -> I.iter (Cg.get ()) f
+let _iter_in_rev_order =
+ Dynamic.register
+ ~comment:"Iterate over all the functions in the callgraph in reverse order"
+ ~plugin:Options.name
+ "iter_in_rev_order"
+ Datatype.(func (func Kernel_function.ty unit) unit)
+ ~journalize:false
+ iter_in_rev_order
+
let iter_on_aux iter_dir f kf =
let cg = Cg.get () in
if Cg.G.mem_vertex cg kf then
@@ -116,6 +125,16 @@ let accept_base ~with_formals ~with_locals kf v =
| true , _, Declaration (_, vd, _, _) -> Base.is_formal_of_prototype v vd)
|| is_local_or_formal_of_caller v kf
+let _accept_base =
+ Dynamic.register
+ ~comment:"Returns [true] if the given base is a global, \
+ or a formal or local of either [kf] or one of its callers"
+ ~plugin:Options.name
+ "accept_base"
+ Datatype.(func2 Kernel_function.ty Base.ty bool)
+ ~journalize:false
+ (fun kf b -> accept_base ~with_formals:true ~with_locals:true kf b)
+
let nb_calls () =
let g = Cg.get () in
(* [g] contains bidirectional edges (from caller to callee and
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 4b7e902243355f0e452b7eff9bde9af57d8bc3aa..523f3a797a92b1f8c1a69565d6b40a2f8a758185 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -147,6 +147,15 @@ let _ignore =
~journalize:false
Visit.get_annotations_exp
+let _ignore =
+ let kf = Kernel_function.ty in
+ Dynamic.register
+ ~plugin:"RteGen"
+ "all_statuses"
+ Datatype.(list (triple string (func2 kf bool unit) (func kf bool)))
+ ~journalize:false
+ Generator.all_statuses
+
let main () =
(* reset "rte generated" properties for all functions *)
if Options.Enabled.get () then begin
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index d4cab9e063d6590ddcd1586d9fafb89941ba01e1..26d5806673e8aca286bbdc294cd813dc5c2202cd 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -28,11 +28,13 @@ open Cil_types
let cat_rm_asserts_name = "rm_asserts"
let () = Plugin.default_msg_keys [cat_rm_asserts_name]
+let name = "scope"
+
module R =
Plugin.Register
(struct
- let name = "scope"
- let shortname = "scope"
+ let name = name
+ let shortname = name
let help = "data dependencies higher level functions"
end)
@@ -694,6 +696,15 @@ let () =
("Value.rm_asserts", Datatype.func Datatype.unit Datatype.unit))
Db.Value.rm_asserts rm_asserts
+let rm_asserts =
+ Dynamic.register
+ ~comment:"Remove redundant alarms. Used by the Eva plugin."
+ ~plugin:name
+ "rm_asserts"
+ Datatype.(func unit unit)
+ ~journalize:true
+ rm_asserts
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 80abee069ddbf66e854c3852c71e984751c2c637..cd9f4376d4ef60a4c288d294eb3bca0ec1345b88 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -559,11 +559,13 @@ module State = struct
let display_results () =
Value_parameters.result "====== VALUES COMPUTED ======";
- Callgraph.Uses.iter_in_rev_order display;
+ Eva_dynamic.Callgraph.iter_in_rev_order display;
Value_parameters.result "%t" Value_perf.display
let post_analysis _state =
- if Value_parameters.ForceValues.get () && Value_parameters.verbose_atleast 1
+ if Value_parameters.ForceValues.get ()
+ && Value_parameters.verbose_atleast 1
+ && Plugin.is_present "inout"
then Value_parameters.ForceValues.output display_results
end
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 718da24a52985bef50b701c9ca5e90154106c37e..89f505305e48128fbed9ca567db7db6b36124c7b 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -54,6 +54,12 @@ let options_ok () =
Value_parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf);
Value_parameters.UsePrototype.iter (fun kf -> check_assigns kf)
+let plugins_ok () =
+ if not (Plugin.is_present "inout") then
+ Value_parameters.warning
+ "The inout plugin is missing: some features are disabled, \
+ and the analysis may have degraded precision and performance."
+
(* Do something tasteless in case the user did not put a spec on functions
for which he set [-eva-use-spec]: generate an incorrect one ourselves *)
let generate_specs () =
@@ -73,6 +79,7 @@ let generate_specs () =
let pre_analysis () =
floats_ok ();
options_ok ();
+ plugins_ok ();
Split_return.pretty_strategies ();
generate_specs ();
Widen.precompute_widen_hints ();
@@ -108,10 +115,10 @@ let post_analysis () =
(* Try to refine the 'Unknown' statuses that have been emitted during
this analysis. *)
Eval_annots.mark_green_and_red ();
- Eval_annots.mark_rte ();
+ Eva_dynamic.RteGen.mark_generated_rte ();
post_analysis_cleanup ~aborted:false;
(* Remove redundant alarms *)
- if Value_parameters.RmAssert.get () then !Db.Value.rm_asserts ()
+ if Value_parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ()
(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
analysis. Returns a function that restores previous signal behaviors after
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 5adf217e9f95053da29b3c13851e32527318dae4..3587497948dafbc7d40353138da1651a5b8202c2 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -227,9 +227,7 @@ let gui_compute_values (main_ui:main_ui) =
let cleaned_outputs kf s =
let outs = Db.Outputs.kinstr (Kstmt s) in
- let accept =
- Callgraph.Uses.accept_base ~with_formals:true ~with_locals:true kf
- in
+ let accept = Eva_dynamic.Callgraph.accept_base kf in
let filter = Locations.Zone.filter_base accept in
Option.map filter outs
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index cb3647e4fde810b6212ce0a8e0351d24e2ee3a2f..68aed0aadab7bc2b5171980bd0962f7b4f3e8c94 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -102,35 +102,6 @@ let mark_unreachable () =
Annotations.iter_all_code_annot do_code_annot;
Visitor.visitFramacFile unreach (Ast.get ())
-let mark_rte () =
- let _, mem, _ = !Db.RteGen.get_memAccess_status () in
- let _, arith, _ = !Db.RteGen.get_divMod_status () in
- let _, signed_ovf, _ = !Db.RteGen.get_signedOv_status () in
- let _, unsigned_ovf, _ = !Db.RteGen.get_unsignedOv_status () in
- let _, signed_downcast, _ = !Db.RteGen.get_signed_downCast_status () in
- let _, unsigned_downcast, _ = !Db.RteGen.get_unsignedDownCast_status () in
- let _, pointer_call, _ = !Db.RteGen.get_pointerCall_status () in
- let _, float_to_int, _ = !Db.RteGen.get_float_to_int_status () in
- let _, finite_float, _ = !Db.RteGen.get_finite_float_status () in
- let b_signed_ovf = Kernel.SignedOverflow.get () in
- let b_unsigned_ovf = Kernel.UnsignedOverflow.get () in
- let b_signed_downcast = Kernel.SignedDowncast.get () in
- let b_unsigned_downcast = Kernel.UnsignedDowncast.get () in
- Globals.Functions.iter
- (fun kf ->
- if !Db.Value.is_called kf then (
- mem kf true;
- arith kf true;
- pointer_call kf true;
- if b_signed_ovf then signed_ovf kf true;
- if b_unsigned_ovf then unsigned_ovf kf true;
- if b_signed_downcast then signed_downcast kf true;
- if b_unsigned_downcast then unsigned_downcast kf true;
- float_to_int kf true;
- finite_float kf true;
- )
- )
-
let c_labels kf cs =
if !Db.Value.use_spec_instead_of_definition kf then
Cil_datatype.Logic_label.Map.empty
diff --git a/src/plugins/value/legacy/eval_annots.mli b/src/plugins/value/legacy/eval_annots.mli
index 03fbb8c51541c594f3d7954bc53a77ce0460f303..ba43b7aa2f95bfa0d3198beef927964e5c40fb74 100644
--- a/src/plugins/value/legacy/eval_annots.mli
+++ b/src/plugins/value/legacy/eval_annots.mli
@@ -26,5 +26,4 @@ val has_requires: spec -> bool
val mark_invalid_initializers: unit -> unit
val mark_unreachable: unit -> unit
val mark_green_and_red: unit -> unit
-val mark_rte: unit -> unit
val c_labels: kernel_function -> Value_types.callstack -> Eval_terms.labels_states
diff --git a/src/plugins/value/utils/eva_dynamic.ml b/src/plugins/value/utils/eva_dynamic.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b62a8ec73cb2f5f61f8db4a83e434ccfcbc2f15b
--- /dev/null
+++ b/src/plugins/value/utils/eva_dynamic.ml
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* 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 ~plugin name typ ~fallback =
+ try Dynamic.get ~plugin name typ
+ with Failure _ | Dynamic.(Unbound_value _ | Incompatible_type _) -> fallback
+
+module Callgraph = struct
+ let plugin = "callgraph"
+
+ let iter_in_rev_order f =
+ let fallback = Globals.Functions.iter in
+ let typ = Datatype.(func (func Kernel_function.ty unit) unit) in
+ get ~plugin "iter_in_rev_order" typ ~fallback f
+
+ let accept_base kf v =
+ let fallback _ _ = true in
+ let typ = Datatype.(func2 Kernel_function.ty Base.ty bool) in
+ get ~plugin "accept_base" typ ~fallback kf v
+end
+
+module Scope = struct
+ let plugin = "scope"
+
+ let rm_asserts () =
+ let fallback () =
+ Value_parameters.warning
+ "The scope plugin is missing: cannot remove redundant alarms."
+ in
+ let typ = Datatype.(func unit unit) in
+ get ~plugin "rm_asserts" typ ~fallback ()
+end
+
+module RteGen = struct
+ let plugin = "RteGen"
+
+ let all_statuses () =
+ let kf = Kernel_function.ty in
+ let typ =
+ Datatype.(list (triple string (func2 kf bool unit) (func kf bool)))
+ in
+ get ~plugin "all_statuses" typ ~fallback:[]
+
+ let mark_generated_rte () =
+ let list = all_statuses () in
+ let mark kf = List.iter (fun (_kind, set, _get) -> set kf true) list in
+ Globals.Functions.iter (fun kf -> if !Db.Value.is_called kf then mark kf)
+end
diff --git a/src/plugins/value/utils/eva_dynamic.mli b/src/plugins/value/utils/eva_dynamic.mli
new file mode 100644
index 0000000000000000000000000000000000000000..85648b915300cf697ce591ed119e748edad837ff
--- /dev/null
+++ b/src/plugins/value/utils/eva_dynamic.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Access to other plugins API via {Dynamic.get}. *)
+
+module Callgraph: sig
+ (** Iterates over all functions in the callgraph in reverse order, i.e. from
+ callees to callers. If callgraph is missing, the order is unspecified. *)
+ val iter_in_rev_order: (Kernel_function.t -> unit) -> unit
+
+ (** Returns [true] if [base] is a global, or a formal or local of either [kf]
+ or one of its callers. If callgraph is missing, always returns true. *)
+ val accept_base: Kernel_function.t -> Base.t -> bool
+end
+
+module Scope: sig
+ (** Removes redundant assertions. Warns if the scope plugin is missing. *)
+ val rm_asserts: unit -> unit
+end
+
+module RteGen: sig
+ (** Marks all RTE as generated. Does nothing if the rte plugin is missing. *)
+ val mark_generated_rte: unit -> unit
+end
diff --git a/tests/value/memexec.c b/tests/value/memexec.c
index bb6bb912db9935c2a1a631b9b398d127236419f3..e87602726a13efd85890a02ab97e39e205d27042 100644
--- a/tests/value/memexec.c
+++ b/tests/value/memexec.c
@@ -1,7 +1,7 @@
/* run.config*
- STDOPT: +"-rte-select fbug @RTE_TEST@ -then -eva"
+ PLUGIN: @PTEST_PLUGIN@ rtegen
+ STDOPT: #"-machdep x86_32 -rte-select fbug @RTE_TEST@ -then -eva"
*/
-
int x1, y1, z1, z2; volatile int c, nondet;
void f11() {
diff --git a/tests/value/oracle/precond2.1.res.oracle b/tests/value/oracle/precond2.1.res.oracle
index ff415fa2c9b324a73cad48fbd8cc4917553d342a..4787a711af49ec5c93398aa4513386bbb9d207e3 100644
--- a/tests/value/oracle/precond2.1.res.oracle
+++ b/tests/value/oracle/precond2.1.res.oracle
@@ -35,8 +35,6 @@
x ∈ {1}
[eva:final-states] Values at end of function main:
x ∈ {0; 1}
-[rte:annot] annotating function f
-[rte:annot] annotating function main
[report] Computing properties status...
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 6faede6c061bc435ba56fa292654caf779bf975c..81eb244352197d5f99e3c7f35bb16ba46ccbe574 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -1,5 +1,3 @@
-[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
- Please use -eva-slevel instead.
[kernel] Parsing summary.i (no preprocessing)
[rte:annot] annotating function alarms
[rte:annot] annotating function bottom
@@ -8,6 +6,8 @@
[rte:annot] annotating function logic
[rte:annot] annotating function main
[rte:annot] annotating function minimal
+[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
+ Please use -eva-slevel instead.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -107,7 +107,7 @@
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
- by the Frama-C kernel: 0 errors 2 warnings
+ by the Frama-C kernel: 0 errors 3 warnings
----------------------------------------------------------------------------
18 alarms generated by the analysis:
3 invalid memory accesses
diff --git a/tests/value/oracle/unknown_sizeof.0.res.oracle b/tests/value/oracle/unknown_sizeof.0.res.oracle
index b106b41c0ed6f8b83419377598478fedd74bcbfe..4244ff0a82bf4d678680de7005b49eb33ba7e264 100644
--- a/tests/value/oracle/unknown_sizeof.0.res.oracle
+++ b/tests/value/oracle/unknown_sizeof.0.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing unknown_sizeof.i (no preprocessing)
+[eva] Warning: The inout plugin is missing: some features are disabled, and the analysis may have degraded precision and performance.
[eva] Analyzing a complete application starting at main1
[eva] Computing initial state
[eva:unknown-size] unknown_sizeof.i:8: Warning:
diff --git a/tests/value/oracle/unknown_sizeof.1.res.oracle b/tests/value/oracle/unknown_sizeof.1.res.oracle
index 52d022abfce0070deb7ef6ef3f21e519c7411d0a..fd9e82d2f78f1e71419051cac7ceafad4710390f 100644
--- a/tests/value/oracle/unknown_sizeof.1.res.oracle
+++ b/tests/value/oracle/unknown_sizeof.1.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing unknown_sizeof.i (no preprocessing)
+[eva] Warning: The inout plugin is missing: some features are disabled, and the analysis may have degraded precision and performance.
[eva] Analyzing a complete application starting at main2
[eva] Computing initial state
[eva:unknown-size] unknown_sizeof.i:8: Warning:
diff --git a/tests/value/summary.i b/tests/value/summary.i
index 718f105808a8e7a74784f387e3945490e35f5f0b..3ef6022672e965f17208f8baaf7385d8cfc54c8b 100644
--- a/tests/value/summary.i
+++ b/tests/value/summary.i
@@ -3,8 +3,8 @@
STDOPT: +"-eva-msg-key=summary -main minimal"
STDOPT: +"-eva-msg-key=summary -main bottom"
STDOPT: +"-eva-msg-key=summary -main main"
-PLUGIN: @PTEST_PLUGIN@ rtegen
- STDOPT: +"@RTE_TEST@ -eva-msg-key=summary -main main -slevel 0"
+ PLUGIN: @PTEST_PLUGIN@ rtegen
+ OPT: -machdep x86_32 @RTE_TEST@ -then @EVA_TEST@ -eva-msg-key=summary -main main -slevel 0
*/
/* Tests the summary on the smallest possible program. */
void minimalist ();