commit dab5664b4d840488a40db59c278e217bd02ff80e
author Martin Brænne <mboehme@google.com> Tue Oct 31 10:45:40 2023 -0700
committer Copybara-Service <copybara-worker@google.com> Tue Oct 31 10:46:23 2023 -0700
tree cb7e6772bc6a6c0aeb15a617a888b1092dd79254
parent 5392b47f7f17e049c041af9a806d9aa79243c8af

[nullability] Use `proves()` and `assume()` instead of deprecated synonyms.

Somehow, these slipped through the cracks when I did the earlier migration.

PiperOrigin-RevId: 578233748
Change-Id: I97566926693ab707a5565c22c389066dbc491c4f

nullability/pointer_nullability_analysis.cc

diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc
index cab631f..1f7f6e7 100644
--- a/nullability/pointer_nullability_analysis.cc
+++ b/nullability/pointer_nullability_analysis.cc
@@ -294,10 +294,8 @@
   assert(NewNullability.IsNull != nullptr);
 
   if (FromNullable != nullptr)
-    Env.addToFlowCondition(
-        A.makeEquals(*NewNullability.FromNullable, *FromNullable));
-  if (Null != nullptr)
-    Env.addToFlowCondition(A.makeEquals(*NewNullability.IsNull, *Null));
+    Env.assume(A.makeEquals(*NewNullability.FromNullable, *FromNullable));
+  if (Null != nullptr) Env.assume(A.makeEquals(*NewNullability.IsNull, *Null));
 
   return &NewPointerVal;
 }
@@ -1064,10 +1062,10 @@
 
   Arena &A = CurEnv.arena();
 
-  if (PrevEnv.flowConditionImplies(*Prev)) {
-    if (CurEnv.flowConditionImplies(*Cur)) return Cur;
-  } else if (PrevEnv.flowConditionImplies(A.makeNot(*Prev)) &&
-             CurEnv.flowConditionImplies(A.makeNot(*Cur))) {
+  if (PrevEnv.proves(*Prev)) {
+    if (CurEnv.proves(*Cur)) return Cur;
+  } else if (PrevEnv.proves(A.makeNot(*Prev)) &&
+             CurEnv.proves(A.makeNot(*Cur))) {
     return Cur;
   }
 
@@ -1119,13 +1117,12 @@
 
     auto &A = CurrentEnv.arena();
     if (FromNullableWidened != nullptr)
-      CurrentEnv.addToFlowCondition(
+      CurrentEnv.assume(
           A.makeEquals(*WidenedNullability.FromNullable, *FromNullableWidened));
     else
       forgetFromNullable(WidenedPtr, DACtx);
     if (NullWidened != nullptr)
-      CurrentEnv.addToFlowCondition(
-          A.makeEquals(*WidenedNullability.IsNull, *NullWidened));
+      CurrentEnv.assume(A.makeEquals(*WidenedNullability.IsNull, *NullWidened));
     else
       forgetIsNull(WidenedPtr, DACtx);