Package: VDMSL

VDMSL

nameinstructionbranchcomplexitylinemethod
VDMSL()
M: 0 C: 14
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
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: 140 C: 0
0%
M: 8 C: 0
0%
M: 5 C: 0
0%
M: 33 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:                 System.setProperty("VDM_SL", "1");
67:         }
68:
69:         /**
70:          * @see VDMJ#parse(java.util.List)
71:          */
72:
73:         @Override
74:         public ExitStatus parse(List<File> files)
75:         {
76:                 modules.clear();
77:                 LexLocation.resetLocations();
78:                 int perrs = 0;
79:                 int pwarn = 0;
80:                 long duration = 0;
81:
82:•                for (File file : files)
83:                 {
84:                         ModuleReader reader = null;
85:
86:                         try
87:                         {
88:•                                if (file.getName().endsWith(".lib"))
89:                                 {
90:                                         FileInputStream fis = new FileInputStream(file);
91:                                         GZIPInputStream gis = new GZIPInputStream(fis);
92:                                         ObjectInputStream ois = new ObjectInputStream(gis);
93:
94:                                         ModuleListInterpreter loaded = null;
95:                                         long begin = System.currentTimeMillis();
96:
97:                                         try
98:                                         {
99:                                                 loaded = new ModuleListInterpreter((ModuleList) ois.readObject());
100:                                         } catch (Exception e)
101:                                         {
102:                                                 println(file + " is not a valid VDM-SL library");
103:                                                 perrs++;
104:                                                 continue;
105:                                         } finally
106:                                         {
107:                                                 ois.close();
108:                                         }
109:
110:                                         long end = System.currentTimeMillis();
111:                                         loaded.setLoaded();
112:                                         modules.addAll(loaded);
113:
114:                                         infoln("Loaded " + plural(loaded.size(), "module", "s")
115:                                                         + " from " + file + " in " + (double) (end - begin)
116:                                                         / 1000 + " secs");
117:                                 } else
118:                                 {
119:                                         long before = System.currentTimeMillis();
120:                                         LexTokenReader ltr = new LexTokenReader(file, Settings.dialect, filecharset);
121:                                         reader = new ModuleReader(ltr);
122:                                         modules.addAll(reader.readModules());
123:                                         long after = System.currentTimeMillis();
124:                                         duration += after - before;
125:                                 }
126:                         } catch (InternalException e)
127:                         {
128:                                 println(e.toString());
129:                         } catch (Throwable e)
130:                         {
131:                                 println(e.toString());
132:                                 perrs++;
133:                         }
134:
135:•                        if (reader != null && reader.getErrorCount() > 0)
136:                         {
137:                                 perrs += reader.getErrorCount();
138:                                 reader.printErrors(Console.out);
139:                         }
140:
141:•                        if (reader != null && reader.getWarningCount() > 0)
142:                         {
143:                                 pwarn += reader.getWarningCount();
144:                                 reader.printWarnings(Console.out);
145:                         }
146:                 }
147:
148:                 perrs += modules.combineDefaults();
149:                 int n = modules.notLoaded();
150:
151:•                if (n > 0)
152:                 {
153:                         info("Parsed " + plural(n, "module", "s") + " in "
154:                                         + (double) duration / 1000 + " secs. ");
155:•                        info(perrs == 0 ? "No syntax errors" : "Found "
156:                                         + plural(perrs, "syntax error", "s"));
157:•                        infoln(pwarn == 0 ? "" : " and " + (warnings ? "" : "suppressed ")
158:                                         + plural(pwarn, "warning", "s"));
159:                 }
160:
161:•                return perrs == 0 ? ExitStatus.EXIT_OK : ExitStatus.EXIT_ERRORS;
162:         }
163:
164:         /**
165:          * @see VDMJ#typeCheck()
166:          */
167:
168:         @Override
169:         public ExitStatus typeCheck()
170:         {
171:                 int terrs = 0;
172:                 long before = System.currentTimeMillis();
173:
174:                 try
175:                 {
176:                         TypeChecker typeChecker = new ModuleTypeChecker(modules);
177:                         typeChecker.typeCheck();
178:                 } catch (InternalException e)
179:                 {
180:                         println(e.toString());
181:                 } catch (Throwable e)
182:                 {
183:                         println(e.toString());
184:                         terrs++;
185:                 }
186:
187:                 long after = System.currentTimeMillis();
188:                 terrs += TypeChecker.getErrorCount();
189:
190:•                if (terrs > 0)
191:                 {
192:                         TypeChecker.printErrors(Console.out);
193:                 }
194:
195:                 int twarn = TypeChecker.getWarningCount();
196:
197:•                if (twarn > 0 && warnings)
198:                 {
199:                         TypeChecker.printWarnings(Console.out);
200:                 }
201:
202:                 int n = modules.notLoaded();
203:
204:•                if (n > 0)
205:                 {
206:                         info("Type checked " + plural(n, "module", "s") + " in "
207:                                         + (double) (after - before) / 1000 + " secs. ");
208:•                        info(terrs == 0 ? "No type errors" : "Found "
209:                                         + plural(terrs, "type error", "s"));
210:•                        infoln(twarn == 0 ? "" : " and " + (warnings ? "" : "suppressed ")
211:                                         + plural(twarn, "warning", "s"));
212:                 }
213:
214:•                if (outfile != null && terrs == 0)
215:                 {
216:                         try
217:                         {
218:                                 before = System.currentTimeMillis();
219:                                 FileOutputStream fos = new FileOutputStream(outfile);
220:                                 GZIPOutputStream gos = new GZIPOutputStream(fos);
221:                                 ObjectOutputStream oos = new ObjectOutputStream(gos);
222:
223:                                 oos.writeObject(modules);
224:                                 oos.close();
225:                                 after = System.currentTimeMillis();
226:
227:                                 infoln("Saved " + plural(modules.size(), "module", "s")
228:                                                 + " to " + outfile + " in " + (double) (after - before)
229:                                                 / 1000 + " secs. ");
230:                         } catch (IOException e)
231:                         {
232:                                 infoln("Cannot write " + outfile + ": " + e.getMessage());
233:                                 terrs++;
234:                         }
235:                 }
236:
237:•                if (pog && terrs == 0)
238:                 {
239:                         IProofObligationList list;
240:                         try
241:                         {
242:                                 list = assistantFactory.createModuleListAssistant().getProofObligations(modules);
243:•                                if (list.isEmpty())
244:                                 {
245:                                         println("No proof obligations generated");
246:                                 } else
247:                                 {
248:                                         println("Generated "
249:                                                         + plural(list.size(), "proof obligation", "s")
250:                                                         + ":\n");
251:                                         print(list.toString());
252:                                 }
253:                         } catch (AnalysisException e)
254:                         {
255:                                 println(e.toString());
256:                         }
257:
258:                 }
259:
260:•                return terrs == 0 ? ExitStatus.EXIT_OK : ExitStatus.EXIT_ERRORS;
261:         }
262:
263:         /**
264:          * @see org.overture.interpreter.VDMJ#interpret(List, String)
265:          */
266:
267:         @Override
268:         protected ExitStatus interpret(List<File> filenames, String defaultName)
269:         {
270:                 ModuleInterpreter interpreter = null;
271:
272:                 try
273:                 {
274:                         long before = System.currentTimeMillis();
275:                         interpreter = getInterpreter();
276:                         interpreter.init(null);
277:
278:•                        if (defaultName != null)
279:                         {
280:                                 interpreter.setDefaultName(defaultName);
281:                         }
282:
283:                         long after = System.currentTimeMillis();
284:
285:                         infoln("Initialized " + plural(modules.size(), "module", "s")
286:                                         + " in " + (double) (after - before) / 1000 + " secs. ");
287:                 } catch (ContextException e)
288:                 {
289:                         println("Initialization: " + e);
290:                         
291:•                        if (e.isStackOverflow())
292:                         {
293:                                 e.ctxt.printStackFrames(Console.out);
294:                         }
295:                         else
296:                         {
297:                                 e.ctxt.printStackTrace(Console.out, true);
298:                         }
299:                         
300:                         return ExitStatus.EXIT_ERRORS;
301:                 } catch (Exception e)
302:                 {
303:                         println("Initialization: " + e.getMessage());
304:                         return ExitStatus.EXIT_ERRORS;
305:                 }
306:
307:                 try
308:                 {
309:•                        if (script != null)
310:                         {
311:                                 println(interpreter.execute(script, null).toString());
312:                                 return ExitStatus.EXIT_OK;
313:                         } else
314:                         {
315:                                 infoln("Interpreter started");
316:                                 CommandReader reader = new ModuleCommandReader(interpreter, "> ");
317:                                 return reader.run(filenames);
318:                         }
319:                 } catch (ContextException e)
320:                 {
321:                         println("Execution: " + e);
322:                         
323:•                        if (e.isStackOverflow())
324:                         {
325:                                 e.ctxt.printStackFrames(Console.out);
326:                         }
327:                         else
328:                         {
329:                                 e.ctxt.printStackTrace(Console.out, true);
330:                         }
331:                 } catch (Exception e)
332:                 {
333:                         println("Execution: " + e);
334:                 }
335:
336:                 return ExitStatus.EXIT_ERRORS;
337:         }
338:
339:         @Override
340:         public ModuleInterpreter getInterpreter() throws Exception
341:         {
342:                 ModuleInterpreter interpreter = new ModuleInterpreter(modules);
343:                 return interpreter;
344:         }
345: }