diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml index 18befa2c68690b2f7e426867f0c1a63a1e890d30..31d72c55b6c13236a81db8d688cbeae9e8cac3fa 100644 --- a/src/kernel_services/abstract_interp/cvalue.ml +++ b/src/kernel_services/abstract_interp/cvalue.ml @@ -1058,6 +1058,11 @@ module Model = struct let v = find_indeterminate ~conflate_bottom state loc in V_Or_Uninitialized.get_v v + let add_binding ~exact mem loc v = + if V_Or_Uninitialized.is_bottom v + then bottom + else add_binding ~exact mem loc v + let add_indeterminate_binding ~exact mem loc v = add_binding ~exact mem loc v diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml index 260ec8ebaeff92d55cf15d53c03d402aa9e19fdb..55a15a5e78e37c7312a55f1f93e6d22482141606 100644 --- a/src/kernel_services/abstract_interp/lmap.ml +++ b/src/kernel_services/abstract_interp/lmap.ml @@ -656,17 +656,14 @@ struct | Map m -> Map (M.add_base_value base ~size v ~size_v m) let add_binding ~exact m loc v = - (* TODO: this should depend on bottom being strict. *) - if V.equal v V.bottom then Bottom - else - match m with - | Top -> Top - | Bottom -> Bottom - | Map m -> - try - let non_bottom, r = M.add_binding ~exact m loc v in - if non_bottom then Map r else Bottom - with M.Result_is_top -> Top + match m with + | Top -> Top + | Bottom -> Bottom + | Map m -> + try + let non_bottom, r = M.add_binding ~exact m loc v in + if non_bottom then Map r else Bottom + with M.Result_is_top -> Top let find ?(conflate_bottom=true) m loc = match m with