If you're allowed to have false positives, it's not so hard. Like "this function allocates if A or B is true" just becomes "this function can allocate". It's no

If you're allowed to have false positives, it's not so hard. Like "this function allocates if A or B is true" just becomes "this function can allocate". It's not so different from finding functions that can panic.