From 2efea5290e297b1ef1f621c94a1e55d447221d4f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 3 Aug 2018 15:55:41 +0000
Subject: [PATCH] Refine test patterns to avoid spurious matches

Intermittent test failures were observed as "1005" happend to match the version
string in

CBMC version 5.9 (cbmc-5.9-1005-g2c1f35e2) 64-bit x86_64 linux
---
 jbmc/regression/jbmc/reachability-slice/test.desc  |  8 ++++----
 jbmc/regression/jbmc/reachability-slice/test2.desc | 10 +++++-----
 jbmc/regression/jbmc/reachability-slice/test3.desc | 10 +++++-----
 regression/cbmc/reachability-slice/test.desc       |  6 +++---
 regression/cbmc/reachability-slice/test2.desc      | 10 +++++-----
 regression/cbmc/reachability-slice/test3.desc      |  8 ++++----
 6 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/jbmc/regression/jbmc/reachability-slice/test.desc b/jbmc/regression/jbmc/reachability-slice/test.desc
index a5f7064d5f9..c997bae2a05 100644
--- a/jbmc/regression/jbmc/reachability-slice/test.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test.desc
@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
-1001
+= \(int\)\(short\)1001
 --
-1003
-1004
-1005
+= \(int\)\(short\)1003
+= \(int\)\(short\)1004
+= \(int\)\(short\)1005
 --
 Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
 At the time of writing of this test, 1002 is removed.
diff --git a/jbmc/regression/jbmc/reachability-slice/test2.desc b/jbmc/regression/jbmc/reachability-slice/test2.desc
index 2e95cfa5107..93b579d1b63 100644
--- a/jbmc/regression/jbmc/reachability-slice/test2.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test2.desc
@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
-1001
-1002
-1003
-1005
+= \(int\)\(short\)1001
+= \(int\)\(short\)1002
+= \(int\)\(short\)1003
+= \(int\)\(short\)1005
 --
-1004
+= \(int\)\(short\)1004
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/jbmc/regression/jbmc/reachability-slice/test3.desc b/jbmc/regression/jbmc/reachability-slice/test3.desc
index 8c84468ecc0..7b10cf97e1a 100644
--- a/jbmc/regression/jbmc/reachability-slice/test3.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test3.desc
@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --cover location
-1001
-1002
-1003
-1004
-1005
+= \(int\)\(short\)1001
+= \(int\)\(short\)1002
+= \(int\)\(short\)1003
+= \(int\)\(short\)1004
+= \(int\)\(short\)1005
 --
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/cbmc/reachability-slice/test.desc
index b43ba07552c..9d5cf620deb 100644
--- a/regression/cbmc/reachability-slice/test.desc
+++ b/regression/cbmc/reachability-slice/test.desc
@@ -1,9 +1,9 @@
 CORE
 test.c
 --reachability-slice --show-goto-functions --cover location --property foo.coverage.2
-1001
+= 1001
 --
-1004
-1005
+= 1004
+= 1005
 --
 We do not include 1002 and 1003, whether this is hit depends on where assertion is put
diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/cbmc/reachability-slice/test2.desc
index 6b9fb6d4d4f..e7d0787affb 100644
--- a/regression/cbmc/reachability-slice/test2.desc
+++ b/regression/cbmc/reachability-slice/test2.desc
@@ -1,9 +1,9 @@
 CORE
 test.c
 --reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
-1001
-1002
-1003
-1005
+= 1001
+= 1002
+= 1003
+= 1005
 --
-1004
+= 1004
diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/cbmc/reachability-slice/test3.desc
index 87e694174d1..ca3684f6281 100644
--- a/regression/cbmc/reachability-slice/test3.desc
+++ b/regression/cbmc/reachability-slice/test3.desc
@@ -1,10 +1,10 @@
 CORE
 test.c
 --reachability-slice --show-goto-functions --cover location
-1001
-1002
-1003
-1004
+= 1001
+= 1002
+= 1003
+= 1004
 --
 --
 We do not include 1005 since it might or might not be present based on where the assertion is in the block.