Skip to content

Commit

Permalink
fixup labels under the "Split Analysis" heading
Browse files Browse the repository at this point in the history
No need to manually tag the nodes with "Original" and "Patched";
they will already be labelled as such since they are single-sided
nodes created from toSingleNode
  • Loading branch information
danmatichuk committed Feb 23, 2024
1 parent 0af41e3 commit 1ee0b90
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Pate/Verification/StrongestPosts.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2406,7 +2406,7 @@ handleSplitAnalysis scope node dom pg = do
currBlockO <- toSingleNode PBi.OriginalRepr node
currBlockP <- toSingleNode PBi.PatchedRepr node
subTree @"node" "Split analysis" $ do
pg' <- subTraceLabel @"node" "Original:" (GraphNode currBlockO) $ do
pg' <- subTrace @"node" (GraphNode currBlockO) $ do
priority <- thisPriority
emitTraceLabel @"address" "Synchronization Address" syncO
bundleO <- noopBundle scope (nodeBlocks currBlockO)
Expand All @@ -2416,7 +2416,7 @@ handleSplitAnalysis scope node dom pg = do
-- by convention, we define the sync point of the original program to
-- connect to the divergence point of the patched program
widenAlongEdge scope bundleO (GraphNode node) dom pg (GraphNode currBlockO)
subTraceLabel @"node" "Patched" (GraphNode currBlockP) $ do
subTrace @"node" (GraphNode currBlockP) $ do
emitTraceLabel @"address" "Synchronization Address" syncP
return $ Just pg'
Left{} -> return Nothing
Expand Down

0 comments on commit 1ee0b90

Please sign in to comment.