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:
11: package de.uka.ilkd.key.unittest.cogent;
12:
13: import de.uka.ilkd.key.logic.Term;
14:
15: public class CogentResult {
16:
17: private boolean valid;
18: private boolean error;
19: private String counterEx = "";
20:
21: public CogentResult(String res) {
22: valid = (res.indexOf("(valid)") != -1 || res.indexOf("=") == -1);
23: error = (res.indexOf("error") != -1);
24: if (!valid && !error) {
25: if (res.indexOf("(not valid)") == -1) {
26: counterEx = res;
27: } else {
28: counterEx = res
29: .substring(res.indexOf("(not valid)") + 12);
30: }
31: }
32: }
33:
34: public boolean valid() {
35: return valid;
36: }
37:
38: public boolean error() {
39: return error;
40: }
41:
42: public int getValueForTerm(Term t, CogentTranslation ct)
43: throws CogentException {
44: String loc = ct.translate(t);
45: String lineSeparator = System.getProperty("line.separator");
46: int index = counterEx.indexOf(loc);
47: if (index != -1) {
48: index = counterEx.indexOf("=", index);
49: return Integer.parseInt(counterEx.substring(index + 1,
50: counterEx.indexOf(lineSeparator, index)));
51: } else {
52: return 3;
53: //throw new CogentException("Term not found");
54: }
55: }
56:
57: }
|