From dc2108e579de340cb4c60f3dde67e5ba6e619406 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 19 Jun 2020 09:19:21 -0700
Subject: [PATCH] Add regression test for issue #642.

---
 intTests/test_issue642/Makefile |   2 ++
 intTests/test_issue642/test.bc  | Bin 0 -> 2720 bytes
 intTests/test_issue642/test.c   |  11 ++++++++++
 intTests/test_issue642/test.saw |  37 ++++++++++++++++++++++++++++++++
 intTests/test_issue642/test.sh  |   1 +
 5 files changed, 51 insertions(+)
 create mode 100644 intTests/test_issue642/Makefile
 create mode 100644 intTests/test_issue642/test.bc
 create mode 100644 intTests/test_issue642/test.c
 create mode 100644 intTests/test_issue642/test.saw
 create mode 100644 intTests/test_issue642/test.sh

diff --git a/intTests/test_issue642/Makefile b/intTests/test_issue642/Makefile
new file mode 100644
index 0000000000..977e89a70a
--- /dev/null
+++ b/intTests/test_issue642/Makefile
@@ -0,0 +1,2 @@
+test.bc : test.c
+	clang -c -emit-llvm -g -o test.bc test.c
diff --git a/intTests/test_issue642/test.bc b/intTests/test_issue642/test.bc
new file mode 100644
index 0000000000000000000000000000000000000000..417112c9381b91e313a7a89058502ea859817559
GIT binary patch
literal 2720
zcmaJ?eN0=|6~B*Xd|!ewc48H?y!Y}9EOoaA9(Hg{44c7OLOP-uE$LFNDK?3T+4wNF
z>kk@j&)ChQ9e+41Ydxu|>?xhn?H|%cQMN{vF@zz{i)a?L2q6>}icpqCtj)A^tJa-s
zV2!kC*E;W<d+)jDo^$T`9WP}o%Mc75P+~hm7$K_7kzHzp1&~p<O00eDwO_vV_m6&j
z^p97%KKjO+|NQJbWt~z7g^)poP-_W7WhDj#4DAHMv6}O(vx*~1jj3szN~peC%2e@+
zpL9!_Z<Vx-m$fA{CY_bhe|x*BZL~e96C8&|-$GTUHpLNjQd>RkZ0(GVEyq88Rbe=!
z?9?OlHrU+t!jq4_fI<1tHY07PbCO;TCvns$52bNvR<<PN@Fg4;WWOL=1UWb%2SN76
zqoX*QmMtQVc;g`k58H8;&BeIY42wqCTW&tr%Fbul1&PlYxcN-^jDekpT}qUFE;(w%
zl1uid<fxa9BxS!|4yM2+9gt)&<wpfjcJp~kSX|~7vh0e1T>w*vUovouF+ShQFQnOd
z1Ghk>arBbxN6K)7coJpgkWscsa=0Cb)3QG)TZ}l=E{D8yID*4o8g_jmmV9#98xQ($
zAoaif&v8qc^4l4Hf#Qk(#XuhOoE)da3=aRl<EsYl<|LPou?zOy;P8^0hd}OR$`=gm
z8pWXigF_H9Vu<Gu1%o4!9Q4V7|4L>zzh+=(+#H0zvdpbz*qIo=1R1ci_a@mwhF!^&
z!(9&{?ahc8W^mLh`{7;mIC2RiK0nE=7<MmG0vK6YX7e%PMjm{~@GBX1l{yh0%F5OW
z+H!&pWaVfQTTaA7UVPRSZ%oNPI}Q{DcrRFwg2PGBEDEVDAx-Ze-ISqbnm|8`o3GIl
z)C^b<H=otwm3?U({PJb*!TW;e%Uq%8()==)i}C+Si$%zhnyio%PCJLt5vbK721Z<M
z0@Um)@KFOdRWsX!(=RJ_R$olO=WZgC)a~dP9V<&DIy7QH;j%jw%(zyHNo~&K=YNKn
zr&gJwoqcDswCz!;EgiRz%wtkE;2~6g3ZEUNt-iQ5Memp5<sPTHe@;ETuI^8&Lv}pu
z!ofM^s)Qk!Apu9`ln*34tiho)4hWmO?`p7L!p~GN+8y?DV>&IhuTB49is}8Nv_!*{
z4v!vGfeQfejp4XRn<S*!n(C`h(j~~gHI=57vD{(Me@-C%!o;UERoaf^*tR`~XB3VR
ztyFDHn2a$$>|KT&1%aCxiJe|%dvsLGsKc6=8f%kqGy=6gq*_H4f6=HPN@}yJjn7ST
zH#2OHSXxwz?<&wOvyPTAx}^{q18lqmmDDc#e0bPLha$31kgEz>_5GxJS*#ckEAFnV
z*PUv!W|~_9tQxqSo9_`{v0abb<{V8|=;rJ3<^*jktm{H9{E`>%_d*@u{gUiU0{$W0
zIP|C#%!Vboi;;))#a@t#J^f%^{os!JZ&~$yk?x))#l2DD?4p}g?R1RGyOkd%9Zj>2
zrd08JZOVGVVI8Gy7pCgr($7b1w`tqNl<IfAvhRfK_r-%=9C67(XfbKI>gIPV9-xX(
zoa&XN`mViVSy11HC<G(7I0-oCZy8wVFN=2oD%?Ga@6mT!CmaXfh}#Oz+RZ>*GPIIN
zs<Y!^vVvrQ{{f$Ovug%!X_EU9ML<<BaO-a6v6ti4!jx^o(E<tiJlDM9u#LiWYV5{#
z8GsZ9f1qg^u|E}i{;o!SKdb)Oss2=~nY`5sIIjdeEKxiugQ$Se3&6YicEK^Ks%omL
zO`f;U%+7kNos7=(roPH>csAMDk$MlIbGxrm4g1E&$+@5>5Ue{@e>~vv2kN~q_Vo0-
z2kO5!=>K7Tz#ZNjIOXs41?zhUg2zBFP*1eG`ualsU1$0RyWM?V?!I1kpw;K=^9UUs
z&mI**V5WC)Kxh!_;3pVQ^|=Sm>}?Q5v96(^ZeL?v<5T1$7(5tu`+J0EH}nsBx?ema
z92w{t+*%2r^1A(9f!<+{^N2&}@Ps^lsD`mOj39jtlLaQg%(TmFS7^$g09=T-b>asQ
zkER_tDF8~=UaDb`NQ)<39aXBV`41ZBr+QSSb0M8s_3Gt<XvF5JIpO!J_)m>yMSM)L
z$5?5xyl1I2T{gdd`L~@TPu7s>>sR-`bKt6}(tLH|-QRRFf6l#gY<~X!!t=Lg^NVYT
zwp}sADYS>=@om5r`4cbO?l(fc;^7m%l%oa8Zo<(tH#M@#&Sc8hS_zz>4R6!|`T+b^
z!Wmp>z8JT?0mVtTq~py{sL3gUe7Atm*MaX;v^K-vJlX+NO<r-kqQn7m&){I>*S|9S
zNxH<)f)N(9(EhfeCmORfLarETVH2$r?;lMdi4yCy*XzFaK0<q#JlQa7DJhwoptOua
z?DipnQJ(w7zo3^+{ev`A^7&>#ueouT(kXu4AgFH8=XQ-KRXr*u{#U6?*rSq&>{yp1
zh@1HOeMK5B-SD{*_?FKkCq<u?(-cwYcKcD$XX9s*Kn@BhiChj>f3<>mjcSyoXv8Jd
z=EtZ^Eti}G#&8-9y>W+Bykkf}hzKUNraD2z6xKV>zziV|B&iYj4*J3+qEF~6KqSWp
zH|I{^WDu?ZngAkt0ua$X07Uc&mbM1bBf}0vWJ2VANYWRmcEh$7=A`#(HrJV_5jqYs
z(IxqKT>m+kmjaPN_KBTZ5Qt1@>+UTMOXwuTwhK7K29JmkK@q$^!D8L%?lX0#JpeVo
y2hzI%y@=J)W!bmaO`y5A-+gK@5P^*bbDg+>_%1kHMDpXOyWn^c+2n>V$G-u^SXK7`

literal 0
HcmV?d00001

diff --git a/intTests/test_issue642/test.c b/intTests/test_issue642/test.c
new file mode 100644
index 0000000000..cd8bb7a6a5
--- /dev/null
+++ b/intTests/test_issue642/test.c
@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+int glob;
+
+int foo (int *x) {
+	return (x == &glob);
+}
+
+int bar () {
+	return foo(&glob);
+}
diff --git a/intTests/test_issue642/test.saw b/intTests/test_issue642/test.saw
new file mode 100644
index 0000000000..b570d50941
--- /dev/null
+++ b/intTests/test_issue642/test.saw
@@ -0,0 +1,37 @@
+// This test checks whether we can use an override with a pointer
+// argument that aliases a global. It is a regression test for
+// saw-script issue #642.
+// https://github.com/GaloisInc/saw-script/issues/642
+
+bc <- llvm_load_module "test.bc";
+
+let i32 = llvm_int 32;
+
+foo_ov <-
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      crucible_alloc_global "glob";
+      x <- crucible_alloc i32;
+      crucible_execute_func [x];
+      crucible_return (crucible_term {{ 0 : [32] }});
+    }
+    z3;
+
+bar_ov1 <-
+  crucible_llvm_verify bc "bar" [] false
+    do {
+      crucible_alloc_global "glob";
+      crucible_execute_func [];
+      crucible_return (crucible_term {{ 1 : [32] }});
+    }
+    z3;
+
+fails (
+  crucible_llvm_verify bc "bar" [foo_ov] false
+    do {
+      crucible_alloc_global "glob";
+      crucible_execute_func [];
+      crucible_return (crucible_term {{ 0 : [32] }});
+    }
+    z3
+  );
diff --git a/intTests/test_issue642/test.sh b/intTests/test_issue642/test.sh
new file mode 100644
index 0000000000..0b864017cd
--- /dev/null
+++ b/intTests/test_issue642/test.sh
@@ -0,0 +1 @@
+$SAW test.saw