Allow llvm_assert_eq to apply to arguments

GaloisInc · Apr 14, 2016 · cf0e50f · cf0e50f
1 parent 5291c25
commit cf0e50f
Showing 1 changed file with 5 additions and 3 deletions.
diff --git 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))