Opened 16 years ago

Closed 16 years ago

#104 closed defect (fixed)

cast error in symbolic package

Reported by: Stephen Siegel Owned by:
Priority: major Milestone:
Component: symbolic Version: 1.0
Keywords: symbolic cast integer double Cc:

Description

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;
				}

Change History (1)

comment:1 by ywei, 16 years ago

Resolution: fixed
Status: newclosed

Bug fixed. I removed the primitive types from the type table but I still tried to get them from the type table in some methods in symbolic universe.

Note: See TracTickets for help on using tickets.