fix file output

jayhorn · Jun 28, 2016 · 5401157 · 5401157
1 parent 784ce49
commit 5401157
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 9 deletions.
diff --git a/jayhorn/src/main/java/jayhorn/Main.java b/jayhorn/src/main/java/jayhorn/Main.java
@@ -64,11 +64,15 @@ public static void main(String[] args) {
 				String outName = null;
 				if (outDir!=null) {
 					String in = Options.v().getJavaInput();
+					if (in.endsWith("/"))
+						in = in.substring(0, in.length()-1);
 					outName = in.substring(in.lastIndexOf('/'), in.length()).replace(".java", "").replace(".class", "");
+					if (outName.equals(""))
+						outName = "noname";
 				}
 				SootToCfg soot2cfg = new SootToCfg(true, false, MemModel.PullPush, outDir, outName);
 				soot2cfg.run(Options.v().getJavaInput(), Options.v().getClasspath());			
-				Checker checker = new Checker(factory);
+				Checker checker = new Checker(factory, outDir + outName + ".horn");
 				System.out.println( "\t \t  ----------- ");
 				System.out.println("\t Hornify and check  ... " + Options.v().getJavaInput());
 				System.out.println( "\t \t  ----------- \n");

diff --git a/jayhorn/src/main/java/jayhorn/checker/Checker.java b/jayhorn/src/main/java/jayhorn/checker/Checker.java
@@ -101,11 +101,17 @@ public String toString() {
 	}
 
 	private final ProverFactory factory;
+	private final String hornOut;
 
 	public Checker(ProverFactory fac) {
-		this.factory = fac;
+		this(fac,null);
 	}
 
+	public Checker(ProverFactory fac, String hornOut) {
+		this.factory = fac;
+		this.hornOut = hornOut;
+	}
+
 	private final Map<CfgBlock, HornPredicate> blockPredicates = new LinkedHashMap<CfgBlock, HornPredicate>();
 	private Map<String, MethodContract> methodContracts = new LinkedHashMap<String, MethodContract>();
 	private Map<ClassVariable, Integer> typeIds = new LinkedHashMap<ClassVariable, Integer>();
@@ -750,13 +756,8 @@ public boolean checkProgram(Program program) {
 			}
 
 			// write Horn clauses to file
-			String out = jayhorn.Options.v().getOut();
-			if(out != null) {
-				if (!out.endsWith("/"))
-					out += "/";
-				String in = Options.v().getJavaInput();
-				String outName = in.substring(in.lastIndexOf('/'), in.length()).replace(".java", "").replace(".class", "");
-				Path file = Paths.get(out+outName+".horn");
+			if(hornOut != null) {
+				Path file = Paths.get(hornOut);
 				LinkedList<String> it = new LinkedList<String>();
 				for (ProverHornClause clause : clauses)
 					it.add("\t\t" + clause);