Package: VDMSL

VDMSL

nameinstructionbranchcomplexitylinemethod
VDMSL()
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
getInterpreter()
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
interpret(List, String)
M: 124 C: 0
0%
M: 4 C: 0
0%
M: 3 C: 0
0%
M: 29 C: 0
0%
M: 1 C: 0
0%
parse(List)
M: 135 C: 116
46%
M: 11 C: 11
50%
M: 10 C: 2
17%
M: 26 C: 25
49%
M: 0 C: 1
100%
typeCheck()
M: 139 C: 95
41%
M: 14 C: 12
46%
M: 11 C: 3
21%
M: 28 C: 20
42%
M: 0 C: 1
100%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (c) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.interpreter;
25:
26: import java.io.File;
27: import java.io.FileInputStream;
28: import java.io.FileOutputStream;
29: import java.io.IOException;
30: import java.io.ObjectInputStream;
31: import java.io.ObjectOutputStream;
32: import java.util.List;
33: import java.util.zip.GZIPInputStream;
34: import java.util.zip.GZIPOutputStream;
35:
36: import org.overture.ast.analysis.AnalysisException;
37: import org.overture.ast.lex.Dialect;
38: import org.overture.ast.lex.LexLocation;
39: import org.overture.ast.messages.InternalException;
40: import org.overture.ast.util.modules.ModuleList;
41: import org.overture.config.Settings;
42: import org.overture.interpreter.commands.CommandReader;
43: import org.overture.interpreter.commands.ModuleCommandReader;
44: import org.overture.interpreter.messages.Console;
45: import org.overture.interpreter.runtime.ContextException;
46: import org.overture.interpreter.runtime.ModuleInterpreter;
47: import org.overture.interpreter.util.ExitStatus;
48: import org.overture.interpreter.util.ModuleListInterpreter;
49: import org.overture.parser.lex.LexTokenReader;
50: import org.overture.parser.syntax.ModuleReader;
51: import org.overture.pog.pub.IProofObligationList;
52: import org.overture.typechecker.ModuleTypeChecker;
53: import org.overture.typechecker.TypeChecker;
54:
55: /**
56: * The main class of the VDM-SL parser/checker/interpreter.
57: */
58:
59: public class VDMSL extends VDMJ
60: {
61:         private ModuleListInterpreter modules = new ModuleListInterpreter();
62:
63:         public VDMSL()
64:         {
65:                 Settings.dialect = Dialect.VDM_SL;
66:         }
67:
68:         /**
69:          * @see VDMJ#parse(java.util.List)
70:          */
71:
72:         @Override
73:         public ExitStatus parse(List<File> files)
74:         {
75:                 modules.clear();
76:                 LexLocation.resetLocations();
77:                 int perrs = 0;
78:                 int pwarn = 0;
79:                 long duration = 0;
80:
81:•                for (File file : files)
82:                 {
83:                         ModuleReader reader = null;
84:
85:                         try
86:                         {
87:•                                if (file.getName().endsWith(".lib"))
88:                                 {
89:                                         FileInputStream fis = new FileInputStream(file);
90:                                         GZIPInputStream gis = new GZIPInputStream(fis);
91:                                         ObjectInputStream ois = new ObjectInputStream(gis);
92:
93:                                         ModuleListInterpreter loaded = null;
94:                                         long begin = System.currentTimeMillis();
95:
96:                                         try
97:                                         {
98:                                                 loaded = new ModuleListInterpreter((ModuleList) ois.readObject());
99:                                         } catch (Exception e)
100:                                         {
101:                                                 println(file + " is not a valid VDM-SL library");
102:                                                 perrs++;
103:                                                 continue;
104:                                         } finally
105:                                         {
106:                                                 ois.close();
107:                                         }
108:
109:                                         long end = System.currentTimeMillis();
110:                                         loaded.setLoaded();
111:                                         modules.addAll(loaded);
112:
113:                                         infoln("Loaded " + plural(loaded.size(), "module", "s")
114:                                                         + " from " + file + " in " + (double) (end - begin)
115:                                                         / 1000 + " secs");
116:                                 } else
117:                                 {
118:                                         long before = System.currentTimeMillis();
119:                                         LexTokenReader ltr = new LexTokenReader(file, Settings.dialect, filecharset);
120:                                         reader = new ModuleReader(ltr);
121:                                         modules.addAll(reader.readModules());
122:                                         long after = System.currentTimeMillis();
123:                                         duration += after - before;
124:                                 }
125:                         } catch (InternalException e)
126:                         {
127:                                 println(e.toString());
128:                         } catch (Throwable e)
129:                         {
130:                                 println(e.toString());
131:                                 perrs++;
132:                         }
133:
134:•                        if (reader != null && reader.getErrorCount() > 0)
135:                         {
136:                                 perrs += reader.getErrorCount();
137:                                 reader.printErrors(Console.out);
138:                         }
139:
140:•                        if (reader != null && reader.getWarningCount() > 0)
141:                         {
142:                                 pwarn += reader.getWarningCount();
143:                                 reader.printWarnings(Console.out);
144:                         }
145:                 }
146:
147:                 perrs += modules.combineDefaults();
148:                 int n = modules.notLoaded();
149:
150:•                if (n > 0)
151:                 {
152:                         info("Parsed " + plural(n, "module", "s") + " in "
153:                                         + (double) duration / 1000 + " secs. ");
154:•                        info(perrs == 0 ? "No syntax errors" : "Found "
155:                                         + plural(perrs, "syntax error", "s"));
156:•                        infoln(pwarn == 0 ? "" : " and " + (warnings ? "" : "suppressed ")
157:                                         + plural(pwarn, "warning", "s"));
158:                 }
159:
160:•                return perrs == 0 ? ExitStatus.EXIT_OK : ExitStatus.EXIT_ERRORS;
161:         }
162:
163:         /**
164:          * @see VDMJ#typeCheck()
165:          */
166:
167:         @Override
168:         public ExitStatus typeCheck()
169:         {
170:                 int terrs = 0;
171:                 long before = System.currentTimeMillis();
172:
173:                 try
174:                 {
175:                         TypeChecker typeChecker = new ModuleTypeChecker(modules);
176:                         typeChecker.typeCheck();
177:                 } catch (InternalException e)
178:                 {
179:                         println(e.toString());
180:                 } catch (Throwable e)
181:                 {
182:                         println(e.toString());
183:                         terrs++;
184:                 }
185:
186:                 long after = System.currentTimeMillis();
187:                 terrs += TypeChecker.getErrorCount();
188:
189:•                if (terrs > 0)
190:                 {
191:                         TypeChecker.printErrors(Console.out);
192:                 }
193:
194:                 int twarn = TypeChecker.getWarningCount();
195:
196:•                if (twarn > 0 && warnings)
197:                 {
198:                         TypeChecker.printWarnings(Console.out);
199:                 }
200:
201:                 int n = modules.notLoaded();
202:
203:•                if (n > 0)
204:                 {
205:                         info("Type checked " + plural(n, "module", "s") + " in "
206:                                         + (double) (after - before) / 1000 + " secs. ");
207:•                        info(terrs == 0 ? "No type errors" : "Found "
208:                                         + plural(terrs, "type error", "s"));
209:•                        infoln(twarn == 0 ? "" : " and " + (warnings ? "" : "suppressed ")
210:                                         + plural(twarn, "warning", "s"));
211:                 }
212:
213:•                if (outfile != null && terrs == 0)
214:                 {
215:                         try
216:                         {
217:                                 before = System.currentTimeMillis();
218:                                 FileOutputStream fos = new FileOutputStream(outfile);
219:                                 GZIPOutputStream gos = new GZIPOutputStream(fos);
220:                                 ObjectOutputStream oos = new ObjectOutputStream(gos);
221:
222:                                 oos.writeObject(modules);
223:                                 oos.close();
224:                                 after = System.currentTimeMillis();
225:
226:                                 infoln("Saved " + plural(modules.size(), "module", "s")
227:                                                 + " to " + outfile + " in " + (double) (after - before)
228:                                                 / 1000 + " secs. ");
229:                         } catch (IOException e)
230:                         {
231:                                 infoln("Cannot write " + outfile + ": " + e.getMessage());
232:                                 terrs++;
233:                         }
234:                 }
235:
236:•                if (pog && terrs == 0)
237:                 {
238:                         IProofObligationList list;
239:                         try
240:                         {
241:                                 list = assistantFactory.createModuleListAssistant().getProofObligations(modules);
242:•                                if (list.isEmpty())
243:                                 {
244:                                         println("No proof obligations generated");
245:                                 } else
246:                                 {
247:                                         println("Generated "
248:                                                         + plural(list.size(), "proof obligation", "s")
249:                                                         + ":\n");
250:                                         print(list.toString());
251:                                 }
252:                         } catch (AnalysisException e)
253:                         {
254:                                 println(e.toString());
255:                         }
256:
257:                 }
258:
259:•                return terrs == 0 ? ExitStatus.EXIT_OK : ExitStatus.EXIT_ERRORS;
260:         }
261:
262:         /**
263:          * @see org.overture.interpreter.VDMJ#interpret(List, String)
264:          */
265:
266:         @Override
267:         protected ExitStatus interpret(List<File> filenames, String defaultName)
268:         {
269:                 ModuleInterpreter interpreter = null;
270:
271:                 try
272:                 {
273:                         long before = System.currentTimeMillis();
274:                         interpreter = getInterpreter();
275:                         interpreter.init(null);
276:
277:•                        if (defaultName != null)
278:                         {
279:                                 interpreter.setDefaultName(defaultName);
280:                         }
281:
282:                         long after = System.currentTimeMillis();
283:
284:                         infoln("Initialized " + plural(modules.size(), "module", "s")
285:                                         + " in " + (double) (after - before) / 1000 + " secs. ");
286:                 } catch (ContextException e)
287:                 {
288:                         println("Initialization: " + e);
289:                         e.ctxt.printStackTrace(Console.out, true);
290:                         return ExitStatus.EXIT_ERRORS;
291:                 } catch (Exception e)
292:                 {
293:                         println("Initialization: " + e.getMessage());
294:                         return ExitStatus.EXIT_ERRORS;
295:                 }
296:
297:                 try
298:                 {
299:•                        if (script != null)
300:                         {
301:                                 println(interpreter.execute(script, null).toString());
302:                                 return ExitStatus.EXIT_OK;
303:                         } else
304:                         {
305:                                 infoln("Interpreter started");
306:                                 CommandReader reader = new ModuleCommandReader(interpreter, "> ");
307:                                 return reader.run(filenames);
308:                         }
309:                 } catch (ContextException e)
310:                 {
311:                         println("Execution: " + e);
312:                         e.ctxt.printStackTrace(Console.out, true);
313:                 } catch (Exception e)
314:                 {
315:                         println("Execution: " + e);
316:                 }
317:
318:                 return ExitStatus.EXIT_ERRORS;
319:         }
320:
321:         @Override
322:         public ModuleInterpreter getInterpreter() throws Exception
323:         {
324:                 ModuleInterpreter interpreter = new ModuleInterpreter(modules);
325:                 return interpreter;
326:         }
327: }