fix: memhavoc should be mem def

seahorn · Sep 19, 2023 · 910fa15 · 910fa15
1 parent 8fc33bd
commit 910fa15
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/lib/seadsa/ShadowMem.cc b/lib/seadsa/ShadowMem.cc
@@ -1251,9 +1251,10 @@ void ShadowMemImpl::visitMemhavoc(CallBase &I) {
   }
 
   m_B->SetInsertPoint(&I);
-  CallInst &memUse =
-      mkShadowLoad(*m_B, cell, dsa::getTypeSizeInBytes(*ptr.getType(), *m_dl));
-  associateConcretePtr(memUse, ptr, &I);
+  CallInst &memDef = mkShadowStore(
+      *m_B, cell,
+      dsa::getTypeSizeInBytes(*ptr.getType(), *m_dl) /* bytes to access */);
+  associateConcretePtr(memDef, ptr, &I);
 }
 
 void ShadowMemImpl::visitIsModified(CallBase &I) {