| Test |
Method name |
Duration |
Result |
| [10] wellFormed.dl,
\forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) ->
boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE
| (java.lang.Object::select(h, o, f)) = null)
|
testSMTLemmaSoundness(String, String)[10] |
3.065s |
passed |
| [11] jdiv.dl,
\forall int divNum; \forall int divDenom;
jdiv(divNum,divDenom) =
\if (divNum >= 0)
\then (div(divNum,divDenom))
\else (div(divNum*(-1),divDenom)*(-1))
|
testSMTLemmaSoundness(String, String)[11] |
3.487s |
passed |
| [12] empty.dl,
\forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false )
|
testSMTLemmaSoundness(String, String)[12] |
3.049s |
passed |
| [13] allLocs.dl,
\forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true )
|
testSMTLemmaSoundness(String, String)[13] |
3.128s |
passed |
| [14] arrayRange.dl,
\forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi;
(elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <->
o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi))
|
testSMTLemmaSoundness(String, String)[14] |
3.008s |
passed |
| [15] seqConcat.dl,
\forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) ->
any::seqGet(seqConcat(s1, s2), i) =
\if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1))))
|
testSMTLemmaSoundness(String, String)[15] |
3.049s |
passed |
| [16] seqLen.dl,
\forall Seq s; seqLen(s)<<Trigger>> >= 0
|
testSMTLemmaSoundness(String, String)[16] |
3.046s |
passed |
| [17] length.dl,
\forall Object o; length(o) >= 0
|
testSMTLemmaSoundness(String, String)[17] |
3.110s |
passed |
| [18] freshLocs.dl,
\forall Heap h; \forall Object o; \forall Field f;
( elementOf(o,f,freshLocs(h))<<Trigger>> <->
o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE )
|
testSMTLemmaSoundness(String, String)[18] |
3.081s |
passed |
| [19] anon.dl,
\forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls;
any::select(anon(h, ls, h2), o, f)<<Trigger>> =
\if(elementOf(o, f, ls) & f != java.lang.Object::<created>
| elementOf(o, f, freshLocs(h)))
\then(any::select(h2, o, f))
\else(any::select(h, o, f))
|
testSMTLemmaSoundness(String, String)[19] |
3.139s |
passed |
| [1] jmod.dl,
\forall int divNum; \forall int divDenom;
jmod(divNum,divDenom) =
divNum + jdiv(divNum,divDenom)*(-1)*divDenom
|
testSMTLemmaSoundness(String, String)[1] |
3.425s |
passed |
| [20] memset.dl,
\forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f;
any::select(memset(h, s, x), o, f)<<Trigger>> =
\if(elementOf(o, f, s) & f != java.lang.Object::<created>)
\then(x)
\else(any::select(h, o, f))
|
testSMTLemmaSoundness(String, String)[20] |
3.096s |
passed |
| [21] store.dl,
\forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v;
any::select(store(h,o,f,v), o2, f2)<<Trigger>> =
\if(o = o2 & f = f2 & f != java.lang.Object::<created>)
\then(v)
\else(any::select(h, o2, f2))
|
testSMTLemmaSoundness(String, String)[21] |
3.002s |
passed |
| [22] seqSub.dl.2,
\forall Seq seq;
\forall int from;
\forall int to;
seqLen(seqSub(seq, from, to)<<Trigger>>)
= \if(from < to)\then(to - from)\else(0)
|
testSMTLemmaSoundness(String, String)[22] |
3.036s |
passed |
| [23] seqSingleton.dl,
\forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x
|
testSMTLemmaSoundness(String, String)[23] |
3.055s |
passed |
| [24] seqSingleton.dl.2,
\forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1
|
testSMTLemmaSoundness(String, String)[24] |
3.116s |
passed |
| [25] null.dl,
\forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null)
|
testSMTLemmaSoundness(String, String)[25] |
3.096s |
passed |
| [2] seqSub.dl,
\forall Seq seq;
\forall int from;
\forall int to;
\forall int idx;
any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx)
= \if(0 <= idx & idx < (to - from))
\then(any::seqGet(seq, idx + from))
\else(seqGetOutside)
|
testSMTLemmaSoundness(String, String)[2] |
3.085s |
passed |
| [3] seqGetOutside.dl,
\forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside )
|
testSMTLemmaSoundness(String, String)[3] |
3.111s |
passed |
| [4] singleton.dl,
\forall Object o; \forall Field f; \forall Object o2; \forall Field f2;
( elementOf(o,f, singleton(o2,f2))<<Trigger>> <->
o = o2 & f = f2 )
|
testSMTLemmaSoundness(String, String)[4] |
3.111s |
passed |
| [5] create.dl,
\forall Heap h; \forall Object o; \forall Object o2; \forall Field f;
any::select(create(h, o), o2, f)<<Trigger>> =
\if(o = o2 & o != null & f = java.lang.Object::<created>)
\then(TRUE)
\else(any::select(h, o2, f))
|
testSMTLemmaSoundness(String, String)[5] |
3.199s |
passed |
| [6] allFields.dl,
\forall Object o; \forall Field f; \forall Object o2;
( elementOf(o,f, allFields(o2))<<Trigger>> <->
o = o2 )
|
testSMTLemmaSoundness(String, String)[6] |
3.102s |
passed |
| [7] seqEmpty.dl,
seqLen(seqEmpty) = 0
|
testSMTLemmaSoundness(String, String)[7] |
3.295s |
passed |
| [8] union.dl,
\forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2;
( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) )
|
testSMTLemmaSoundness(String, String)[8] |
3.104s |
passed |
| [9] seqConcat.dl.2,
\forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2)
|
testSMTLemmaSoundness(String, String)[9] |
3.065s |
passed |