File tree 2 files changed +5
-4
lines changed
src/SAWScript/Crucible/LLVM
2 files changed +5
-4
lines changed Original file line number Diff line number Diff line change @@ -641,7 +641,7 @@ verifyObligations cc mspec tactic assumes asserts =
641
641
{ goalNum = n
642
642
, goalType = " vc"
643
643
, goalName = nm
644
- , goalLoc = show ploc
644
+ , goalLoc = show ( W4. plSourceLoc ploc) ++ " in " ++ show ( W4. plFunction ploc)
645
645
, goalDesc = msg
646
646
, goalProp = goal'
647
647
}
@@ -811,6 +811,7 @@ assumptionsContainContradiction cc methodSpec tactic assumptions =
811
811
let sym = cc^. ccSym
812
812
st <- io $ Common. sawCoreState sym
813
813
let sc = saw_ctx st
814
+ let ploc = methodSpec^. MS. csLoc
814
815
pgl <- io $
815
816
do
816
817
-- conjunction of all assumptions
@@ -822,7 +823,7 @@ assumptionsContainContradiction cc methodSpec tactic assumptions =
822
823
{ goalNum = 0
823
824
, goalType = " vacuousness check"
824
825
, goalName = show (methodSpec^. MS. csMethod)
825
- , goalLoc = show (methodSpec ^. MS. csLoc )
826
+ , goalLoc = show (W4. plSourceLoc ploc) ++ " in " ++ show ( W4. plFunction ploc )
826
827
, goalDesc = " vacuousness check"
827
828
, goalProp = goal'
828
829
}
Original file line number Diff line number Diff line change @@ -1374,12 +1374,12 @@ matchTerm sc cc loc prepost real expect =
1374
1374
_ ->
1375
1375
do t <- liftIO $ scEq sc real expect
1376
1376
let msg = unlines $
1377
- [ " Literal equality " ++ stateCond prepost ++ " at " ++ show loc
1377
+ [ " Literal equality " ++ stateCond prepost
1378
1378
-- , "Expected term: " ++ prettyTerm expect
1379
1379
-- , "Actual term: " ++ prettyTerm real
1380
1380
]
1381
1381
addTermEq t $ Crucible. SimError loc $ Crucible. AssertFailureSimError msg " "
1382
- where prettyTerm = show . ppTermDepth 20
1382
+ -- where prettyTerm = show . ppTermDepth 20
1383
1383
1384
1384
1385
1385
------------------------------------------------------------------------
You can’t perform that action at this time.
0 commit comments