Skip to content

Commit

Permalink
Loosen Crucible/LLVM override return type check
Browse files Browse the repository at this point in the history
This is a spot fix. The check we have right now is too strict, it won't even let
you specify that a function returns `crucible_null`.

See #443, which we should leave open until we implement the proper check
described there.
  • Loading branch information
langston-barrett committed May 24, 2019
1 parent 7191a6a commit a88c6f4
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/SAWScript/CrucibleBuiltins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -380,8 +380,9 @@ checkSpecReturnType cc mspec =
(csAllocations mspec) -- map allocation indices to allocations
(mspec^.csPreState.csVarTypeNames) -- map alloc indices to var names
sv
-- The following check is even more strict than checkRegisterCompatibility
unless (retTy == retTy') $ fail $ unlines
-- This check is too lax, see saw-script#443
b <- checkRegisterCompatibility retTy retTy'
unless b $ fail $ unlines
[ "Incompatible types for return value when verifying " ++ mspec^.csName
, "Expected: " ++ show retTy
, "but given value of type: " ++ show retTy'
Expand Down

0 comments on commit a88c6f4

Please sign in to comment.