You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
On the crucible-integration branch, the crucible_llvm_verify command can be used to verify LLVM functions, but it cannot use previous proofs as overrides. It takes a list of overrides as parameters, but will currently fail if the verification attempts to use those overrides.
The scope of this ticket is to implement the most central features of overrides: arguments and return values. Supporting these will require processing specifications that include only crucible_fresh_var and crucible_execute_func (including the return value of crucible_execute_func). Separate tickets will describe addition features of overrides.
The text was updated successfully, but these errors were encountered:
On the
crucible-integration
branch, thecrucible_llvm_verify
command can be used to verify LLVM functions, but it cannot use previous proofs as overrides. It takes a list of overrides as parameters, but will currently fail if the verification attempts to use those overrides.The scope of this ticket is to implement the most central features of overrides: arguments and return values. Supporting these will require processing specifications that include only
crucible_fresh_var
andcrucible_execute_func
(including the return value ofcrucible_execute_func
). Separate tickets will describe addition features of overrides.The text was updated successfully, but these errors were encountered: