Opened 17 years ago

Closed 17 years ago

#56 closed defect (fixed)

mean: null pointer exception

Reported by: zirkel Owned by: ywei
Priority: major Milestone:
Component: front Version: 1.0
Keywords: mean, examples, front, exception, null pointer, verify Cc:

Description

Running verify on meanImpl_2.mmp gives the following:

Exception in thread "main" java.lang.NullPointerException

at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processSpecExpr(ModelBuilder.java:1070)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processExpression(ModelBuilder.java:912)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processBinaryExpr(ModelBuilder.java:937)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processExpression(ModelBuilder.java:892)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processBinaryExpr(ModelBuilder.java:936)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processExpression(ModelBuilder.java:892)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processWhileStmt(ModelBuilder.java:859)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processStatement(ModelBuilder.java:539)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processStatementList(ModelBuilder.java:483)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processFunctionBody(ModelBuilder.java:445)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processFunctions(ModelBuilder.java:420)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processAST(ModelBuilder.java:274)
at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.buildModel(ModelBuilder.java:267)
at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:398)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:506)

Change History (4)

comment:1 by ywei, 17 years ago

Status: newaccepted

comment:2 by Stephen Siegel, 17 years ago

Problem is that during verify, need to ignore the references to "spec" since the spec is not around!

comment:3 by ywei, 17 years ago

Fixed.

comment:4 by ywei, 17 years ago

Resolution: fixed
Status: acceptedclosed
Note: See TracTickets for help on using tickets.