id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
131	Extra assumptions in implementation not used	zirkel	Stephen Siegel	"When the implementation has inputs that are not in the specification, any assumptions on these input variables are not used.  For example, in diffusion_par.mmp there is an input variable m:

{{{
input int m {m >= 2 && m <= nx && m == ((PID+1)*nx)/NPROCS - (PID*nx)/NPROCS+2};
}}}

This m is then used as the extent of an array.  The code passes verify, but when used as the impl in compare mode it returns the exception:

{{{
Exception in thread ""main"" edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at diffusion_par.mmp 32.5--32.6: ""m""
Cannot prove that extent 0 of array is nonnegative
}}}"	defect	closed	major		semantics	1.0	fixed	input, assumption, extend, impl, array, diffusion