id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
25	SyntaxException when verifying matmat-seq.mmp	zirkel	zirkel	"When running verify on examples/matmat/matmat-seq.mmp, a SyntaxException is generated.  It may be due to passing array c, an output variable (which is supposed to be written, but not read), as an argument to a function.

The exception is:

Exception in thread ""main"" edu.udel.cis.vsl.minimp.model.IF.SyntaxException: Syntax error in line 30 column 19 through line 30 column 23:
c[i]):
c[i]
Argument 2 of function call not in read scope of calling function main
	at edu.udel.cis.vsl.minimp.model.impl.statement.InvocationStatement.<init>(InvocationStatement.java:63)
	at edu.udel.cis.vsl.minimp.model.impl.Model.newInvocationStatement(Model.java:309)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processInvocationStmt(ModelBuilder.java:673)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processStatement(ModelBuilder.java:489)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processCompoundStmt(ModelBuilder.java:578)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processStatement(ModelBuilder.java:473)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processWhileStmt(ModelBuilder.java:810)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processStatement(ModelBuilder.java:505)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processStatementList(ModelBuilder.java:449)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processFunctionBody(ModelBuilder.java:411)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processFunctions(ModelBuilder.java:386)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.processAST(ModelBuilder.java:244)
	at edu.udel.cis.vsl.minimp.front.minimp.ModelBuilder.buildModel(ModelBuilder.java:237)
	at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:273)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:371)
"	defect	closed	minor		examples	1.0	fixed