dinuxOct 3, 2025
Krister Walfridsson

I have implemented support for BPF assembly in the smtgcc GCC translation validator:
https://github.com/kristerw/smtgcc

It has already found multiple bugs in the GCC BPF backend. I have reported three so far:
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=122139
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=122140
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=122141

GitHub - kristerw/smtgcc: Some experiments with SMT solvers and GIMPLE IR

Some experiments with SMT solvers and GIMPLE IR. Contribute to kristerw/smtgcc development by creating an account on GitHub.

GitHub
Oct 3, 2025 at 1:07amWeb
Show threadJohn RegehrOct 3, 2025
@kristerw nice work! wouldn't have expected this kind of low-hanging fruit.