-
Notifications
You must be signed in to change notification settings - Fork 27
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Basic Nullness Checker configuration #3183
Conversation
It seems that I think we could need another annotation: If there is no annotation, then the class is excluded from checking, and an annotation like Is it possible to have the checker framework as an extra step outside compileJava? |
key.util/src/main/java/org/key_project/util/java/StringUtil.java
Outdated
Show resolved
Hide resolved
key.util/src/main/java/org/key_project/util/java/StringUtil.java
Outdated
Show resolved
Hide resolved
(not all checks are successful and need some more discussion!)
with Werner and Alexander
* origin/main: (65 commits) Remove unnecessary parentheses in JmlLexer Remove dead code Harmonize action and status bar labels All layout actions in one sub-menu Add shortcut key for last layout action Revert "Move layout controls to menu" Document 'minimize interactions' correctly Show SMT solver info in text area Consider divider width in layout Disable rearrangement of toolbar Fix extension panels not showing up sometimes Move layout controls to menu Make exploration extension experimental Spotless Fix broken test case for free conditions on block contracts Fix InvariantConfigurator repairs on the KeYParser Check for popup on all needed events Move action history button to main toolbar Set location of all dialogs relative to parent ... # Conflicts: # key.util/src/main/java/org/key_project/util/java/StringUtil.java
Added a system property which enables the nullness checker. See |
@wmdietl Following
Why is there a problem? The inner class is static. Edit: The correct version is |
* main: (63 commits) Bump org.junit.vintage:junit-vintage-engine from 5.10.1 to 5.10.2 Make caching more robust by catching exceptions Fix caching bug where an exception was thrown Transparent proof caching icon Bump org.junit.jupiter:junit-jupiter-engine from 5.10.1 to 5.10.2 Bump org.junit.jupiter:junit-jupiter-api from 5.10.1 to 5.10.2 Init new settings with last read config Always sort extension actions in context submenus New proof context menu action to cache open goals Bump com.diffplug.spotless from 6.24.0 to 6.25.0 Move caching settings to extension package Document other caching option Caching: make behaviour when reference proof is pruned configurable Handle prunes of proof cache targets Naming of cached goal re-open action Set tooltip of proof caching button Fix ProgramMethodFinder + javadocs Bump com.diffplug.spotless from 6.23.3 to 6.24.0 New action to re-open goals closed by cache Refactor CopyReferencedProof action into own class ... # Conflicts: # build.gradle # key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java # key.core/src/main/java/de/uka/ilkd/key/util/package-info.java # settings.gradle
@flo2702 The flag should work now. I have updated eisop to the latest version which results into one new compile error in The two compile errors on
First one repaired. |
* origin/main: (174 commits) unified naming of operator to "seq_upd". Bump org.ow2.asm:asm from 9.6 to 9.7 reformat after merge fix hashing of set statements and assert statements Typo in message in dlsmt.sh More logging in run all proofs Infrastructure for selection of proof groups Update pull_request_template.md fix check for cvc5 exit in error in dlsmt.sh fix cvc5 fix smt solver downloader script for z3 added references to hard-coded rulesets applying spotless replacing "\seq_length(x)" by "x.length" in set statements in examples fix rap for SetStatmentRule fix rap for JmlAssertRule repair unit tests Update broken link in README.md different highlighting for JML statements ...
* main: (36 commits) fix reviewer comments Add key features for the FM tutorial Bump ch.qos.logback:logback-classic in the gradle-deps group Bump ch.qos.logback:logback-classic from 1.5.3 to 1.5.5 Bump org.slf4j:slf4j-api from 2.0.12 to 2.0.13 applying spotless Boyer Moore Majority Vote Added test case for the bugfix Fixes a StackOverflow when pretty printing a taclet updating test case descriptions for error reporting Update dependabot.yml Update dependabot configuration Rename constant to TEMP_INDEX_SEPARATOR Fix newnames handling for new local vars cleaning up the test cases enabling KeY test cases common functionality in new superclass improving the feedback of the parsers in KeY Fix keyword for message matching for ParseExceptionTest better error reporting or JML parsing ...
We have a lot of type errors in the test cases. This leads to an interesting question: @mattulbrich @flo2702 Do we start with trusting the type system and get rid of the (now) useless NP checks? For example, consider public static <T> List<T> searchAll(Iterable<T> iterable, Predicate<T> filter) {
List<T> result = new ArrayList<>();
if (iterable != null && filter != null) {
for (T element : iterable) {
if (filter.test(element)) {
result.add(element);
}
}
}
return result;
} Are useless now, as the parameters are non-null by type system. There are test cases which for behavior with null args which currently fail in the type checker.
Errors:
|
Is there a plan for the other modules? Next would be |
This integrates the Nullness Checker into
./gradlew compileJava
.The line
"-AonlyDefs=^org\\.key_project\\.util\\.lookup"
says that only elements in theorg.key_project.util.lookup
package should be checked.I only did a quick annotation of that file, which might need to change when more sources are checked.