Commit c0bd89e7 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Bigfix in relaoding contracts

parent 291eec9d
Pipeline #23252 passed with stages
in 82 minutes and 7 seconds
...@@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.Services; ...@@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.init.ProofOblInput;
import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
...@@ -91,8 +92,23 @@ public class KeYProofFacade { ...@@ -91,8 +92,23 @@ public class KeYProofFacade {
*/ */
public void reload(File problemFile) throws ProofInputException, ProblemLoaderException { public void reload(File problemFile) throws ProofInputException, ProblemLoaderException {
if (contract.get() != null) {// reinstante the contract if (contract.get() != null) {// reinstante the contract
setProof(getEnvironment().createProof( pma = KeYApi.loadFromKeyFile(problemFile);
contract.get().getProofObl(getEnvironment().getServices()))); List<Contract> contracts = pma.getProofContracts();
contracts.forEach(contract1 -> {
if(contract.get().getName().equals(contract1.getName())){
contractProperty().set(contract1);
}
});
if(contract.get() != null){
try{
activateContract(contract.get());
}catch (ProofInputException pie){
throw new ProofInputException("Contract not reloadable.", pie.getCause());
}
}
/*setProof(getEnvironment().createProof(
contract.get().getProofObl(getEnvironment().getServices())));*/
} else { } else {
setProof(KeYApi.loadFromKeyFile(problemFile).getLoadedProof().getProof()); setProof(KeYApi.loadFromKeyFile(problemFile).getLoadedProof().getProof());
} }
......
...@@ -545,10 +545,11 @@ public class DebuggerMain implements Initializable { ...@@ -545,10 +545,11 @@ public class DebuggerMain implements Initializable {
//save old information and refresh models //save old information and refresh models
statusBar.publishMessage("Reloading..."); statusBar.publishMessage("Reloading...");
File lastLoaded; File lastLoaded;
Contract chosen = null;
if (model.getKeyFile() != null) { if (model.getKeyFile() != null) {
lastLoaded = model.getKeyFile(); lastLoaded = model.getKeyFile();
} else { } else {
Contract chosen = model.getChosenContract(); chosen = model.getChosenContract();
lastLoaded = model.getJavaFile(); lastLoaded = model.getJavaFile();
} }
//model.reload(); //model.reload();
...@@ -562,8 +563,11 @@ public class DebuggerMain implements Initializable { ...@@ -562,8 +563,11 @@ public class DebuggerMain implements Initializable {
iModel.clearHighlightLines(); iModel.clearHighlightLines();
iModel.getGoals().clear(); iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null); iModel.setSelectedGoalNodeToShow(null);
if(chosen != null) {
FACADE.contractProperty().set(chosen);
}
try { try {
FACADE.reload(lastLoaded); FACADE.reload(lastLoaded);
if (iModel.getGoals().size() > 0) { if (iModel.getGoals().size() > 0) {
iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0)); iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment