More LLVMSetup error checking #2758
Conversation
|
The new error checks broke a few of our integration tests, which included specs that had missing |
RyanGlScott
left a comment
RyanGlScott
left a comment
There was a problem hiding this comment.
Yes, please do mention this in the changelog. I suspect that this will actually break some proofs in the wild—rightfully so in some cases, but we should give some general advice on how to migrate these proofs.
brianhuffman
force-pushed
the
bh/llvm-setup-errors
branch
from
0a067fc to
098a023
Compare
Function crucible_execute_func is called internally by llvm_execute_func, jvm_execute_func and mir_execute_func. So this should detect duplicates of any of these.
The check should happen with both llvm_verify and llvm_unsafe_assume_spec.
The following integration tests used LLVMSetup blocks with missing llvm_return specifications, which are now required if the function has a non-void return type. * test0061_path_sat * test0061_detect_vacuity * test0067_term_eqs * test_sanitize
An llvm_execute_func declaration is now required in all LLVMSetup blocks.
|
I just noticed that the docstring for |
brianhuffman
force-pushed
the
bh/llvm-setup-errors
branch
from
098a023 to
2cd5a75
Compare
|
|
||
| ## Changes | ||
|
|
||
| * `llvm_verify` now enforces that an `llvm_return` specification is |
There was a problem hiding this comment.
This applies to jvm_verify as well, right?
There was a problem hiding this comment.
Yes, it does. I'll add a note saying that the same applies to jvm_verify/jvm_return.
(Logically this entry ought to have been included as part of #2743.)
This is basically like PR #2743, but for LLVM. We now detect the following error conditions in
LLVMSetupblocks:llvm_execute_funcdeclarationsllvm_execute_funcdeclarationsllvm_returndeclaration on non-void functionThis fixes the LLVM part of #2506.
Note that we still need a comprehensive regression test to exercise this and all other
LLVMSetuperror-checking code (#947); such a test is not included in this PR.