GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-22 23:32:15 +03:00
Code Issues Projects Releases Wiki Activity
63a65c3d85
macaw/macaw-aarch32-symbolic
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
..
src/Data/Macaw/AArch32 Revise handling of syscalls in AArch32 to match X86 (#246) 2021-11-24 11:59:56 -08:00
tests x86: Fix failing proof obligations due to EvenParity 2022-01-21 15:33:10 -08:00
CHANGELOG.md Add a (dummy) symbolic backend for AArch32 2020-04-05 21:16:03 -07:00
LICENSE Add a (dummy) symbolic backend for AArch32 2020-04-05 21:16:03 -07:00
macaw-aarch32-symbolic.cabal AArch32: Support conditional returns (#243) 2021-11-19 16:20:50 -08:00
Setup.hs Add a (dummy) symbolic backend for AArch32 2020-04-05 21:16:03 -07:00