more commits related to the fix

boogie-org · Jul 18, 2018 · 0367812 · 0367812
1 parent 43ade27
commit 0367812
Show file tree

Hide file tree

Showing 3 changed files with 58 additions and 52 deletions.
diff --git a/AddOns/AngelicVerifierNull/test/propinst-regressions/Answer b/AddOns/AngelicVerifierNull/test/propinst-regressions/Answer
@@ -1,50 +1,55 @@
-
--------------------- uaf0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-
--------------------- uaf1.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf1_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-
--------------------- df0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing df0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-
--------------------- uaf2.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf2_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
-
--------------------- uaf3.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf3_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
-
--------------------- irql0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing irql0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 2)
-
--------------------- irql1.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing irql1_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 1)
-
--------------------- irql2.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing irql2_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int, x_2: int :: unknownTrigger_0(x_1) && unknownTrigger_1(x_2) ==> x_1 <= x_2)
-
--------------------- null0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing null0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr !(ax == NULL)
+
+-------------------- uaf0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+
+-------------------- uaf1.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf1_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+
+-------------------- df0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing df0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+
+-------------------- uaf2.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf2_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
+
+-------------------- uaf3.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf3_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
+
+-------------------- irql0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing irql0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 2)
+
+-------------------- irql1.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing irql1_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 1)
+
+-------------------- irql2.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing irql2_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int, x_2: int :: unknownTrigger_0(x_1) && unknownTrigger_1(x_2) ==> x_1 <= x_2)
+
+-------------------- null0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing null0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr !(ax == NULL)
+
+-------------------- rodrigo_refnull.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing rodrigo_refnull_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc Foo with expr r != null
diff --git a/AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat b/AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat
@@ -18,6 +18,7 @@ call:add irql0.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle
 call:add irql1.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle.avp
 call:add irql2.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle.avp
 call:add null0.bpl ..\..\..\PropInst\PropInst\ExampleProperties\nullcheck-razzle.avp
+call:add rodrigo_refnull.bpl ..\..\..\PropInst\PropInst\ExampleProperties\nullcheck-csharp.avp
 
 REM for %%f in (eeSlice3.bpl) do (
 set i=0

diff --git a/source/Util/Visitor.cs b/source/Util/Visitor.cs
@@ -1294,7 +1294,7 @@ public override Expr VisitNAryExpr(NAryExpr node)
  var nodeFunc = ((FunctionCall)node.Fun).Func;
  for (var i = 0; i < tcFunc.InParams.Count; i++)
  {
- if (!Equals(tcFunc.InParams[i].TypedIdent.Type, nodeFunc.InParams[i].TypedIdent.Type))
+ if (!Equals(tcFunc.InParams[i].TypedIdent.Type.ToString(), nodeFunc.InParams[i].TypedIdent.Type.ToString()))
  {
  Matches = false;
  return base.VisitNAryExpr(node);
@@ -1355,7 +1355,7 @@ public override Expr VisitIdentifierExpr(IdentifierExpr node)
 
  if (idexToConsume.Decl != null)
  {
- if (Equals(node.Decl.TypedIdent.Type, idexToConsume.Decl.TypedIdent.Type)
+ if (Equals(node.Decl.TypedIdent.Type.ToString(), idexToConsume.Decl.TypedIdent.Type.ToString())
  && AreAttributesASubset(idexToConsume.Decl.Attributes, node.Decl.Attributes))
  {
  Substitution.Add(idexToConsume.Decl, node);