GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-03 10:51:25 +03:00
Code Issues Projects Releases Wiki Activity
0f2264b7c4
macaw/x86_symbolic/tests/fail
History
Tristan Ravitch 63a65c3d85 x86: Fix failing proof obligations due to EvenParity 
See the writeup in Crucible.hs in this commit for details. In short, the recent
changes to generalize `PtrAdd` triggered a failing proof obligation due to a use
of `llvmPointer_bv`.  The new implementation is as sound as the previous one,
but more general.

Fixes #260
2022-01-21 15:33:10 -08:00
..
constant.c Add a testing framework for macaw-symbolic (#184) 2021-03-01 09:21:44 -08:00
constant.opt.exe Add a testing framework for macaw-symbolic (#184) 2021-03-01 09:21:44 -08:00
constant.unopt.exe Add a testing framework for macaw-symbolic (#184) 2021-03-01 09:21:44 -08:00
Makefile Add a testing framework for macaw-symbolic (#184) 2021-03-01 09:21:44 -08:00
T260.c x86: Fix failing proof obligations due to EvenParity 2022-01-21 15:33:10 -08:00
T260.opt.exe x86: Fix failing proof obligations due to EvenParity 2022-01-21 15:33:10 -08:00
T260.unopt.exe x86: Fix failing proof obligations due to EvenParity 2022-01-21 15:33:10 -08:00