From e54bc4765e79734b311272febcdebbc7b96711e2 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 31 Aug 2017 16:32:16 +0100
Subject: [PATCH] Tests for unique java bytecode instrumentation selection

---
 regression/cbmc-cover/unique-bytecode1/Test.class | Bin 0 -> 301 bytes
 regression/cbmc-cover/unique-bytecode1/Test.java  |   6 ++++++
 regression/cbmc-cover/unique-bytecode1/test.desc  |   7 +++++++
 regression/cbmc-cover/unique-bytecode2/Test.class | Bin 0 -> 262 bytes
 regression/cbmc-cover/unique-bytecode2/Test.java  |   3 +++
 regression/cbmc-cover/unique-bytecode2/test.desc  |   8 ++++++++
 regression/cbmc-cover/unique-bytecode3/Test.class | Bin 0 -> 292 bytes
 regression/cbmc-cover/unique-bytecode3/Test.java  |   4 ++++
 regression/cbmc-cover/unique-bytecode3/test.desc  |   9 +++++++++
 9 files changed, 37 insertions(+)
 create mode 100644 regression/cbmc-cover/unique-bytecode1/Test.class
 create mode 100644 regression/cbmc-cover/unique-bytecode1/Test.java
 create mode 100644 regression/cbmc-cover/unique-bytecode1/test.desc
 create mode 100644 regression/cbmc-cover/unique-bytecode2/Test.class
 create mode 100644 regression/cbmc-cover/unique-bytecode2/Test.java
 create mode 100644 regression/cbmc-cover/unique-bytecode2/test.desc
 create mode 100644 regression/cbmc-cover/unique-bytecode3/Test.class
 create mode 100644 regression/cbmc-cover/unique-bytecode3/Test.java
 create mode 100644 regression/cbmc-cover/unique-bytecode3/test.desc

diff --git a/regression/cbmc-cover/unique-bytecode1/Test.class b/regression/cbmc-cover/unique-bytecode1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..8fa774304fd6c9a88db55a668f645bad89ff2495
GIT binary patch
literal 301
zcmYL_y-ve06ot=q(u9QmO)LnBu`tku1yQjeF%=k6u`oHos$5zZ1(zq_Nm!VfkQjIX
zo(LfX90w#UUEk~D^Ic#0?d#<gz&`ppB6L!8Q}hJM$U5tf1kqsULJ%J>uZ*BKw$7Zb
z7Nw~tx|~yq7uq_(#^7>1(|39}*KRs2d~MzIFo2!H>+1Sc-~9RWV!5g-b7BLWP0X#|
z3tSs9TI?1CLI1zic{wwc$2JtF3rjKR1xIAH#VpLN-Dk)X3qi^~X+%DNHO8;?fM|fb
l(P%SyKz1+k`28Lj)i8N;%P(N_oN5O32_+vq2-X{0`v-w@HDCY$

literal 0
HcmV?d00001

diff --git a/regression/cbmc-cover/unique-bytecode1/Test.java b/regression/cbmc-cover/unique-bytecode1/Test.java
new file mode 100644
index 0000000000..8ffd0be984
--- /dev/null
+++ b/regression/cbmc-cover/unique-bytecode1/Test.java
@@ -0,0 +1,6 @@
+class Test {
+  public static void main(String[] args) {
+    for (int i=0; i<3; i++) {
+    }
+  }
+}
diff --git a/regression/cbmc-cover/unique-bytecode1/test.desc b/regression/cbmc-cover/unique-bytecode1/test.desc
new file mode 100644
index 0000000000..1ac356b520
--- /dev/null
+++ b/regression/cbmc-cover/unique-bytecode1/test.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--cover location --show-properties --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^Ignoring block .* java::Test\.main
diff --git a/regression/cbmc-cover/unique-bytecode2/Test.class b/regression/cbmc-cover/unique-bytecode2/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c949f8d85a47b363eb9074cd1767f0b7ef1e7878
GIT binary patch
literal 262
zcmZ9GyAA<i5QWdIy<68_qC`QX6pch85elN;U4LX{t%T*hL?Kal01qY3FB*!OIr-+C
z$vj{82Y^26K1`H76i{(cbx;$?ku?$6gCtAxp`g%euLS03zgB|EG|ANLw2RbX8Ad6I
zJBZV-(_idQhggjh&Ap{M=G|?04g)xF16Z(mMpHpm^IjTeo8COysyIiJKbZW92ep&R
oU@=JIQ8hS))9TzH7Yc#TZhxQ-6@RQ;!E&!K{;dWB0hb0!Z<CNESpWb4

literal 0
HcmV?d00001

diff --git a/regression/cbmc-cover/unique-bytecode2/Test.java b/regression/cbmc-cover/unique-bytecode2/Test.java
new file mode 100644
index 0000000000..57c5f32c84
--- /dev/null
+++ b/regression/cbmc-cover/unique-bytecode2/Test.java
@@ -0,0 +1,3 @@
+class Test {
+  static int s=5;
+}
diff --git a/regression/cbmc-cover/unique-bytecode2/test.desc b/regression/cbmc-cover/unique-bytecode2/test.desc
new file mode 100644
index 0000000000..145a55f396
--- /dev/null
+++ b/regression/cbmc-cover/unique-bytecode2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--cover location --show-properties --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^java::Test\.<clinit>:\(\)V block 2, location 4: bytecode-index 1 already instrumented
+^Ignoring block 2 location .* file Test\.java line 2 function java::Test\.<clinit>:\(\)V bytecode-index .* \(bytecode-index already instrumented\)
+--
diff --git a/regression/cbmc-cover/unique-bytecode3/Test.class b/regression/cbmc-cover/unique-bytecode3/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..7cd485fe136508e66742524c696d267ac2146d40
GIT binary patch
literal 292
zcmYLD&1%A65S%stX{xC|N5M-$d#D$W(u*JnQV)vvBz{OFji9l#k0l<29{K=%DCvAb
z^su|Lv$MPNclr4RFhI+Ph0ueEC!OjJ8V;HQ`C?2M-vWD>=4tUJFuJ{^z#MH?N>H1o
zxq3f*#A>&Q;*5+tOtP!epKlMlM2%C;dkeKMUN_Na6u^TYz=jjRg~MBVBnb7epGEn)
zKZ`diDbS%Aiw-N)QBLIQjgo=B0>J~jHmk5&FK5V+KoBt7B}q$oyh)!+j?2ag74rn+
QF8BFI|1x1vR4sAsA6o$@B>(^b

literal 0
HcmV?d00001

diff --git a/regression/cbmc-cover/unique-bytecode3/Test.java b/regression/cbmc-cover/unique-bytecode3/Test.java
new file mode 100644
index 0000000000..857bb865a7
--- /dev/null
+++ b/regression/cbmc-cover/unique-bytecode3/Test.java
@@ -0,0 +1,4 @@
+class Test {
+  static int x = 0;
+  static int y = 1;
+}
diff --git a/regression/cbmc-cover/unique-bytecode3/test.desc b/regression/cbmc-cover/unique-bytecode3/test.desc
new file mode 100644
index 0000000000..ced6411193
--- /dev/null
+++ b/regression/cbmc-cover/unique-bytecode3/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--cover location --show-properties --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^java::Test\.<clinit>:\(\)V block 2, location 4: bytecode-index 1 already instrumented
+^java::Test\.<clinit>:\(\)V block 2: location 5, bytecode-index 3 selected for instrumentation
+--
+^Ignoring block 2 location .* file Test\.java line 3 function java::Test\.<clinit>:\(\)V bytecode-index .* \(bytecode-index already instrumented\)