From 40a905151afd5876a4d9602b45c022428798bb13 Mon Sep 17 00:00:00 2001
From: BigGan <784810497@qq.com>
Date: Mon, 20 Jul 2020 15:13:01 +0800
Subject: [PATCH] =?UTF-8?q?the=20function=20TranslateCallStatement=20(=20N?=
 =?UTF-8?q?ULL=C2=A0Pointer=C2=A0Dereference=20)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

In the function TranslateCallStatement (Sources/SolToBoogie/ProcedureTranslator.cs), the parameter outParams may be null. However, This code BoogieIdentifierExpr tmpVarExpr = outParams[0]; will call directly outParams[0] without judging whether the outParams is null.

Test Case( Test.sol ):

pragma solidity >=0.4.20;
contract Test {
  function BugTest() public  {
      msg.sender.call.value(123)("");
  }
}
---
 Sources/SolToBoogie/ProcedureTranslator.cs | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/Sources/SolToBoogie/ProcedureTranslator.cs b/Sources/SolToBoogie/ProcedureTranslator.cs
index 00ac9b07..8a91a94d 100644
--- a/Sources/SolToBoogie/ProcedureTranslator.cs
+++ b/Sources/SolToBoogie/ProcedureTranslator.cs
@@ -2674,13 +2674,21 @@ private void TranslateCallStatement(FunctionCall node, List<BoogieIdentifierExpr
                 currentStmtList.AddStatement(new BoogieSkipCmd(node.ToString()));
                 VeriSolAssert(false, "low-level call statements with non-empty signature not implemented..");
             }
-
-            // almost identical to send(amount)
-            BoogieIdentifierExpr tmpVarExpr = outParams[0]; //bool part of the tuple
-            if (tmpVarExpr == null)
+						
+			BoogieIdentifierExpr tmpVarExpr;
+            if (null == outParams)
             {
                 tmpVarExpr = MkNewLocalVariableWithType(BoogieType.Bool);
             }
+            else
+            {
+                // almost identical to send(amount)
+                tmpVarExpr = outParams[0]; //bool part of the tuple
+                if (null == tmpVarExpr)
+                {
+                    tmpVarExpr = MkNewLocalVariableWithType(BoogieType.Bool);
+                }
+            }		
 
             var amountExpr = node.MsgValue != null ? TranslateExpr(node.MsgValue) : new BoogieLiteralExpr(BigInteger.Zero);
             TranslateSendCallStmt(node, tmpVarExpr, amountExpr, true);