01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: /*
10: * Created on 18.12.2004
11: */
12: package de.uka.ilkd.key.util;
13:
14: import java.io.File;
15:
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.proof.Proof;
18: import de.uka.ilkd.key.proof.ProofAggregate;
19: import de.uka.ilkd.key.proof.init.*;
20:
21: /**
22: * @author bubel
23: *
24: * TODO To change the template for this generated type comment go to
25: * Window - Preferences - Java - Code Style - Code Templates
26: */
27: public class HelperClassForTests {
28:
29: private static Profile JUNIT_PROFILE = new JUnitTestProfile();
30:
31: public HelperClassForTests() {
32:
33: }
34:
35: public ProofAggregate parse(File file) {
36: return parse(file, JUNIT_PROFILE);
37: }
38:
39: public ProofAggregate parse(File file, Profile profile) {
40: ProblemInitializer pi = null;
41: ProofAggregate result = null;
42:
43: try {
44: KeYUserProblemFile po = new KeYUserProblemFile(
45: "UpdatetermTest", file, null, false);
46: pi = new ProblemInitializer(profile);
47: pi.startProver(po, po);
48: result = po.getPO();
49:
50: } catch (Exception e) {
51: System.err.println("Exception occurred while parsing "
52: + file + "\n");
53: e.printStackTrace();
54: System.exit(-1);
55: }
56: return result;
57: }
58:
59: public ProofAggregate parseThrowException(File file)
60: throws ProofInputException {
61: return parseThrowException(file, JUNIT_PROFILE);
62: }
63:
64: public ProofAggregate parseThrowException(File file, Profile profile)
65: throws ProofInputException {
66: KeYUserProblemFile po = new KeYUserProblemFile(
67: "UpdatetermTest", file, null, false);
68: ProblemInitializer pi = new ProblemInitializer(profile);
69: pi.startProver(po, po);
70: return po.getPO();
71: }
72:
73: public Term extractProblemTerm(Proof p) {
74: return p.root().sequent().succedent().iterator().next()
75: .formula();
76: }
77:
78: }
|