AV: Fix to null dereference. Fixes boogie-org#71.

rcastano · Jul 25, 2018 · 34abe74 · 34abe74
1 parent 38aeb6e
commit 34abe74
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/AddOns/AngelicVerifierNull/test/avn-regressions/Answer b/AddOns/AngelicVerifierNull/test/avn-regressions/Answer
@@ -107,4 +107,4 @@
 
 -------------------- type_alias.bpl --------------------
 [TAG: AV_OUTPUT] ----- Analyzing type_alias_hinst.bpl ------
-[TAG: AV_OUTPUT] AngelicVerifier failed with: Object reference not set to an instance of an object.
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> m[x_1] != r1)
diff --git a/AddOns/AngelicVerifierNull/test/avn-regressions/type_alias.bpl b/AddOns/AngelicVerifierNull/test/avn-regressions/type_alias.bpl
@@ -4,8 +4,8 @@ type Ref = Union;
 
 const unique r1 : Ref;
 const unique null : Ref;
-var m : [Ref] Ref;
+var m : [int] Ref;
 
-procedure Foo(r : Ref) {
+procedure Foo(r : int) {
   assert m[r] != r1;
 }
diff --git a/source/CoreLib/SdvUtils.cs b/source/CoreLib/SdvUtils.cs
@@ -268,7 +268,7 @@ private CallCmd makeRecordCall(IdentifierExpr v)
                 return new CallCmd(Token.NoToken, recordProcNameBool, ins, new List<IdentifierExpr>());
             else if (v.Type.IsCtor)
             {
-                var t = (v.Type as CtorType).Decl.Name;
+                var t = v.Type.AsCtor.Decl.Name;
                 if (!typeToRecordProc.ContainsKey(t))
                 {
                     var inpVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", v.Type), true);