Accommodate changes from GaloisInc/macaw#310

RyanGlScott · RyanGlScott · commit bd244edbceba · 2023-03-01T11:05:36.000-05:00
This bumps the `macaw` submodule to bring in the changes from GaloisInc/macaw#310, which removes some redundant pointer validity checks from `macaw-symbolic`'s load- and store-related operations. Because the verifier's test suite counts the number of goals generated, this has the effect of reducing the overall number of goals in some test cases. I have confirmed (by manual inspection) that the goals that were removed with this patch all come from the redundant checks removed in the `macaw` patch.
diff --git a/submodules/macaw b/submodules/macaw
@@ -1 +1 @@
-Subproject commit 734039274d3d00cb7728aca3ce0999fb8a02015e
+Subproject commit d9525554ca3d6414e20a9f7571e38758ea5a3c3f
diff --git a/tests/binaries/x86_64/fsbase.exe.expected b/tests/binaries/x86_64/fsbase.exe.expected
@@ -1,3 +1,3 @@
 successful: 0
-failed: 2
+failed: 1
 
diff --git a/tests/binaries/x86_64/function-call-pie.exe.expected b/tests/binaries/x86_64/function-call-pie.exe.expected
@@ -1,3 +1,3 @@
-successful: 6
-failed: 6
+successful: 4
+failed: 5
 
diff --git a/tests/binaries/x86_64/function-call.exe.expected b/tests/binaries/x86_64/function-call.exe.expected
@@ -1,3 +1,3 @@
-successful: 6
-failed: 6
+successful: 4
+failed: 5
 
diff --git a/tests/binaries/x86_64/stack-read.exe.expected b/tests/binaries/x86_64/stack-read.exe.expected
@@ -1,3 +1,3 @@
 successful: 0
-failed: 4
+failed: 2
 
diff --git a/tests/binaries/x86_64/stack-write.exe.expected b/tests/binaries/x86_64/stack-write.exe.expected
@@ -1,3 +1,3 @@
 successful: 0
-failed: 4
+failed: 2
 
diff --git a/tests/binaries/x86_64/syscall.exe.expected b/tests/binaries/x86_64/syscall.exe.expected
@@ -1,3 +1,3 @@
 successful: 0
-failed: 2
+failed: 1
 

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,3 @@`
`1`	`1`	`successful: 0`
`2`		`-failed: 2`
	`2`	`+failed: 1`
`3`	`3`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,3 @@`
`1`	`1`	`successful: 0`
`2`		`-failed: 4`
	`2`	`+failed: 2`
`3`	`3`