|
| |
|
| java.lang.Object
 junit.framework.TestCase
de.uka.ilkd.key.rule.TestUpdateSimplifier
| TestUpdateSimplifier | | public class TestUpdateSimplifier extends TestCase (Code) | | Class used for testing the simultaneous update simplifier. ATTENTION: If
assertSame is used, do not replace this test with
assertEquals without thinking, as we test here also if the
memory resources are wasted or not.
|
| TestUpdateSimplifier | | public TestUpdateSimplifier(String s)(Code) | | |
| createUpdateTerm | | public Term createUpdateTerm(Location[] locations, Term[] subs)(Code) | | creates an update term where the given locations are updated
this method requires detailed knowledge of the update structure as
the subterms must have the correct order.
Parameters:
locations - the Location operators of the update
Parameters:
subs - the array of Term with the subterms of the locations to be updated, the values and the target term the above described update term |
| setUp | | public void setUp()(Code) | | |
| tearDown | | public void tearDown()(Code) | | |
| testAnonymous1 | | public void testAnonymous1()(Code) | | |
| testAnonymous2 | | public void testAnonymous2()(Code) | | |
| testApplicationOnAttributeNoneSim | | public void testApplicationOnAttributeNoneSim()(Code) | | |
| testApplicationOnAttributeSim | | public void testApplicationOnAttributeSim()(Code) | | |
| testApplyArrayAccessOnShadowedArray | | public void testApplyArrayAccessOnShadowedArray()(Code) | | |
| testApplyAttributeOnShadowedAttribute | | public void testApplyAttributeOnShadowedAttribute()(Code) | | |
| testApplyOnAttribute | | public void testApplyOnAttribute()(Code) | | |
| testApplyShadowedAttributeOnAttribute | | public void testApplyShadowedAttributeOnAttribute()(Code) | | |
| testAttributeEvaluateSubsFirst | | public void testAttributeEvaluateSubsFirst()(Code) | | |
| testAttributeRule3 | | public void testAttributeRule3()(Code) | | |
| testAttributeRule4 | | public void testAttributeRule4()(Code) | | |
| testBaseArrayApplications | | public void testBaseArrayApplications()(Code) | | tests the application of
- {a[i] := t} a[i]
- {a[i] := t} a[j]
- {a[i] := t} b[i] (a compatible to b)
- {a[i] := t} b[j] (a compatible to b)
- {a[i] := t} c[j] (a not compatible to c)
- {a[i] := t} o.a
- {a[i] := t} i
|
| testBaseAttributeApplications | | public void testBaseAttributeApplications()(Code) | | tests the application of
- {o.a := t} o.a
- {o.a := t} u.a (u compatible to o)
- {o.a := t} r.a (r not compatible to o)
- {o.a := t} i
- {o.a := t} a[i]
|
| testBaseLocalVariableApplications | | public void testBaseLocalVariableApplications()(Code) | | tests the application of
- {o := t} o
- {o := t} u
- {o := t} o.a
- {o := t} u.a
- {o := t} r.a
- {a := b} a[i]
- {a := b} c[i]
- {i := j} a[i]
|
| testBasicRules | | public void testBasicRules()(Code) | | |
| testBugInUStarComputation | | public void testBugInUStarComputation()(Code) | | |
| testDeletion | | public void testDeletion()(Code) | | |
| testDeletion10 | | public void testDeletion10()(Code) | | |
| testDeletion11 | | public void testDeletion11()(Code) | | |
| testDeletion12 | | public void testDeletion12()(Code) | | |
| testDeletion3 | | public void testDeletion3()(Code) | | |
| testDeletion4 | | public void testDeletion4()(Code) | | |
| testDeletion5 | | public void testDeletion5()(Code) | | |
| testDeletion6 | | public void testDeletion6()(Code) | | |
| testDeletion7 | | public void testDeletion7()(Code) | | |
| testDeletion8 | | public void testDeletion8()(Code) | | |
| testDeletion9 | | public void testDeletion9()(Code) | | |
| testDeletionStrategy | | public void testDeletionStrategy()(Code) | | |
| testHeapDependentFunctions1 | | public void testHeapDependentFunctions1()(Code) | | |
| testHeapDependentFunctions2 | | public void testHeapDependentFunctions2()(Code) | | |
| testMergeSingleUpdates | | public void testMergeSingleUpdates()(Code) | | tests the application of
- {a := b} {a[i] := o} <> true
- {i := j} {a[i] := o} <> true
- {a[i] := t} {a[i] := o} <> true
- {a[i] := t} {b[i] := o} <> true (a, b compatible)
- {a[i] := t} {c[i] := o} <> true (a, c not compatible)
- {a[i] := t} {o := a[i]} <> true
- {a[i] := t} {o := a[j]} <> true
- {o.a := t} {o.a := o } <> true
- {o.a := t} {o.a.a := o} <> true
- {o.a := t} {o.a.a := o.a} <> true
- {o.a := t} {u.a := u.a} <> true
- {o.a := t} {r.a := r.a} <> true
- {o.a := t} {r.a.a := o} <> true
|
| testNoDeletionIfAppliedOnNonRigidFunction | | public void testNoDeletionIfAppliedOnNonRigidFunction()(Code) | | |
| testQuantified1 | | public void testQuantified1()(Code) | | |
| testQuantified2 | | public void testQuantified2()(Code) | | |
| testQuantified3 | | public void testQuantified3()(Code) | | |
| testQuantified4 | | public void testQuantified4()(Code) | | |
| testQuantified5 | | public void testQuantified5()(Code) | | |
| testShadowOnShadowSameTransactionNr | | public void testShadowOnShadowSameTransactionNr()(Code) | | |
| testShadowedArraySimplificationRule | | public void testShadowedArraySimplificationRule()(Code) | | |
| testSimultaneousArrayApplications | | public void testSimultaneousArrayApplications()(Code) | | tests the application of
- {a[i] := t, a[j] :=u} a[i]
- {a[j] := t, a[i] :=u} a[i]
- {a[j] := t, a[i] := o, a[m] := u} a[i]
- {a[i] := u, a[m] := u} a[i]
|
| testSimultaneousUpdateEquality | | public void testSimultaneousUpdateEquality()(Code) | | |
| testStaticAttributes | | public void testStaticAttributes()(Code) | | tests the application of
- {o.spv:=u, t.spv:=i} u.spv
|
| xtestBugInDeleteTrivialUpdates | | public void xtestBugInDeleteTrivialUpdates()(Code) | | |
|
|
|