From 43ade27f76c1c7a416bb2178d931e3bd1fdc2cce Mon Sep 17 00:00:00 2001
From: Shuvendu Lahiri <shuvendu@microsoft.com>
Date: Wed, 18 Jul 2018 00:31:32 -0700
Subject: [PATCH] fix to Corral to instrument user defined types such as ref

---
 .../propinst-regressions/rodrigo_refnull.bpl  |  9 ++++++++
 .../ExampleProperties/nullcheck-csharp.avp    | 21 +++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 AddOns/AngelicVerifierNull/test/propinst-regressions/rodrigo_refnull.bpl
 create mode 100644 AddOns/PropInst/PropInst/ExampleProperties/nullcheck-csharp.avp

diff --git a/AddOns/AngelicVerifierNull/test/propinst-regressions/rodrigo_refnull.bpl b/AddOns/AngelicVerifierNull/test/propinst-regressions/rodrigo_refnull.bpl
new file mode 100644
index 000000000..3c24e6492
--- /dev/null
+++ b/AddOns/AngelicVerifierNull/test/propinst-regressions/rodrigo_refnull.bpl
@@ -0,0 +1,9 @@
+type Ref;
+
+const unique null : Ref;
+var r: Ref;
+
+procedure Foo() {
+  r := null;
+  assume {:nonnull} r != null;
+}
diff --git a/AddOns/PropInst/PropInst/ExampleProperties/nullcheck-csharp.avp b/AddOns/PropInst/PropInst/ExampleProperties/nullcheck-csharp.avp
new file mode 100644
index 000000000..5658d2510
--- /dev/null
+++ b/AddOns/PropInst/PropInst/ExampleProperties/nullcheck-csharp.avp
@@ -0,0 +1,21 @@
+GlobalDeclarations
+{
+function {:inline} {:aliasingQuery} {:mkUniqueFn} aliasQ(p:Ref, q:Ref) returns (bool) { p == q }
+}
+
+
+TemplateVariables
+{
+var p : Ref;
+}
+
+
+//Check every dereference
+CmdRule
+{
+  assume {:nonnull} p != null;
+}
+-->
+{
+  assert p != null;
+}
\ No newline at end of file