Merge pull request #433 from GaloisInc/lb/stack-abi

 x86-symbolic: Setting up a SysV-compatible stack

macaw-aarch32-symbolic/tests/Main.hs

@@ -106,7 +106,7 @@ armResultExtractor :: ( CB.IsSymInterface sym
                       )
                    => MS.ArchVals MA.ARM
                    -> MST.ResultExtractor sym MA.ARM
-armResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do
+armResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do
   let re = MS.lookupReg archVals regs (MAR.ARMGlobalBV (ASL.knownGlobalRef @"_R0"))
   k PC.knownRepr (CS.regValue re)
 

macaw-aarch32-symbolic/tests/README.org

@@ -1,7 +1,7 @@
 * Overview
 This test suite tests that symbolic execution of AArch32 programs works. It is also a convenient place to test the semantics.  The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories.  In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states.  It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion).  Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected).  The test harness uses yices for path satisfiability checking and z3 to prove goals.  Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
 
-In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures).
+In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures).
 
 * Usage
 

macaw-ppc-symbolic/tests/Main.hs

@@ -118,7 +118,7 @@ ppcResultExtractor :: ( arch ~ MP.AnyPPC v
                       )
                    => MS.ArchVals arch
                    -> MST.ResultExtractor sym arch
-ppcResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do
+ppcResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do
   let re = MS.lookupReg archVals regs (MP.PPC_GP (DP.GPR 3))
   k PC.knownRepr (CS.regValue re)
 

macaw-ppc-symbolic/tests/README.org

@@ -1,7 +1,7 @@
 * Overview
 This test suite tests that symbolic execution of PowerPC programs works. It is also a convenient place to test the semantics.  The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories.  In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states.  It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion).  Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected).  The test harness uses yices for path satisfiability checking and z3 to prove goals.  Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
 
-In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures).
+In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures).
 
 * Usage
 

macaw-riscv-symbolic/tests/Main.hs

@@ -109,7 +109,7 @@ riscvResultExtractor :: ( arch ~ MR.RISCV rv
                         )
                      => MS.ArchVals arch
                      -> MST.ResultExtractor sym arch
-riscvResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do
+riscvResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do
   let re = MS.lookupReg archVals regs MR.GPR_A0
   k PC.knownRepr (CS.regValue re)
 

macaw-riscv-symbolic/tests/README.org

@@ -1,7 +1,7 @@
 * Overview
 This test suite tests that symbolic execution of RISC-V programs works. It is also a convenient place to test the semantics.  The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories.  In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states.  It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion).  Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected).  The test harness uses yices for path satisfiability checking and z3 to prove goals.  Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
 
-In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures).
+In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures).
 
 * Usage