diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java index 207e610ab8bd5cac07d9e3b5b8dc2f15775e92e1..ea1d7103486ca32072f2c6d6215c7d072dda94b1 100755 --- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -107,7 +107,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { public void saveInFile(String path) throws FileException { // TODO check if pvspec exists etc. // TODO: Add a field for Hash and check it - FileUtils.saveFile(path + "pvspec", this.spec.getStringSpec ()); + FileUtils.saveFile(path, this.spec.getStringSpec ()); } public Vector getWarnings() { diff --git a/src/proverifspec/ProVerifOutputAnalyzerTest.java b/src/proverifspec/ProVerifOutputAnalyzerTest.java index 1f8700434b0d815120473d1ad7d6dfad73b151c5..ae9de88d04051a057279c02fa762bde23e1f8131 100644 --- a/src/proverifspec/ProVerifOutputAnalyzerTest.java +++ b/src/proverifspec/ProVerifOutputAnalyzerTest.java @@ -57,7 +57,7 @@ public class ProVerifOutputAnalyzerTest { try { String s=""; String sCurrentLine; - br = new BufferedReader(new FileReader("/home/lile/TURTLE/src/proverifspec/typed.txt")); + br = new BufferedReader(new FileReader("proverifspec/typed.txt")); while ((sCurrentLine = br.readLine()) != null) { s= s.concat(sCurrentLine+"\n"); } @@ -111,7 +111,7 @@ public class ProVerifOutputAnalyzerTest { System.out.println("Untyped Tests"); - br = new BufferedReader(new FileReader("/home/lile/TURTLE/src/proverifspec/untyped.txt")); + br = new BufferedReader(new FileReader("proverifspec/untyped.txt")); while ((sCurrentLine = br.readLine()) != null) { s= s.concat(sCurrentLine+"\n"); } diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java index df529de880fccb73d32d333ff636ebaaca635e52..475a8e572c5ccd579fbe25d5dda4050178b479ca 100644 --- a/src/ui/window/JDialogProVerifGeneration.java +++ b/src/ui/window/JDialogProVerifGeneration.java @@ -323,14 +323,30 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac hasError = false; TraceManager.addDev("Thread started"); - + File testFile; try { // Code generation if (jp1.getSelectedIndex() == 0) { jta.append("Generating ProVerif code\n"); testGo(); - + pathCode = code1.getText(); + testFile = new File(pathCode); + if (pathCode.isEmpty() || pathCode.trim().isEmpty()){ + pathCode="pvspec"; + } + if (testFile.isDirectory()){ + if (pathCode.charAt(pathCode.length()-1) != '/'){ + pathCode = pathCode + "/"; + } + pathCode = pathCode+"pvspec"; + } + else { + if (testFile.exists()){ + //Raise error + System.out.println("FILE EXISTS!!!"); + } + } if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachability.isSelected(), translationOfBooleanFunction.isSelected(), typedLanguage.isSelected())) { jta.append("ProVerif code generation done\n"); } else { @@ -342,6 +358,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac else { exe2.setText(pathExecute + " -in pi "); } + exe2.setText(exe2.getText()+pathCode); //if (mgui.gtm.getCheckingWarnings().size() > 0) { jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n"); //} @@ -358,13 +375,13 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac String filename = "pvspec"; String[] args = exe2.getText().split(" "); if (args.length > 3){ - File testFile = new File(args[3]); + testFile = new File(args[3]); if (testFile.isFile()){ filename = ""; } } - cmd = exe2.getText() + pathCode + filename; + cmd = exe2.getText() + filename; jta.append("Executing ProVerif code with command: \n" + cmd + "\n");