Skip to content

Instantly share code, notes, and snippets.

@romac

romac/last.log Secret

Last active October 2, 2017 21:12
Show Gist options
  • Save romac/2c93baaec63617a00a180cb7d8dfdc42 to your computer and use it in GitHub Desktop.
Save romac/2c93baaec63617a00a180cb7d8dfdc42 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
last.log
def a: Object = {
Foo(Adt(1072, Nil()), A())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
}
{
Foo(Adt(1072, Nil()), A())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
} is of type <untyped>
Foo(Adt(1072, Nil()), A()) is of type <untyped>
Adt(1072, Nil()) is of type Adt
1072 is of type BigInt
Nil() is of type Nil
A() is of type A because Foo was instantiated with with type (Type,Object) => Object
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
} is of type (Object) => Boolean
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
})) is of type Boolean
getType(res) is of type Type
res is of type Object because getType was instantiated with with type (Object) => Type
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
})) is of type Boolean
tp1.isInstanceOf[Class] is of type Boolean
tp1 is of type Type
tp1.asInstanceOf[Class].id ≠ 1074 is of type Boolean
tp1.asInstanceOf[Class].id == 1074 is of type Boolean
tp1.asInstanceOf[Class].id is of type BigInt
tp1.asInstanceOf[Class] is of type Class
tp1 is of type Type
1074 is of type BigInt
tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}) is of type Boolean
tp1.isInstanceOf[Bot] is of type Boolean
tp1 is of type Type
if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
} is of type Boolean
tp1.isInstanceOf[Class] is of type Boolean
tp1 is of type Type
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true is of type Boolean
tp1.asInstanceOf[Class].id == 1074 is of type Boolean
tp1.asInstanceOf[Class].id is of type BigInt
tp1.asInstanceOf[Class] is of type Class
tp1 is of type Type
1074 is of type BigInt
tp1.asInstanceOf[Class].id == 1075 && true is of type Boolean
tp1.asInstanceOf[Class].id == 1075 is of type Boolean
tp1.asInstanceOf[Class].id is of type BigInt
tp1.asInstanceOf[Class] is of type Class
tp1 is of type Type
1075 is of type BigInt
true is of type Boolean
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil()) is of type Boolean
¬tp1.isInstanceOf[Adt] is of type Boolean
tp1.isInstanceOf[Adt] is of type Boolean
tp1 is of type Type
¬tp1.isInstanceOf[Tuple] is of type Boolean
tp1.isInstanceOf[Tuple] is of type Boolean
tp1 is of type Type
¬tp1.isInstanceOf[Function] is of type Boolean
tp1.isInstanceOf[Function] is of type Boolean
tp1 is of type Type
tp1 == Class(1074, Nil()) is of type Boolean
tp1 is of type Type
Class(1074, Nil()) is of type Class
1074 is of type BigInt
Nil() is of type Nil
def b: Object = {
Foo(Adt(1073, Nil()), B())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
}
{
Foo(Adt(1073, Nil()), B())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
} is of type <untyped>
Foo(Adt(1073, Nil()), B()) is of type <untyped>
Adt(1073, Nil()) is of type Adt
1073 is of type BigInt
Nil() is of type Nil
B() is of type B because Foo was instantiated with with type (Type,Object) => Object
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
} is of type (Object) => Boolean
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
})) is of type Boolean
getType(res) is of type Type
res is of type Object because getType was instantiated with with type (Object) => Type
tp1.isInstanceOf[Class] && tp1.asInstanceOf[Class].id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
})) is of type Boolean
tp1.isInstanceOf[Class] is of type Boolean
tp1 is of type Type
tp1.asInstanceOf[Class].id ≠ 1074 is of type Boolean
tp1.asInstanceOf[Class].id == 1074 is of type Boolean
tp1.asInstanceOf[Class].id is of type BigInt
tp1.asInstanceOf[Class] is of type Class
tp1 is of type Type
1074 is of type BigInt
tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}) is of type Boolean
tp1.isInstanceOf[Bot] is of type Boolean
tp1 is of type Type
if (tp1.isInstanceOf[Class]) {
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
} is of type Boolean
tp1.isInstanceOf[Class] is of type Boolean
tp1 is of type Type
tp1.asInstanceOf[Class].id == 1074 || tp1.asInstanceOf[Class].id == 1075 && true is of type Boolean
tp1.asInstanceOf[Class].id == 1074 is of type Boolean
tp1.asInstanceOf[Class].id is of type BigInt
tp1.asInstanceOf[Class] is of type Class
tp1 is of type Type
1074 is of type BigInt
tp1.asInstanceOf[Class].id == 1075 && true is of type Boolean
tp1.asInstanceOf[Class].id == 1075 is of type Boolean
tp1.asInstanceOf[Class].id is of type BigInt
tp1.asInstanceOf[Class] is of type Class
tp1 is of type Type
1075 is of type BigInt
true is of type Boolean
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil()) is of type Boolean
¬tp1.isInstanceOf[Adt] is of type Boolean
tp1.isInstanceOf[Adt] is of type Boolean
tp1 is of type Type
¬tp1.isInstanceOf[Tuple] is of type Boolean
tp1.isInstanceOf[Tuple] is of type Boolean
tp1 is of type Type
¬tp1.isInstanceOf[Function] is of type Boolean
tp1.isInstanceOf[Function] is of type Boolean
tp1 is of type Type
tp1 == Class(1074, Nil()) is of type Boolean
tp1 is of type Type
Class(1074, Nil()) is of type Class
1074 is of type BigInt
Nil() is of type Nil
[ Info ] - Now solving 'postcondition' VC for a @?:?...
Exception in thread "main" java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: inox.ast.TypeOps$TypeErrorException: Type error: {
Foo(Adt(1072, Nil()), A())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
{
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1074 || {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
}, expected Object, found <untyped>
at java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:1006)
at stainless.frontend.CallBackWithRegistry$$anonfun$join$1.apply(CallBackWithRegistry.scala:49)
at stainless.frontend.CallBackWithRegistry$$anonfun$join$1.apply(CallBackWithRegistry.scala:49)
at scala.collection.immutable.List.foreach(List.scala:381)
at scala.collection.generic.TraversableForwarder$class.foreach(TraversableForwarder.scala:35)
at scala.collection.mutable.ListBuffer.foreach(ListBuffer.scala:45)
at stainless.frontend.CallBackWithRegistry$class.join(CallBackWithRegistry.scala:49)
at stainless.verification.VerificationCallBack.join(VerificationCallBack.scala:11)
at stainless.frontend.MasterCallBack$$anonfun$join$1.apply(CallBack.scala:54)
at stainless.frontend.MasterCallBack$$anonfun$join$1.apply(CallBack.scala:54)
at scala.collection.immutable.List.foreach(List.scala:381)
at stainless.frontend.MasterCallBack.join(CallBack.scala:54)
at stainless.frontend.Frontend.join(Frontend.scala:40)
at stainless.MainHelpers$class.main(MainHelpers.scala:94)
at stainless.Main$.main(Main.scala:3)
at stainless.Main.main(Main.scala)
Caused by: java.lang.RuntimeException: java.lang.RuntimeException: inox.ast.TypeOps$TypeErrorException: Type error: {
Foo(Adt(1072, Nil()), A())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
{
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1074 || {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
}, expected Object, found <untyped>
at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
at java.lang.reflect.Constructor.newInstance(Constructor.java:423)
at java.util.concurrent.ForkJoinTask.getThrowableException(ForkJoinTask.java:593)
at java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:1005)
... 15 more
Caused by: java.lang.RuntimeException: inox.ast.TypeOps$TypeErrorException: Type error: {
Foo(Adt(1072, Nil()), A())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
{
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1074 || {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
}, expected Object, found <untyped>
at java.util.concurrent.ForkJoinTask$AdaptedCallable.exec(ForkJoinTask.java:1431)
at java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:289)
at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1056)
at java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1692)
at java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:157)
Caused by: inox.ast.TypeOps$TypeErrorException: Type error: {
Foo(Adt(1072, Nil()), A())
} ensuring {
(res: Object) => {
val tp1: Type = getType(res)
tp1.isInstanceOf[Class] && {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id ≠ 1074 && (tp1.isInstanceOf[Bot] || (if (tp1.isInstanceOf[Class]) {
{
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1074 || {
assert(tp1.isInstanceOf[Class], "Cast error")
tp1.asInstanceOf[Class]
}.id == 1075 && true
} else {
¬tp1.isInstanceOf[Adt] && ¬tp1.isInstanceOf[Tuple] && ¬tp1.isInstanceOf[Function] && tp1 == Class(1074, Nil())
}))
}
}, expected Object, found <untyped>
at inox.ast.TypeOps$TypeErrorException$.apply(TypeOps.scala:17)
at inox.ast.TypeOps$class.typeCheck(TypeOps.scala:278)
at inox.ast.SimpleSymbols$SimpleSymbols.typeCheck(SimpleSymbols.scala:12)
at inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormed$2.apply(Definitions.scala:180)
at inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormed$2.apply(Definitions.scala:179)
at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
at scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
at inox.ast.Definitions$AbstractSymbols$class.ensureWellFormed(Definitions.scala:179)
at inox.ast.SimpleSymbols$SimpleSymbols.ensureWellFormed$lzycompute(SimpleSymbols.scala:12)
at inox.ast.SimpleSymbols$SimpleSymbols.ensureWellFormed(SimpleSymbols.scala:12)
at inox.solvers.unrolling.AbstractUnrollingSolver$class.assertCnstr(UnrollingSolver.scala:132)
at inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$3.inox$tip$TipDebugger$$super$assertCnstr(SolverFactory.scala:122)
at inox.tip.TipDebugger$class.assertCnstr(TipDebugger.scala:51)
at inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$3.assertCnstr(SolverFactory.scala:122)
at inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$3.assertCnstr(SolverFactory.scala:122)
at stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:107)
at stainless.verification.VerificationChecker$Checker$1.checkVC(VerificationChecker.scala:167)
at stainless.verification.VerificationChecker$$anonfun$5.apply(VerificationChecker.scala:82)
at stainless.verification.VerificationChecker$$anonfun$5.apply(VerificationChecker.scala:81)
at scala.collection.immutable.Stream$StreamWithFilter.scala$collection$immutable$Stream$StreamWithFilter$$tailMap$1(Stream.scala:541)
at scala.collection.immutable.Stream$StreamWithFilter.map(Stream.scala:546)
at stainless.verification.VerificationChecker$class.checkVCs(VerificationChecker.scala:81)
at stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:167)
at stainless.verification.VerificationChecker$class.verify(VerificationChecker.scala:58)
at stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:167)
at stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:180)
at stainless.verification.VerificationComponent$.check(VerificationComponent.scala:111)
at stainless.verification.VerificationComponent$.apply(VerificationComponent.scala:119)
at stainless.verification.VerificationComponent$.apply(VerificationComponent.scala:22)
at stainless.SimpleComponent$class.apply(Component.scala:53)
at stainless.verification.VerificationComponent$.apply(VerificationComponent.scala:22)
at stainless.verification.VerificationCallBack.solve(VerificationCallBack.scala:24)
at stainless.verification.VerificationCallBack.solve(VerificationCallBack.scala:11)
at stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:110)
at stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:109)
at java.util.concurrent.ForkJoinTask$AdaptedCallable.exec(ForkJoinTask.java:1424)
... 4 more
Raw
test.scala
object existential {
case class A()
case class B()
sealed abstract class AnyFoo
case class Foo[T](x: T) extends AnyFoo
val a: AnyFoo = Foo(A())
val b: AnyFoo = Foo(B())
val list0: List[AnyFoo] = List(a, b)
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment