From cf0e50fe8faf2d1e3d842d059f5d33fc5068c932 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 14 Apr 2016 15:04:22 -0700 Subject: [PATCH] Allow `llvm_assert_eq` to apply to arguments --- src/SAWScript/LLVMMethodSpec.hs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/SAWScript/LLVMMethodSpec.hs b/src/SAWScript/LLVMMethodSpec.hs index b2e4826d70..59beb71b27 100644 --- a/src/SAWScript/LLVMMethodSpec.hs +++ b/src/SAWScript/LLVMMethodSpec.hs @@ -441,10 +441,12 @@ initializeVerification' sc ir = do -- until later to initialize the fields. argAssignments' <- forM argAssignments $ \(expr, mle) -> case (expr, mle) of - (CC.Term (TC.Arg _ _ _), Just _) -> - fail "argument assignments not allowed" + (CC.Term (TC.Arg _ _ _), Just le) -> do + ps <- fromMaybe (error "initializeVerification: arg with value") <$> getPath + tm <- useLogicExprPS ir sc ps [] le + return (Just (expr, tm)) (CC.Term (TC.Arg _ _ ty), Nothing) -> do - ps <- fromMaybe (error "initializeVerification") <$> getPath + ps <- fromMaybe (error "initializeVerification: arg w/o value") <$> getPath (tm, ps') <- liftIO $ createLogicValue cb sbe sc expr ps ty mle setPS ps' return (Just (expr, tm))