diff --git a/Makefile b/Makefile index c4185f9379adc3ba190abf24083fada13956da0a..9ef3420063a5513f1bfd5d88ed0d0966ddc315bd 100644 --- a/Makefile +++ b/Makefile @@ -891,7 +891,6 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \ domains/sign_domain \ domains/cvalue/warn domains/cvalue/locals_scoping \ domains/cvalue/cvalue_offsetmap \ - utils/eva_results \ utils/summary \ domains/cvalue/builtins domains/cvalue/builtins_malloc \ domains/cvalue/builtins_string domains/cvalue/builtins_misc \ @@ -904,6 +903,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \ domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \ domains/cvalue/cvalue_specification \ domains/cvalue/cvalue_domain \ + utils/eva_results \ partitioning/auto_loop_unroll \ partitioning/partition partitioning/partitioning_parameters \ partitioning/partitioning_index partitioning/trace_partitioning \ diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml index de214be4544168e7d7a87d7017c4f4602a5f6de8..f65cbc8046a1e3b3ea8488465e5b83e8f4eae0ef 100644 --- a/src/plugins/value/domains/cvalue/cvalue_domain.ml +++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml @@ -456,7 +456,7 @@ module State = struct let default () = false end) - let register_global_state _ _ = Storage.set true + let register_global_state b _ = Storage.set b let register_initial_state callstack (state, _clob) = Db.Value.merge_initial_state callstack state let register_state_before_stmt callstack stmt (state, _clob) = diff --git a/src/plugins/value/utils/eva_results.ml b/src/plugins/value/utils/eva_results.ml index 07c6fa00638dcd8c96849ad9ef72dae8b2329417..266589b752a99adadbf133b3d3825a6b9b096e56 100644 --- a/src/plugins/value/utils/eva_results.ml +++ b/src/plugins/value/utils/eva_results.ml @@ -253,6 +253,10 @@ let set_results results = Property_status.emit Eva_utils.emitter ~hyps:[] ip st in Property.Hashtbl.iter aux_statuses results.statuses; + let b = Parameters.ResultsAll.get () in + Cvalue_domain.State.Store.register_global_state b + (`Value Cvalue_domain.State.top); + Self.set_computation_state Computed; Db.Value.mark_as_computed (); ;;