diff --git a/testcases/web/tutorials/01_Introduction.scala b/testcases/graveyard/tutorials/01_Introduction.scala similarity index 100% rename from testcases/web/tutorials/01_Introduction.scala rename to testcases/graveyard/tutorials/01_Introduction.scala diff --git a/testcases/web/tutorials/02_Ex1_Account.scala b/testcases/graveyard/tutorials/02_Ex1_Account.scala similarity index 100% rename from testcases/web/tutorials/02_Ex1_Account.scala rename to testcases/graveyard/tutorials/02_Ex1_Account.scala diff --git a/testcases/web/tutorials/03_Ex2_Propositional_Logic.scala b/testcases/graveyard/tutorials/03_Ex2_Propositional_Logic.scala similarity index 100% rename from testcases/web/tutorials/03_Ex2_Propositional_Logic.scala rename to testcases/graveyard/tutorials/03_Ex2_Propositional_Logic.scala diff --git a/testcases/web/tutorials/04_Ex3_List.scala b/testcases/graveyard/tutorials/04_Ex3_List.scala similarity index 100% rename from testcases/web/tutorials/04_Ex3_List.scala rename to testcases/graveyard/tutorials/04_Ex3_List.scala diff --git a/testcases/web/tutorials/05_Ex4_InsertionSort.scala b/testcases/graveyard/tutorials/05_Ex4_InsertionSort.scala similarity index 100% rename from testcases/web/tutorials/05_Ex4_InsertionSort.scala rename to testcases/graveyard/tutorials/05_Ex4_InsertionSort.scala diff --git a/testcases/web/tutorials/06_Ex5_Add.scala b/testcases/graveyard/tutorials/06_Ex5_Add.scala similarity index 100% rename from testcases/web/tutorials/06_Ex5_Add.scala rename to testcases/graveyard/tutorials/06_Ex5_Add.scala diff --git a/testcases/web/tutorials/07_Ex6_Mult.scala b/testcases/graveyard/tutorials/07_Ex6_Mult.scala similarity index 100% rename from testcases/web/tutorials/07_Ex6_Mult.scala rename to testcases/graveyard/tutorials/07_Ex6_Mult.scala diff --git a/testcases/web/tutorials/08_Ex7_MaxSum.scala b/testcases/graveyard/tutorials/08_Ex7_MaxSum.scala similarity index 100% rename from testcases/web/tutorials/08_Ex7_MaxSum.scala rename to testcases/graveyard/tutorials/08_Ex7_MaxSum.scala diff --git a/testcases/web/tutorials/09_Ex8_ListImp.scala b/testcases/graveyard/tutorials/09_Ex8_ListImp.scala similarity index 100% rename from testcases/web/tutorials/09_Ex8_ListImp.scala rename to testcases/graveyard/tutorials/09_Ex8_ListImp.scala diff --git a/testcases/web/tutorials/10_Ex9_RedBlackTree.scala b/testcases/graveyard/tutorials/10_Ex9_RedBlackTree.scala similarity index 100% rename from testcases/web/tutorials/10_Ex9_RedBlackTree.scala rename to testcases/graveyard/tutorials/10_Ex9_RedBlackTree.scala diff --git a/testcases/web/tutorials/11_Ex10_SearchLinkedList.scala b/testcases/graveyard/tutorials/11_Ex10_SearchLinkedList.scala similarity index 100% rename from testcases/web/tutorials/11_Ex10_SearchLinkedList.scala rename to testcases/graveyard/tutorials/11_Ex10_SearchLinkedList.scala diff --git a/testcases/web/demos/01_Compiler.scala b/testcases/web/demos/01_Compiler.scala index 87b06b2c61473eb5c4172785ffc956a461d5fc04..a38c57f425cab0fc6b143a842276231ee7a759ba 100644 --- a/testcases/web/demos/01_Compiler.scala +++ b/testcases/web/demos/01_Compiler.scala @@ -170,7 +170,7 @@ object Simplifier { case And(lhs, rhs) => And(simplify(lhs), simplify(rhs)) case Or(lhs, rhs) => And(simplify(lhs), simplify(rhs)) case LessThan(lhs, rhs) => LessThan(simplify(lhs), simplify(rhs)) - case Ite(cond, then, elze) => Ite(simplify(cond), simplify(then), simplify(elze)) + case Ite(cond, thn, elze) => Ite(simplify(cond), simplify(thn), simplify(elze)) case _ => e }) ensuring { res => run(res)(m) == run(e)(m) @@ -189,11 +189,11 @@ object Runtime { case IntLiteral(v) => v case Var(id) => if (m contains id) m(id) else 0 case LessThan(lhs, rhs) => if (run(lhs) < run(rhs)) 1 else 0 - case Ite(cond, then, elze) => if (run(cond) != 0) run(then) else run(elze) + case Ite(cond, thn, elze) => if (run(cond) != 0) run(thn) else run(elze) } def test() = { - run(Plus(IntLiteral(42), Var(0)))(Map(0 -> 1)) + run(Plus(IntLiteral(42), Var(0)))(Map(BigInt(0) -> BigInt(1))) } } diff --git a/testcases/web/demos/05_OpenDays2.scala b/testcases/web/demos/05_OpenDays2.scala index fe99ebb2c17e0473f0cec12c1b020dec4219f8d7..188b62158f9b80d747bb7ffd6aacf734ed814257 100644 --- a/testcases/web/demos/05_OpenDays2.scala +++ b/testcases/web/demos/05_OpenDays2.scala @@ -5,7 +5,7 @@ import leon.annotation._ object EpflOpenDays { @library sealed abstract class Piece { - def valeur = this match { + def valeur: BigInt = this match { case Cent5 => 5 case Cent10 => 10 case Cent20 => 20 @@ -18,9 +18,8 @@ object EpflOpenDays { case Bi50 => 5000 case Bi100 => 10000 case Bi200 => 20000 - case Bi1000 => 100000 + case Bi1000 => 100000 } - } case object Cent5 extends Piece case object Cent10 extends Piece @@ -36,7 +35,7 @@ object EpflOpenDays { case object Bi200 extends Piece case object Bi1000 extends Piece - + @library sealed abstract class Liste { def somme: BigInt = { @@ -55,7 +54,7 @@ object EpflOpenDays { else if (v >= Bi200.valeur ) Bi200 else if (v >= Bi100.valeur ) Bi100 else if (v >= Bi50.valeur ) Bi50 - else if (v >= Bi20.valeur ) Bi100 + else if (v >= Bi20.valeur ) Bi100 // *wink* *wink* else if (v >= Bi10.valeur ) Bi10 else if (v >= Fr5.valeur ) Fr5 else if (v >= Fr2.valeur ) Fr2 diff --git a/testcases/web/sav15/02_Exercise2.scala b/testcases/web/sav15/02_Exercise2.scala index b67ce260367e52ded82e3986d3ab1013a5695d7e..e13db4ca70d29b2334c2573f588c191379256b90 100644 --- a/testcases/web/sav15/02_Exercise2.scala +++ b/testcases/web/sav15/02_Exercise2.scala @@ -1,3 +1,5 @@ +import leon.lang._ + object PropositionalLogic { sealed abstract class Formula @@ -21,6 +23,7 @@ object PropositionalLogic { }) ensuring(isNNF(_)) def isNNF(f: Formula): Boolean = f match { + case _ => false /* TODO: Implement isNNF */ }