Bugfix with services object and contract loading+ added test cases

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java

@@ -132,7 +132,7 @@ public class KeYProofFacade {
             @Override
             protected void succeeded() {
                 System.out.println("KeYProofFacade.succeeded");
-                environment.set(getValue().getEnv());
+                setEnvironment(getValue().getEnv());
                 //SaG: this needs to be set to filter inapplicable rules
                 getEnvironment().getProofControl().setMinimizeInteraction(true);
                 proof.set(getValue().getProof());
@@ -183,13 +183,17 @@ public class KeYProofFacade {
     public List<Contract> getContractsForJavaFile(File javaFile)
             throws ProblemLoaderException {
         pma = KeYApi.loadFromKeyFile(javaFile);
+        setEnvironment(pma.getCurrentEnv());
         //TODO relax key api setEnvironment(pma.getEnvironment());
-        return pma.getProofContracts();
+        List<Contract> contracts =  pma.getProofContracts();
+
+//        environment.set(pma.getCurrentEnv());
+        return contracts;
     }
 
     public void activateContract(Contract c) throws ProofInputException {
         ProofApi pa = pma.startProof(c);
-        environment.set(pa.getEnv());
+        setEnvironment(pa.getEnv());
         proof.set(pa.getProof());
         contract.set(null);
     }
@@ -226,6 +230,7 @@ public class KeYProofFacade {
 
     //region Getter and Setters
     public Services getService() {
+
         //FIXME if key api relaxed
         return pma != null ? pma.getServices() : getEnvironment().getServices();
     }

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EnvironmentTest.java

+package edu.kit.iti.formal.psdbg.interpreter;
+
+import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.api.ProofManagementApi;
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.logic.op.IObserverFunction;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.settings.ChoiceSettings;
+import de.uka.ilkd.key.settings.ProofSettings;
+import de.uka.ilkd.key.speclang.Contract;
+import de.uka.ilkd.key.strategy.StrategyProperties;
+import de.uka.ilkd.key.util.KeYTypeUtil;
+import de.uka.ilkd.key.util.MiscTools;
+import static edu.kit.iti.formal.psdbg.TestHelper.getFile;
+import org.junit.Test;
+import org.key_project.util.collection.ImmutableSet;
+
+import java.io.File;
+import java.net.URL;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Set;
+
+public class EnvironmentTest {
+
+        /**
+         * The program entry point.
+         */
+        @Test
+        public void bigInt() {
+            File location  = new File(getFile(getClass(), "javaTestFiles/BigInteger.java"));
+
+            List<File> classPaths = null; // Optionally: Additional specifications for API classes
+            File bootClassPath = null; // Optionally: Different default specifications for Java API
+            List<File> includes = null; // Optionally: Additional includes to consider
+            try {
+                // Ensure that Taclets are parsed
+                if (!ProofSettings.isChoiceSettingInitialised()) {
+                    KeYEnvironment<?> env = KeYEnvironment.load(location, classPaths, bootClassPath, includes);
+                    env.dispose();
+                }
+                // Set Taclet options
+                ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
+                HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
+                HashMap<String, String> newSettings = new HashMap<String, String>(oldSettings);
+                newSettings.putAll(MiscTools.getDefaultTacletOptions());
+                choiceSettings.setDefaultChoices(newSettings);
+                // Load source code
+                KeYEnvironment<?> env = KeYEnvironment.load(location, classPaths, bootClassPath, includes); // env.getLoadedProof() returns performed proof if a *.proof file is loaded
+                try {
+                    // List all specifications of all types in the source location (not classPaths and bootClassPath)
+                    final List<Contract> proofContracts = new LinkedList<Contract>();
+                    Set<KeYJavaType> kjts = env.getJavaInfo().getAllKeYJavaTypes();
+                    for (KeYJavaType type : kjts) {
+                        if (!KeYTypeUtil.isLibraryClass(type)) {
+                            ImmutableSet<IObserverFunction> targets = env.getSpecificationRepository().getContractTargets(type);
+                            for (IObserverFunction target : targets) {
+                                ImmutableSet<Contract> contracts = env.getSpecificationRepository().getContracts(type, target);
+                                for (Contract contract : contracts) {
+                                    proofContracts.add(contract);
+
+                                    System.out.println("contract.getPlainText(env.getServices()) = " + contract.getPlainText(env.getServices()));
+                                }
+                            }
+                        }
+                    }
+
+                }
+                finally {
+                    env.dispose(); // Ensure always that all instances of KeYEnvironment are disposed
+                }
+            }
+            catch (ProblemLoaderException e) {
+                System.out.println("Exception at '" + location + "':");
+                e.printStackTrace();
+            }
+        }
+
+
+    /**
+     * API test
+     */
+    @Test
+    public void bigInt2() {
+        File location  = new File(getFile(getClass(), "javaTestFiles/BigInteger.java"));
+
+
+        List<File> classPaths = null; // Optionally: Additional specifications for API classes
+        File bootClassPath = null; // Optionally: Different default specifications for Java API
+        List<File> includes = null; // Optionally: Additional includes to consider
+
+        try {
+            KeYProofFacade facade = new KeYProofFacade();
+           // ProofApi proofApi = facade.loadKeyFile(location);
+            //List<Contract> contractsForJavaFile = facade.getContractsForJavaFile(location);
+            //contractsForJavaFile.forEach(contract -> System.out.println("contract.getPlainText(facade.getService()) = " + contract.getPlainText(facade.getService())));
+
+
+
+            ProofManagementApi pma = KeYApi.loadFromKeyFile(location);
+            facade.setEnvironment(pma.getCurrentEnv());
+            List<Contract> proofContracts = pma.getProofContracts();
+            proofContracts.forEach(contract -> System.out.println(contract.getPlainText(facade.getService())));
+
+
+        } catch (ProblemLoaderException e) {
+            e.printStackTrace();
+        }
+    }
+
+}

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/BigInteger.java

+package java.math;
+
+import java.util.Arrays;
+
+public class BigInteger extends Number implements Comparable/*<BigInteger>*/ {
+    /**
+     * The signum of this BigInteger: -1 for negative, 0 for zero, or
+     * 1 for positive.  Note that the BigInteger zero <i>must</i> have
+     * a signum of 0.  This is necessary to ensures that there is exactly one
+     * representation for each BigInteger value.
+     *
+     * @serial
+     */
+    final int signum;
+
+    /**
+     * The magnitude of this BigInteger, in <i>big-endian</i> order: the
+     * zeroth element of this array is the most-significant int of the
+     * magnitude.  The magnitude must be "minimal" in that the most-significant
+     * int ({@code mag[0]}) must be non-zero.  This is necessary to
+     * ensure that there is exactly one representation for each BigInteger
+     * value.  Note that this implies that the BigInteger zero has a
+     * zero-length mag array.
+     */
+    final int[] mag;
+
+    /**
+     * This constant limits {@code mag.length} of BigIntegers to the supported
+     * range.
+     */
+    private static final int MAX_MAG_LENGTH = Integer.MAX_VALUE / Integer.SIZE + 1; // (1 << 26)
+
+    /**
+     * This mask is used to obtain the value of an int as if it were unsigned.
+     */
+    final static long LONG_MASK = 0xffffffffL;
+
+    /**
+     * The BigInteger constant zero.
+     *
+     * @since   1.2
+     */
+    public static final BigInteger ZERO = new BigInteger(new int[0], 0);
+
+
+    /*@ helper normal_behavior
+      @ ensures this.mag == magnitude;
+      @*/
+    BigInteger(int[] magnitude, int signum) {
+
+    }
+
+
+
+
+
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java

@@ -102,7 +102,9 @@ public class ContractChooser extends Dialog<Contract> {
         private void render() {
             if (getItem() != null) {
                 text.getChildren().clear();
-                String content = getItem().getPlainText(services);
+                System.out.println(getItem().getName());
+                String content = content = getItem().getPlainText(services);
+
                 Text contract = new Text("Contract for method: ");
                 Text name = new Text(getItem().getTarget().toString());
                 Text tcontent = new Text(content);
@@ -116,7 +118,7 @@ public class ContractChooser extends Dialog<Contract> {
                 text.getChildren().add(new Text("\n"));
                 //text.getChildren().addCell(tcontent);
 
-                for (String line : content.split("\n")) {
+               for (String line : content.split("\n")) {
                     if (line.contains(":")) {
                         String[] a = line.split(":", 2);
                         Text s = new Text(String.format("%-15s", a[0] + ":"));

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -833,6 +833,7 @@ public class DebuggerMain implements Initializable {
         if (javaFile != null) {
             model.setJavaFile(javaFile);
             model.setInitialDirectory(javaFile.getParentFile());
+
             contractLoaderService.reset();
             contractLoaderService.start();
         }
@@ -1507,7 +1508,10 @@ public class DebuggerMain implements Initializable {
 
             ContractChooser cc = null;
             try {
-                cc = new ContractChooser(FACADE.getService(), FACADE.getContractsForJavaFile(model.getJavaFile()));
+                //SaG: Never refactor these two calls, as otherwise the service object is not set. The contracts have to be loaded first.
+                //In case they are loaded the right service object is set
+                List<Contract> contractsForJavaFile = FACADE.getContractsForJavaFile(model.getJavaFile());
+                cc = new ContractChooser(FACADE.getEnvironment().getServices(), contractsForJavaFile);
             } catch (ProblemLoaderException e) {
                 e.printStackTrace();
             }