Skip to content

Conversation

@KevinLeeFM
Copy link

@KevinLeeFM KevinLeeFM commented Sep 18, 2025

Motivation for this PR

I have made this work-in-progress port to LLVM 15 available for use in research. Through initial testing against verify-c-common benchmark, precision loss appears to be outweighed by the need to unblock ongoing research efforts for some people.

Specifically, there are loss of precision due to pointee type information no longer provided by the LLVM IR. While a few functions in this PR was able to be refactored to maintain functionality (although no testing is done yet to confirm), most changes involved commenting out a signification portion of the code and resorting to return a safer and imprecise answer.

Work is ongoing to improve this port. See #162 for details.

@KevinLeeFM KevinLeeFM changed the title LLVM 15 Port Experimental LLVM 15 Port Sep 18, 2025
@agurfinkel agurfinkel merged commit 8248b6b into seahorn:dev15 Sep 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants