From dcd92c6a8151fea061735400e517b89925de4407 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Mon, 21 Nov 2016 01:50:34 +0100
Subject: [PATCH] switch example
---
Settings.hs | 4 ++--
Tests/switch.java | 20 ++++++++++++++++++++
Tests/try-catch-finally.java | 2 +-
WLP.hs | 20 +++++++++++++-------
4 files changed, 36 insertions(+), 10 deletions(-)
create mode 100644 Tests/switch.java
diff --git a/Settings.hs b/Settings.hs
index add915e..8d577fc 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,5 +1,5 @@
module Settings where
-testFile = "test"
-postCond = "true"
+testFile = "switch"
+postCond = "x == 2"
invariant = "true"
\ No newline at end of file
diff --git a/Tests/switch.java b/Tests/switch.java
new file mode 100644
index 0000000..87b08d7
--- /dev/null
+++ b/Tests/switch.java
@@ -0,0 +1,20 @@
+public class Class {
+ public static void main(String[] args)
+ {
+ int x, y;
+
+ y = 0;
+
+ switch (y)
+ {
+ case 0: x = 0;
+ case 1: x = 1;
+ break;
+ case 2: x = 2;
+ break;
+ default: x = 2;
+ break;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/Tests/try-catch-finally.java b/Tests/try-catch-finally.java
index fdeaf10..554e394 100644
--- a/Tests/try-catch-finally.java
+++ b/Tests/try-catch-finally.java
@@ -8,7 +8,7 @@ class MyExc3 extends MyExc2 {}
public class C1 {
public static void main(String[] args) throws Exception {
try {
- x = 1;
+ int x = 1;
try
{
diff --git a/WLP.hs b/WLP.hs
index cb10279..8c16a29 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -107,13 +107,19 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- Converts a switch into nested if-then-else statements. The switch is assumed to be non-trivial.
desugarSwitch :: Exp -> [SwitchBlock] -> (Exp, Stmt, Stmt)
- desugarSwitch e [SwitchBlock l bs] = case l of
- SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), Empty)
- Default -> (true, StmtBlock (Block bs), Empty)
- desugarSwitch e (SwitchBlock l bs:sbs) = case l of
- SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), sbscode)
- Default -> (true, StmtBlock (Block (bs ++ [BlockStmt sbscode])), sbscode)
- where sbscode = let (e, s1, s2) = desugarSwitch e sbs in IfThenElse e s1 s2
+ desugarSwitch e [SwitchBlock l bs] = case l of
+ SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), Empty)
+ Default -> (true, StmtBlock (Block bs), Empty)
+ desugarSwitch e sbs@(SwitchBlock l bs:sbs') = case l of
+ SwitchCase e' -> (BinOp e Equal e', StmtBlock (switchBlockToBlock sbs), otherCases)
+ Default -> (true, StmtBlock (switchBlockToBlock sbs), otherCases)
+ where otherCases = let (e', s1, s2) = desugarSwitch e sbs' in IfThenElse e' s1 s2
+
+ -- Gets the statements from a switch statement
+ switchBlockToBlock :: [SwitchBlock] -> Block
+ switchBlockToBlock [] = Block []
+ switchBlockToBlock (SwitchBlock l bs:sbs) = case switchBlockToBlock sbs of
+ Block b -> Block (bs ++ b)
throwException :: Exp -> Exp
throwException e = false
--
GitLab