Adapt to debugIntrinsics
option in crucible
#1388
Labels
PR: submodule bump
Pull requests that include a submodule bump
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
GaloisInc/crucible#782 adds a new
debugIntrinsics
option, which controls whetherllvm.dbg
statements should be translated or not, to various functions incrucible-llvm:Lang.Crucible.LLVM.Translation
, which will affect SAW. While tools like Crux can safely setdebugIntrinsics
toFalse
, as they do not make use ofllvm.dbg
intrinsics, SAW does make use of these intrinsics (see #1385). As a result, we'll need to be a bit careful when updating SAW to use GaloisInc/crucible#782. We'll likely want to add a SAW option for configuring the value ofdebugIntrinsics
, since there are programs (such as the one identified in GaloisInc/crucible#778) that currently will not work in Crucible with the debug intrinsics present.The text was updated successfully, but these errors were encountered: