id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
104	cast error in symbolic package	Stephen Siegel		"Run any of the tests and cast exception is thrown:

{{{
java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.Double
	at edu.udel.cis.vsl.minimp.symbolic.expression.SymConcreteValue.<init>(SymConcreteValue.java:42)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.integerLiteral(SymUniverse.java:324)
	at edu.udel.cis.vsl.minimp.dynamic.impl.value.ValueFactory.<init>(ValueFactory.java:89)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.<init>(DynamicFactory.java:63)
	at edu.udel.cis.vsl.minimp.dynamic.DynamicModule.newDynamicFactory(DynamicModule.java:10)
	at edu.udel.cis.vsl.minimp.verify.std.StandardVerificationFactory.newValueFactory(StandardVerificationFactory.java:51)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:70)
	at edu.udel.cis.vsl.minimp.test.SimpleArrayTest.testVerifySpec(SimpleArrayTest.java:75)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:73)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:46)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:180)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:41)
	at org.junit.runners.ParentRunner$1.evaluate(ParentRunner.java:173)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:220)
	at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:46)
	at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)
}}}

Offending code seems to be here in {{{SymConcreteValue.java}}}:



{{{
	public SymConcreteValue(SymType type, Object value)
	{
		super(type);
		this.concreteValue = value;
		if(!((SymSimpleType)type instanceof SymBoolean))
		{
			if((SymSimpleType)type instanceof SymInteger)
			{
				if(((Integer)value).intValue() == 0)
				{
					isZero = true;
					isOne = false;
				}
				else if(((Integer)value).intValue() == 1)
				{
					isOne = true;
					isZero = false;
				}
				else
				{
					isZero = false;
					isOne = false;
				}
			}
			else
			{
				if(((Double)value).doubleValue() == 0.0)
				{
					isZero = true;
					isOne = false;
				}
}}}"	defect	closed	major		symbolic	1.0	fixed	symbolic cast integer double