`crucible-llvm`: Skip `llvm.experimental.noalias.scope.decl` and `llvm.dbg.assign` - Githubissues

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs

617 stars 42 forks source link

`crucible-llvm`: Skip `llvm.experimental.noalias.scope.decl` and `llvm.dbg.assign` #1205

Closed RyanGlScott closed 2 months ago

RyanGlScott commented 2 months ago

This adds llvm.experimental.noalias.scope.decl and llvm.dbg.assign to the list of LLVM intrinsics that crucible-llvm skips over during simulation. Doing so unlocks more support for recent LLVM versions.

It is conceivable that we may want to reason about these intrinsics at a deeper level some day. If so, see:

https://github.com/GaloisInc/crucible/issues/1196#issuecomment-2129665566 for how this would be done for llvm.experimental.noalias.scope.decl
https://github.com/GaloisInc/crucible/issues/1204#issue-2315526875 for how this would be done for llvm.dbg.assign

Fixes #1196. Fixes #1204.