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
WPI should be able to infer flow-sensitive type refinement annotations. Specifically, WPI should be able to infer the following annotation for OptStringContainer#isStringEqTo:
Given that @Pure is inferred for OptStringContainer#getOptStr
After WPI is able to infer these annotations, running the Optional Checker on the annotated code should output no errors.
The text was updated successfully, but these errors were encountered:
mernst
changed the title
Feature request: WPI should infer flow-sensitive type refinement annotations
Feature request: WPI should infer conditional postconditions
Feb 6, 2024
Given the following Java class:
WPI should be able to infer flow-sensitive type refinement annotations. Specifically, WPI should be able to infer the following annotation for
OptStringContainer#isStringEqTo
:Given that
@Pure
is inferred forOptStringContainer#getOptStr
After WPI is able to infer these annotations, running the Optional Checker on the annotated code should output no errors.
The text was updated successfully, but these errors were encountered: