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: package de.uka.ilkd.key.proof.init;
11:
12: import java.io.File;
13: import java.io.FileNotFoundException;
14:
15: import de.uka.ilkd.key.parser.KeYLexer;
16: import de.uka.ilkd.key.parser.KeYParser;
17: import de.uka.ilkd.key.parser.ParserConfig;
18: import de.uka.ilkd.key.parser.ParserMode;
19: import de.uka.ilkd.key.proof.CountingBufferedInputStream;
20: import de.uka.ilkd.key.proof.RuleSource;
21:
22: /**
23: * Used for TESTS ONLY as we allow there to declare program variables global
24: * in rule files .
25: */
26: public class KeYFileForTests extends KeYFile {
27:
28: /** creates a new representation for a given file by indicating a name
29: * and a file representing the physical source of the .key file.
30: */
31: public KeYFileForTests(String name, File file) {
32: super (name, file, null);
33: }
34:
35: /** reads the whole .key file and modifies the initial configuration
36: * assigned to this object according to the given modification strategy.
37: * Throws an exception if no initial configuration has been set yet.
38: */
39: public void read(ModStrategy mod) throws ProofInputException {
40: if (initConfig == null) {
41: throw new IllegalStateException(
42: "KeYFile: InitConfig not set.");
43: }
44: try {
45: final CountingBufferedInputStream cinp = new CountingBufferedInputStream(
46: getNewStream(), monitor, getNumberOfChars() / 100);
47: final ParserConfig pc = new ParserConfig(initConfig
48: .getServices().copy(), initConfig.namespaces()
49: .copy());
50: problemParser = new KeYParser(ParserMode.PROBLEM,
51: new KeYLexer(cinp, null), file.toString(), pc, pc,
52: initConfig.getTaclet2Builder(), initConfig
53: .getTaclets(), initConfig
54: .getActivatedChoices());
55: problemParser.problem();
56: initConfig.setTaclets(problemParser.getTaclets());
57: initConfig.add(problemParser.namespaces(),
58: ModStrategy.MOD_ALL);
59: } catch (antlr.ANTLRException e) {
60: throw new ProofInputException(e);
61: } catch (FileNotFoundException ioe) {
62: throw new ProofInputException(ioe);
63: }
64: }
65:
66: public Includes readIncludes() throws ProofInputException {
67: Includes result = super .readIncludes();
68:
69: //add test LDTs
70: if (result.getLDTIncludes().isEmpty()) {
71: result.put("ldtsForTests", RuleSource
72: .initRuleFile("LDTsForTestsOnly.key"));
73: }
74:
75: return result;
76: }
77: }
|