Skip to content
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.

Sign up for GitHub

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

Jump to bottom

LemmaGenerator #3477

Closed
wadoon opened this issue Jun 7, 2024 · 0 comments · Fixed by #3481
Closed

LemmaGenerator #3477

wadoon opened this issue Jun 7, 2024 · 0 comments · Fixed by #3481
Assignees
@unp1

Comments

@wadoon
Copy link
Member

wadoon commented Jun 7, 2024

Description

Please describe your concern in detail!

Reproducible

Is the issue reproducible?
Select one of: always, sometimes, random, have not tried, n/a

Steps to reproduce

Describe the steps needed to reproduce the issue.

  1. ...
  2. ...
  3. ...

What is your expected behavior and what was the actual behavior?

[14:40:35.608] ERROR LemmaGenerationAction - java.lang.NullPointerException: Cannot invoke "org.key_project.util.collection.ImmutableSet.isEmpty()" because "set" is null
        at org.key_project.util.collection.DefaultImmutableSet.originalUnion(DefaultImmutableSet.java:135)
        at org.key_project.util.collection.DefaultImmutableSet.union(DefaultImmutableSet.java:125)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:336)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:570)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:461)
        at de.uka.ilkd.key.taclettranslation.lemma.TacletLoader.getProofEnvForTaclets(TacletLoader.java:109)
        at de.uka.ilkd.key.gui.actions.LemmaGenerationAction$ProveUserDefinedTaclets.loadTaclets(LemmaGenerationAction.java:243)
unp1 added a commit that referenced this issue Jun 14, 2024
@unp1
Fix loading of taclet proof obligations (issue #3477)
a49cf56 
* This commit fixes an NPE when loading
* This commit fixes missing or inconsistent selection of loaded proof
  obligation
@unp1 unp1 mentioned this issue Jun 14, 2024
Merged
unp1 added a commit that referenced this issue Jun 14, 2024
@unp1
Fix loading of taclet proof obligations (issue #3477)
77d6967 
* This commit fixes an NPE when loading
* This commit fixes missing or inconsistent selection of loaded proof
  obligation
@unp1 unp1 self-assigned this Jun 14, 2024
@unp1 unp1 linked a pull request Jun 14, 2024 that will close this issue
Fix loading of taclet proof obligations (issue #3477) #3481
Merged
github-merge-queue bot pushed a commit that referenced this issue Jun 14, 2024
@wadoon
Fix loading of taclet proof obligations (issue #3477) (#3481)
19f83d3
wadoon added a commit that referenced this issue Jun 21, 2024
@wadoon
Merge branch 'refs/heads/main' into weigl/key-javaparser3
78286a3 
* refs/heads/main: (40 commits)
  spotlessing ...
  making RuleCommand work if already fully instantiated
  RuleCommand can now deal with rules that have schema variables for logical variables.
  Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof   obligation
  Code clean up (remove unused method)
  Fix loading of closed proofs (GUI threw error)
  Spotless fixes
  Fixed small typo in merge fixes.
  fix \locset() with empty args
  adding test cases for empty seq and locset.
  allow "\seq()" and "\locset()" in JML
  Bump the gradle-deps group with 6 updates
  Bump the github-actions-deps group with 4 updates
  Code formatting
  Adapted those qodana suggestions that are not false positives.
  Removed eclipse project file
  Also fixes for testcases
  Applied spotless
  Towards desired renaming on JML level
  Again spotless
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractExternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContract.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContract.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/OperationContract.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/RepresentsAxiom.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/dl/translation/DLSpecFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassAxiom.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassInv.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLFieldDecl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLInitially.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLRepresents.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSetStatement.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLMethodResolver.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java
#	key.core/src/test/resources/testcase/proofBundle/complexBundleGeneration/a/lang/String.key
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java
wadoon added a commit that referenced this issue Jun 21, 2024
@wadoon
Merge branch 'refs/heads/main' into weigl/pckgreworked
7200b6a 
* refs/heads/main: (42 commits)
  EQ version of seqSwapPreservesSeqPerm + proof
  added rule for sequences: swap preserves perm
  spotlessing ...
  making RuleCommand work if already fully instantiated
  RuleCommand can now deal with rules that have schema variables for logical variables.
  Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof   obligation
  Code clean up (remove unused method)
  Fix loading of closed proofs (GUI threw error)
  Spotless fixes
  Fixed small typo in merge fixes.
  fix \locset() with empty args
  adding test cases for empty seq and locset.
  allow "\seq()" and "\locset()" in JML
  Bump the gradle-deps group with 6 updates
  Bump the github-actions-deps group with 4 updates
  Code formatting
  Adapted those qodana suggestions that are not false positives.
  Removed eclipse project file
  Also fixes for testcases
  Applied spotless
  ...
wadoon added a commit to wadoon/key that referenced this issue Jun 26, 2024
@wadoon
Merge branch 'main' into weigl/recordsftw
49a2b02 
* main: (77 commits)
  Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
  spotless
  update oracle for taclet equality test
  change gradle github action to new syntax
  adding comments to jml spec factory default contracts
  repair soundness of assignment2UpdateRules with checked overflows
  spotless
  EQ version of seqSwapPreservesSeqPerm + proof
  added rule for sequences: swap preserves perm
  Changed types in replacement map for WD taclets, since PR KeYProject#3436 made casting TermSV to ProgramVariable not applicable
  spotlessing ...
  making RuleCommand work if already fully instantiated
  RuleCommand can now deal with rules that have schema variables for logical variables.
  Fix loading of taclet proof obligations (issue KeYProject#3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof   obligation
  Code clean up (remove unused method)
  Fix loading of closed proofs (GUI threw error)
  Fix and test goToNext()
  Fix goToNextSibling() (thx Tobias)
  Format
  Add comments and next() method
  ...
wadoon added a commit that referenced this issue Jun 26, 2024
@wadoon
Merge branch 'main' into eisop/keycore2
9e0ce25 
* main: (77 commits)
  Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
  spotless
  update oracle for taclet equality test
  change gradle github action to new syntax
  adding comments to jml spec factory default contracts
  repair soundness of assignment2UpdateRules with checked overflows
  spotless
  EQ version of seqSwapPreservesSeqPerm + proof
  added rule for sequences: swap preserves perm
  Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable
  spotlessing ...
  making RuleCommand work if already fully instantiated
  RuleCommand can now deal with rules that have schema variables for logical variables.
  Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof   obligation
  Code clean up (remove unused method)
  Fix loading of closed proofs (GUI threw error)
  Fix and test goToNext()
  Fix goToNextSibling() (thx Tobias)
  Format
  Add comments and next() method
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@unp1 unp1

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix loading of taclet proof obligations (issue #3477) KeYProject/key
2 participants
@wadoon @unp1