Renovation of the TestCase generation #3388
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
wadoon
added
🐞 Bug
Test Case Generator
🛠 Maintenance
wadoon
force-pushed
the
weigl/testgen
branch
2 times, most recently
from
87f9f32
to
25a0200
Compare
wadoon
force-pushed
the
weigl/testgen
branch
2 times, most recently
from
7abaaf2
to
ddab633
Compare
# By Drodt (54) and others # Via GitHub (3) and others * origin/main: (89 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 Document ncore Fix merge import errors Fix merge errors Spotless Fix label retainement on terms Use static operator comparison Fix NPE for some taclet input Rename JavaDLFunction -> JFunction Remove JavaBlock from TermFactory Fix renamer Spotless Fix(?) information flow tests Spotless Add Function to ncore; add Modifier Fix rebase Fix rebase and run spotless Cleanup Visitor inheritance of Term visitors ... # Conflicts: # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleConstant.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java
* refs/heads/main: (63 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: (69 commits) reformat with spotless typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization key.ncore done configure key.ncore fix null values eisop in ncore Fix formatting Fix more NoSuchElementExceptions Fix NoSuchElementException in JavaInfo Remove redundant nullness checks and fix test cases Fix proof script fix error in the legacy compat part of the proof obligation loading revert some changes of Mattias in the Configuration #equals must allow null values jspecify was missing in the compile classpath of tests Code style Revert JavaRedux Object ...
* refs/heads/main: (26 commits) Fix comment Fix checkstyle workflow Fix checkstyle workflow Fix merge conflicts & spotless Remove todo Spotless Fix? resolving error Move ParsableVariable to ncore Spotless Spotless Rename AbstractSV to OperatorSV Beautified code Fix settings test for SE Spotless fixes Fix taclet prefix check when parsing Fix taclet equality test Fix parsing of variable conditions Fix errors resulting from changing ParseableVar Delete Legacy Matcher and adapt VM matcher for new Modality operator Fix errors after changing ParsableVars ...
* also fix some encoding in recorder/src files
* weigl/codequality: reenable sonarqube, disable the crappy things adding comments to jml spec factory default contracts EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Fix test case that failed with new default-contract behavior Fix code format Add test Add documentation Add proof setting for sound or unsound default contracts Don't add default contracts for Object or <init> methods Default contract for contractless methods Fix compiler check when using classpath Add printf to JavaRedux
* refs/heads/main: Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test repair soundness of assignment2UpdateRules with checked overflows spotless Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version API design throw an error if choices used in a taclet are not declared correct inRange(..) predicates for overflow check semantics fix creating of branches for overflow checking
# Conflicts: # .github/workflows/code_quality.yml # build.gradle # key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Intended Change
Make test case generation usable again, especially, from the CLI in the new verification template.
Type of pull request
Changes
StringBuilderfoo.