From 98b928a670b2caa90a43009b8200e52bf8e01de1 Mon Sep 17 00:00:00 2001 From: Koen Wermer <koenwermer@gmail.com> Date: Sat, 25 Feb 2017 22:20:56 +0100 Subject: [PATCH] made some small fixes and changed vector_r3 to be actually equivalent to vector. Also added haskell code to generate a shell script to run daikon --- Daikon.hs | 35 ++++++++++++++++++ Equivalent mutations/Mutants/Vector_R1.java | 9 +++-- Equivalent mutations/Mutants/Vector_R2.java | 9 +++-- Equivalent mutations/Mutants/Vector_R3.java | 9 +++-- Equivalent mutations/Vector.java | 9 +++-- HelperFunctions.hs | 5 +++ Main.hs | 6 +-- ...eturnValueVar == returnValue_False_False_1 | 3 +- ...rue_returnValue != null_true_False_False_1 | 3 +- ...eturnValueVar == returnValue_False_False_1 | 28 +------------- Settings.hs | 5 ++- Tests/BaseSecantSolver$1.class | Bin 1519 -> 0 bytes Tests/BaseSecantSolver$Method.class | Bin 1296 -> 0 bytes Tests/BaseSecantSolver.class | Bin 11581 -> 0 bytes Tests/GradientFunction.class | Bin 2475 -> 0 bytes Tests/Iterator.class | Bin 2704 -> 0 bytes WLP.hs | 7 ++-- 17 files changed, 78 insertions(+), 50 deletions(-) create mode 100644 Daikon.hs delete mode 100644 Tests/BaseSecantSolver$1.class delete mode 100644 Tests/BaseSecantSolver$Method.class delete mode 100644 Tests/BaseSecantSolver.class delete mode 100644 Tests/GradientFunction.class delete mode 100644 Tests/Iterator.class diff --git a/Daikon.hs b/Daikon.hs new file mode 100644 index 0000000..1061d0e --- /dev/null +++ b/Daikon.hs @@ -0,0 +1,35 @@ +module Daikon where + +import Control.Monad +import System.FilePath(joinPath) +import System.Directory + +source, pathDir, packageDir, methodName :: String +source = "GradientFunction" +pathDir = "org/apache/commons/math3/analysis/differentiation" +methodName = "value" + +packageDir = map (\c -> if c == '/' then '.' else c) pathDir + +-- Creates a shell script that checks the daikon invariants against all mutations for the current test file +createDaikonScript :: IO () +createDaikonScript = do + writeFile scriptName ("#!/bin/sh\nHOME=\"T3Daikon\"\nSOURCE=\"" ++ source ++ "\"\nPATHDIR=\"" ++ pathDir ++ "\"\nPACKAGEDIR=\"" ++ packageDir ++ "\"\nMETHODNAME=\"" ++ methodName ++ "\"\n\n") + + mutationFolders <- listDirectory (joinPath ["..", source ++ " mutants"]) + checkMutants (length mutationFolders) + + appendFile scriptName "read -p \"Press enter to continue\"" + + +scriptName :: FilePath +scriptName = joinPath["..", "Daikon check inv " ++ source ++ ".sh"] + +-- Adds the code to check the mutants +checkMutants :: Int -> IO () +checkMutants 0 = return () +checkMutants n = do + appendFile scriptName ("echo \"compiling mutation " ++ show n ++ "..\"\njavac -cp \".;wlp/Tests/\" -d \"wlp/Tests\" \"$SOURCE mutants/" ++ show n ++ "/$PATHDIR/$SOURCE.java\"\n\n") + appendFile scriptName ("echo \"generating test suite\"\njava -cp \".;$HOME/KWT3daikon.jar;$HOME/libs/T3.jar;$HOME/libs/T3Daikon.jar;wlp/tests\" MyT3Daikon.Generator wlp/tests $PACKAGEDIR.$SOURCE $METHODNAME 50 1000 \"Daikon test suites/$SOURCE\"\n\n") + appendFile scriptName ("echo \"checking invariants " ++ show n ++ "..\"\njava -cp \".;$HOME/KWT3daikon.jar;$HOME/libs/T3.jar;$HOME/libs/T3Daikon.jar;wlp/Tests\" MyT3Daikon.Miner -check \"Daikon test suites/$SOURCE.tr\" $METHODNAME \"Daikon invariants/$SOURCE\"\n\n") + checkMutants (n-1) \ No newline at end of file diff --git a/Equivalent mutations/Mutants/Vector_R1.java b/Equivalent mutations/Mutants/Vector_R1.java index 2878703..88710ae 100644 --- a/Equivalent mutations/Mutants/Vector_R1.java +++ b/Equivalent mutations/Mutants/Vector_R1.java @@ -23,12 +23,15 @@ public class Vector { * R1 replaces the return in the INPRODUCT-case with a break. */ public Vector combine(int operation, Vector Z) { + int ACCUMULATE = 1; + int INPRODUCT = 2; + int PLUS = 3; if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ; double[] result = new double[this.vector.length] ; double[] vector2 = Z.getVector() ; switch (operation) { - case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT - case VectorCONST.INPRODUCT: { + case ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT + case INPRODUCT: { int r = 0 ; for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ; double[] rr = new double[1]; @@ -36,7 +39,7 @@ public class Vector { result = rr ; break ; } - case VectorCONST.PLUS: { + case PLUS: { for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ; break ; } diff --git a/Equivalent mutations/Mutants/Vector_R2.java b/Equivalent mutations/Mutants/Vector_R2.java index 2ed6569..7fb4216 100644 --- a/Equivalent mutations/Mutants/Vector_R2.java +++ b/Equivalent mutations/Mutants/Vector_R2.java @@ -23,19 +23,22 @@ public class Vector { * R2 replaces the fall through in the ACCUMULATE case with a recursive call with INPRODUCT. */ public Vector combine(int operation, Vector Z) { + int ACCUMULATE = 1; + int INPRODUCT = 2; + int PLUS = 3; if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ; double[] result = new double[this.vector.length] ; double[] vector2 = Z.getVector() ; switch (operation) { - case VectorCONST.ACCUMULATE: return this.combine(VectorCONST.INPRODUCT,Z) ; - case VectorCONST.INPRODUCT: { + case ACCUMULATE: return this.combine(INPRODUCT,Z) ; + case INPRODUCT: { int r = 0 ; for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ; double[] rr = new double[1]; rr[0] = r; return new Vector(rr) ; } - case VectorCONST.PLUS: { + case PLUS: { for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ; break ; } diff --git a/Equivalent mutations/Mutants/Vector_R3.java b/Equivalent mutations/Mutants/Vector_R3.java index 2e384ef..715a74d 100644 --- a/Equivalent mutations/Mutants/Vector_R3.java +++ b/Equivalent mutations/Mutants/Vector_R3.java @@ -23,17 +23,20 @@ public class Vector { * R3 reorder the cases, and remove the use of return from the case arms. */ public Vector combine(int operation, Vector Z) { + int ACCUMULATE = 1; + int INPRODUCT = 2; + int PLUS = 3; if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ; double[] result = new double[this.vector.length] ; double[] vector2 = Z.getVector() ; Vector resultingVector = null ; switch (operation) { - case VectorCONST.PLUS: { + case PLUS: { for (int k1=0; k1<this.vector.length; k1++) result[k1] = this.vector[k1] + vector2[k1] ; resultingVector = new Vector(result) ; break ; } - case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT - case VectorCONST.INPRODUCT: { + case ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT + case INPRODUCT: { int r = 0 ; for (int k2=0; k2<this.vector.length; k2++) r += this.vector[k2]*vector2[k2] ; double[] rr = new double[1]; diff --git a/Equivalent mutations/Vector.java b/Equivalent mutations/Vector.java index fe437b8..a091323 100644 --- a/Equivalent mutations/Vector.java +++ b/Equivalent mutations/Vector.java @@ -19,19 +19,22 @@ public class Vector { public int getSize() { return this.vector.length ; } public Vector combine(int operation, Vector Z) { + int ACCUMULATE = 1; + int INPRODUCT = 2; + int PLUS = 3; if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ; double[] result = new double[this.vector.length] ; double[] vector2 = Z.getVector() ; switch (operation) { - case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT - case VectorCONST.INPRODUCT: { + case ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT + case INPRODUCT: { int r = 0 ; for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ; double[] rr = new double[1]; rr[0] = r; return new Vector(rr) ; } - case VectorCONST.PLUS: { + case PLUS: { for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ; break ; } diff --git a/HelperFunctions.hs b/HelperFunctions.hs index 2a278ea..24608a2 100644 --- a/HelperFunctions.hs +++ b/HelperFunctions.hs @@ -58,12 +58,17 @@ getMethodClassType decls id = head $ concatMap (flip getMethodTypeFromClassDecl extendEnv :: TypeEnv -> [TypeDecl] -> Ident -> TypeEnv extendEnv env decls methodId = case getMethodType decls methodId of Nothing -> (Name [Ident "*obj"], getMethodClassType decls methodId) : env + Just (RefType _) -> (Name [Ident "returnValue"], returnValueType) : (Name [Ident "returnValueVar"], returnValueType) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env -- | Creates a string that that represents the return var name of a method call. This name is extended by a number to indicate the depth of the recursive calls makeReturnVarName :: Ident -> String makeReturnVarName (Ident s) = "$" ++ s ++ "$" +-- | We introduce a special type for the return value, +returnValueType :: Type +returnValueType = RefType (ClassRefType (ClassType [(Ident "ReturnValueType", [])])) + -- | Get's the type of a generated variable getReturnVarType :: [TypeDecl] -> String -> Type getReturnVarType decls s = case getMethodType decls (Ident (takeWhile (/= '$') (tail s))) of diff --git a/Main.hs b/Main.hs index d3bf36f..e65ad46 100644 --- a/Main.hs +++ b/Main.hs @@ -19,7 +19,7 @@ import Settings sourcePath, mutantsDir, resultsPath :: FilePath sourcePath = joinPath ["Tests", testFile ++ ".java"] mutantsDir = joinPath ["..", testFile ++ " mutants"] -resultsPath = joinPath ["Results", testFile ++ "_" ++ postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll] +resultsPath = joinPath ["Results", testFile ++ "_" ++ postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll ++ if eitherWay then "_either way" else ""] -- The main functions performs the mutation test on the test file, given that the mutations of the source are already created in the right location main :: IO () @@ -110,7 +110,7 @@ compareWlps results env decls s (path, s') = do where compareMethod (ident, e) = case lookup ident s' of Nothing -> putStrLn ("The method \'" ++ prettyPrint ident ++ "\' is missing in mutation " ++ path) >> return 0 -- print a warning and return 0 errors found - Just e' -> if unsafeIsTrue (extendEnv env decls ident) decls (e `imp` e') then return 0 else printAndAppend results (path ++ " " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found + Just e' -> if unsafeIsTrue (extendEnv env decls ident) decls (if eitherWay then (e `imp` e') |* (e' `imp` e) else (e `imp` e')) then return 0 else printAndAppend results (path ++ " " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found -- Gets the right post-condition given the type of a method getPostCond :: Maybe Type -> Exp @@ -136,7 +136,7 @@ getMutantNumber path = takeWhile (/= '\\') (path \\ (mutantsDir ++ "\\")) -- Performs the false-positives-test on the set of test programs with equivalent mutations testFalsePositives :: IO () testFalsePositives = do - let results = joinPath ["Results", "False Positives", postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll] + let results = joinPath ["Results", "False Positives", postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll ++ if eitherWay then "_either way" else ""] -- Create the file for the results writeFile results ("False positives test") diff --git a/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1 b/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1 index 15d8186..a7be12d 100644 --- a/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1 +++ b/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1 @@ -7,5 +7,4 @@ ignoreMainMethod: False nrOfUnroll: 1 False positives found in: Equivalent mutations\Mutants\Vector_R2.java combine -Equivalent mutations\Mutants\Vector_R3.java combine -Total number of false positives: 2 \ No newline at end of file +Total number of false positives: 1 \ No newline at end of file diff --git a/Results/False Positives/true_returnValue != null_true_False_False_1 b/Results/False Positives/true_returnValue != null_true_False_False_1 index 09c9e42..f91b164 100644 --- a/Results/False Positives/true_returnValue != null_true_False_False_1 +++ b/Results/False Positives/true_returnValue != null_true_False_False_1 @@ -7,5 +7,4 @@ ignoreMainMethod: False nrOfUnroll: 1 False positives found in: Equivalent mutations\Mutants\Vector_R2.java combine -Equivalent mutations\Mutants\Vector_R3.java combine -Total number of false positives: 2 \ No newline at end of file +Total number of false positives: 1 \ No newline at end of file diff --git a/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1 b/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1 index 2521dc0..ad587ee 100644 --- a/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1 +++ b/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1 @@ -5,30 +5,4 @@ postCondPrimType: returnValueVar == returnValue ignoreLibMethods: False ignoreMainMethod: False nrOfUnroll: 1 -erronous mutations detected: -206 verifyBracketing -200 verifyInterval1 -200 verifySequence1 -200 verifyBracketing -197 isSequence1 -196 isSequence1 -195 isSequence1 -194 isSequence1 -193 isSequence1 -192 isSequence1 -191 isSequence1 -190 isSequence1 -189 isSequence1 -188 isSequence1 -152 midpoint -151 midpoint -150 midpoint -149 midpoint -148 midpoint -147 midpoint -146 midpoint -145 midpoint -144 midpoint -143 midpoint -Total number of mutants: 207 -Number of mutants in which we found an error: 22 \ No newline at end of file +erronous mutations detected: \ No newline at end of file diff --git a/Settings.hs b/Settings.hs index cb8f58d..362dc7b 100644 --- a/Settings.hs +++ b/Settings.hs @@ -8,7 +8,7 @@ testFile = test3 -- The post condition may depend on the type of the method we are looking at postCondVoid = "true" postCondRefType = heur1 -postCondPrimType = heur0 +postCondPrimType = heur2 -- When ignoreLibMethods is true, library calls will simply be ignored. When false, we consider library methods but make no assumptions about them (so the WLP will be true) -- To prevent insanely long calculation times, we may decide to not calculate the wlp of the main method when ignoring library methods @@ -16,6 +16,9 @@ ignoreLibMethods, ignoreMainMethod :: Bool ignoreLibMethods = False -- No longer supported ignoreMainMethod = False +-- If true, we accept mutations that satisfy either diraction of the implication, if false mutation must satisfy WLP(S, Q) => WLP(S', Q), where S' is the mutation. +-- This does not seem to catch any mutations at all +eitherWay = False nrOfUnroll :: Int nrOfUnroll = 1 diff --git a/Tests/BaseSecantSolver$1.class b/Tests/BaseSecantSolver$1.class deleted file mode 100644 index bec0ed2fba45f003679dbdd52cc1df95e176387f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1519 zcmbu9ZBNrs6vzK}Y;>DNCW;^;qEwz#8bFaJk#2OjST;g=h#`iQu3?3)CG7@L-<ude zhA(_ACWIKn2k=7~&mGJ~kOVO4&N;u^-v3Vjz4!k7_5BdQFw$|{MQ02N+>23lpJSH* ziNgaPx_Ri~p*M~`^z%m_#;AJ4v5Qxac^D8N3m9V1Bz@N|nT0uHTk`x3$=Ei`f+d+= zvFN#hR5VJ3Vaad}=WSpIQs6l|mLEt-Bd~PKG~AM28Ik6!Qo+kJgjO>QGndj-9LL+W z@+4R;*`CV~oirWWwM$bBb-jJd4B?cQw-_2V+qJUg;=1K88tV>?H0UM6+@e>gF!{j{ z*S)fDT4|f#Z$8=Yz^1Wdkdo?}ju+VO#!>$Qh6Owk@f0H>Zs59zXBZVRhH-{AK1Fs6 zcSFv4df6<bZOh54zVG=WCir8MJUr)N3ZnvEa2-WN6W2*1C1QpL6)A>EvRXc}T0XW~ zu2?Nst(K3imQS`W4Kjd1%($-QryL^)tbid=>n^vxX_+O4@yq`Q!`S&JpZad~JBCx{ zO-=Rot!kGRnxGY+WM8l8nHiN~;=hCh&(GVmh$}0JR%lF9(~HN-@rBIn%Ri7*wcJYe zj*`qRtH+?6|3yxHvg+=ruNLWxIdg^}cPOK2nQShjGo&uy(Ak2*ygIAsOQa_*sIyC& zvX)jfJ(K99gX9{WL7_w|U(o<%+95PTO`sV!DYp=`ppGiw(*fAwkN7u)_V`t|k8n8m z1>si}tS5}rP#~<YVU$p)VT>?Z!2`rAnpgHfm$;9HswUx8!m1`=BjJ(eS86au&9)$d zR&=48au0@RcSbM*g|=mccI7;D%5PA>7G(#!ct`m?KHwwe5X}VQlz~Gm;xleh)sMuA pfHutiBP{<tMz-9h86mXe4&^X9C=SxEiN+F~5>YyrJ1{-n{u}S^kYWG; diff --git a/Tests/BaseSecantSolver$Method.class b/Tests/BaseSecantSolver$Method.class deleted file mode 100644 index 2c436a53bcdc9bc2c78059d3eeba86dc646cff4e..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1296 zcmb_b-A@xi5dUp^?Ol)K!}6hgC<-VoC?_H>mKZ7)(&Pl=Sq$;PEXP`oT<^@?mBjx_ zOCm<2;n}|i_1!po5UJvmb~l;XnVp^a&BuQE@!>Oo1uW*E;JS_*m{u{QqNt+>Gm^|| z=+)`+rnI=Fp<nVj4Fi&!DsD3vPbzCQtNdcMY}r+Y>?0BH20Ns$`o0KPJRU_NVpy?) zux|2K+}RbT6EqruADImv?=G0!=ickcjm#+U_C*+(4|pVO;c!2;6V23#&k}=HwXEv; zM%89eA6M4Oc1@n9Hp^D6LZ^q%I}#<k&%LGuy;>-C#-p+l><ETl%k{;2v#~A0r+nKZ zjhckoc**drVD0gJZhG9Wn|2(!e!W!eOgc-h@5c8ThW-+wTHIvF*>2tEaWf=D>4MZ~ zOOAK?s@8_9;x`*h9RPKoda2t%GjznNE9)@$XV2$kF$@gKc^on@k2@+B7|Q=WMFvK3 z*T7|5IVHWw8|as00C|R<vo6SN88VI+_ylpFP;9Hj#`d0YVoKxQzawH;Z0|_&S4wR$ zeoevekV?z*^!s|~>nh8`Aou`r${^vC1kg7kD<>_G!$n*I!!St`#O2akVDFGRLi!C! z3?oFd$=xy8k7Df9eiErf+tm+c<~=e;P|iO{$y$=33^0x~Z9tuw9Xmw!?K$t`q)Fi_ zG+ZNkf=Uodxym1*Y~|JTA+!VJ5<yoIp(_!LOd@n=KapL!MN_+_w9sX5Wm@RA55UgC l<r9}*(T#7E+;>dlm~fp0pTJ}SVhR_C>jXkU0e#D3KLK&6NKF6$ diff --git a/Tests/BaseSecantSolver.class b/Tests/BaseSecantSolver.class deleted file mode 100644 index 2bb94aed62ecc60b5a296eeb85e071bb882e16da..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 11581 zcmb_i32;?qmj3R$Z_i8e-z>bB01_~e1u>uqvZx7J6oIfL1OYWZ!ZSQb@*sIZamRf{ z#kPURlDKhQ5fy>fQCfT4P{)}mXQsNUYo^DVa;B!LYZj|(x~sd!Ip^Ga-;x9dyG?TM zyZ`ymf6n)xbN=(6`@fw2-*?^za50VsaUre?;Cgfh>2^Z^QEUic2D<pRk$Yo&yD>=3 zZoX~eTiko<KWRMuaBDN)w(zZoZ@mG`L|>4kC%jkuTDagnWk2|^HHZkd`OqIkIkp8c zfFutX43g>uH@Ew6Qvf$(hYz;|QGr|Ya2sy-;SMI=8N^-K8N^iF&ARU4+r2*A7sPbj z@52K=Jm|wiK0K@e8bXWv`eOZ!J<)-I*nkg@Xz(tJB{wBDYA9=JZfRJ(w7s)oQQPvR ztJ|A98yXu|uWD#qt3hkhkl&c-8%Rd`k{!{W!I<~*qaXjz@Y}z6OoK1l)04O<Mj{q0 zP4suyMYl$~HpS|?61}}NqOLcZ+;nkWv@hDTV<0|IH<0Mr9_t^dYp@2jC3*&v@kHMO zLegs^Y5W0V7DWeQZLuzbMUqHxr8ONEw=mupPhPI!%Ic;cL10aX26tm(V@yNg(s*C2 zb+C6stiL_Fp@%5>ZOLfYmSxec(iW?eX|Jko`mr=GCQ(0@EZ@e2*h+(5T|<ryHs9P8 z+saND(BSWlZ`_)Q_a!xWNGJD);scBNX?n3_ysw*_TzwAKT-_Jn9_^1uld+b;zAkYv z30vpGqZ;z!18uQwgR#D@*er4r&#Y!0S(UsOzj4RnzGSR_d$fnT1VD!mkNL1G-9Kt5 z`9)bne<YM7Fwhq7?u#Y|`^mQ-oWpd}LA_xhNv29>rf)^%4_O%YEMgl+3R!p#Kr&;} zcE6m~La;3{*xwaviF2@)j$AVrZjNq`hHyC^_u+{Up2Y4Dp2AOjcshiiVnGP=`L+<3 zG0!T#b%d}7SB0>bZ~Kr6VGVce=jH*v9pu{~423X^XEe+`V_t|ku~$dwh1}T9VUZ3< z*7dB0+2=5P8KoJC9ZEFK{r!o4AD#>0dB*kv<2Z~Z8ZJEtL9K&5Jq`WcgT1l7WEuzs zVF)H(q*!BP)%8UCy6cv2*c|IhGRBuEutRtmDGdwHNd@PQ#RKh$#L_5DIjtsySMVZ5 zdkC-MH5Pm%gq3XBrC4^3=o6V$kR|qVyslyX8KI5J&Lcxa!=iH^+;E0fprP^Hg`9C2 zoXy1l?>s6gtu*`q5M%EyXN$-*gwad!+&oCzVNc!CL|3#YeoJg)OQN4PP)f{Mao3a> zlwHSN-Nd_6X>W9MqQ9<pFd5}U%M0noI3;RtXXmoc*5$N&FQ!epad}7cs%A>(p6bPm zIp5AZcQcIGt7(^LXkFXcwz#R8v~<Uk%i?|ZL-c0CLp%T0!DP%@9`WrlDHv$?B)FtM zLIa%SBs~pXU4xV~cW5Z4E(#tl31Yd_Rk0qL-1aQ$(#p1*;>oT}wCPsTOe(FaqtdQA zDy8bEbevIXC+NzNac!3i8eHqyNQwT9ampXEGg6!ON3!p<Ga5=<)e;>@a`GYe=mv6B z)1L%vl!^6Twxz#ib!%h$;^nQhde5BxW9cM1X7JDku;eV8_SmDjuvxHv>BwxifGy&o z{dtgflCtL3rWMN<x3;%YoKfM}+DXsNt2!E%k}ZX2`Hd70<o7H&R`e34>;5!MS)!~O zY{6*CI!5W^%7Rvidoq>87gF(C2OSe|3FgrATq?s|xRfs1+~~Q8_c!_s!cA%S3gW1z z)_xk{rq8C@suR%Ogv&jI2z{iG=XRfjo<gwpO}O8Nhdzi}=<yJBAAFjLLZWzv<<ULk zZFt`xIW9ENy+~v(frrxiWGq7?TCs@eGvN82UIBC;8tG~RysPN(YP!Cs-Za@o1ny>_ z%{I^>66PhQmfEVC6Y!C0ZyKrBI~G!(FO5_YyU#-EDf5g0bsfoGk14p8^j#-V>lo^I zxEbmwthChA^lY##HrT`P!B1e95ZH+41pK7mpN8xAj{(<EUd7X}Ol!~p<#iDI#z4G< z6!f4Hy|@~Ef_N4qo(PX1vmv)rV+mc~6R@lf2XhIo#8u?8dZ73_5?BHhR+H)!4CPa{ z{R&JJGaNP`J^N~pBXE_?<X1cw!t5~lGfcs&ZKi+<q?t-sQov&J*H#@z-aL=Z7F5Ap zwxGjS!))wwRX7Z<i6{86U>NxkPr;u3*lA)TQ}Qj!-h)V(SS3=!Dqj_fRN+lwwTVk3 zj>bF{N^3liC4`0%C_%^s2aL)i{e>pn1$$DM$OJWnQW2Z4=!b@;;Hi3@drC97N*IMN z8&|PK$;DNyN^M-kYvbZ6vgr*~l#8n<2bVDt*SHL>acZ1}t445zhfroC4y&;A1Slqt zqrg@bQIWJN@p8m6I(xZrUclxmQ)RhaWf?9tFVE&GSLL}}<rywxUcSvWUX8c7blc41 ziOWr9*5`0SQFX&8sfqY%s=BvCd=XD~B4KKO;EoGNc66EAH{3B}WXBd$`;0p-7}+sk zYDcLfh4a(}s!m|!>gqPN$7^`#^kEcbfgt*JCfDYY2|*{5YjVk?pBIR#&LxxfSwv1@ zf~r>2MSHdmnr9J@I)4};QB6_&922HEgl-eNnK0QQbeY)6gbIf+U}7r~QW&Qy)cK;q zlC{Oenusi+Nfb*pRV2HGN1i7wl5;7yCQ6HVIoYcT(jt))L}am=peBh(8c$HX>>}o? z8b%(wie#?f_B6XqQtP=r)ozpAncS|l+a$Sy+9{N(N>wG2MGndKTdwb(r-Z>!Gu2FC z;6%e~P|dVrD^MFzoE^k+m&hu7lDlW~nk(W}c(<J$F19GN3b$sm!^P?n5i7hYbZ~ZH zQM?Lgsf*GoB|BV1_Q+(1Sp>kz4$?hm2;*dEzM7-v(9jgT5hcs;3I?XlWnh;NL($}l zwiN6=s7*ET5fd*<6Zh=Xl!>Dvr(9j8t`G>$hy(b}#8W(CzGcHA$L90wHrY;WeyQCi zABfH8+U+cx&sFn9INQ94e8V;`Vu$kN7pR4~lV6xK`3278_a49vjHf=6g6dVhOx{x? zi=bf$VG)|I8dQVy_#!^Z`fAaTYlhvoNG;+%*TmAoR5~A+F3M9ywa4H+j^YbnrX3a9 z@AyWSPS<$4?x*H`454`lOKf4ys#z2*uv2}pYE(@`*~bnnvBFL@$&ALCkl1Oo;>k<> zTP$!bwm-FpRf}p7dE~^~S=I6({FAL}xmqq=Ux_N!I*bCcBU!SGTycV#mt{!gjpv!P zG(#f8OTaG4kjO`Oi1dhBqFM#EBa__SWi8{YM+Cs)5dm<O-F6n;m7@dTN_DjemjEDW z5&&HZd-^M!aDGIsP%G@|3oz9t>ud$jWEHO}RYU8n!NeS<th6Y!&gx85$~?kqrD_vZ z!b=O@M36^OmH93rYfqr;6c258R7O<0YIjr;OF6NO7naoyOTJpIR$D9)#g&HY$OKx4 z>X0sSgH<=I6~xyt+cm>5B2?N;hy?beT&GMdV(OX<b?*V!OC~NLY6|1k8nsrCJ7e}9 zbUk9Sk3|BtC?F<MgnEwSJdRLTw;i7z`kYJ`*WQOHMk!{sW2|ajW~r=G>jbAqcIy<B zTCc7ZbyVd@M!r^n%g(%B9;cKR?z5_q>oRh#Q`cq5QP(?>`_Jlnb-naZ<bEwPQmRwk z;HZ$ib%V&|b*MV!(a%dz3Z7_2MN~zzRcvrn+@Ut84UUR!ETmh6$aZ-n$AZ*1PK_3` zD3mrRlvfF&u!^Z}LBzZiH&UZHwNRJZD1Dsx1@6Y2MAVf|L<cR%n=+6$sZH6C<4)*& zuHq_gL&p0Ixi15`*M@v3T~_v_Cy@oYNA;y4Q}E|N-mJFdLf(=Cd9wqV#)*{^8ORBh z$cDVtfgDj=)m8^`&Vsm=q3Z)Yi(7^<f%aq$%={X<Z;9lc#H76k_0^^(5wv4WhCTcA z*(Uy5d@)V!P`3*Bu_PVP^Grx(m82PEiiiPeQ3jEa?Uxqi9VsHVNsCgNQ$%c2Nl}m~ zA_ywOznSeUz{$?*m~vB^Lb+5nlkI5=X_Is_n5K{pC*2IHn?;8$kFW%DOme_Qi#~hR z(z?BX)+wz~dd&pRr|UAh9-`}4M822N+?H|EZR$30hP7_hokO@%%$Kk3RCh`b@AbT% zZ&!B+5?aqwSjZg`Y2uCB<uSzT*;hmLue?bZxO)i8WN;xp)1Qc2Ae15lcNy5}2;|vP zQ^fFl74>F`tRj(;Rt!8igl8R*4^mS^J|QC>kP*Dy7`UHJDXX>L1Q!AZ?z2d=Tsuv0 z`b?pWs0JPo5cYy?G_g>2r4)({++*Ng>E$KM1s=622&8f{q<N3C0%);kPkmPw&Rqs} zW#N1*3+JOY&O=D!d?XD$8|Nbi9!uk-)s~C%Ap;MO!1-`4&W9YFG}gxH>_z5x9TXeZ zX~(yiN6!QF1!a<6#s{$t+v$6QTeWexO`C~3v?I7v`xN(R-{O8(2oJa}!h^1B@Tlun zJn7zr-R|Sq<C%@Up5-{;orNLq5)6C0@r-vDp7S2V3qCgv`zGN<zmAvu=ixPfACCC9 z<EZ~hyyf4A6aHg3>HllI7nq6n1J~l`f$jJ(@H~DIcpo1Heu+<lK71OSjMKq|_#*fY zz6^eiuY&)9zsc*x-{w7luk)V8-{-xIUxmKKKjxR<*ZCLXoBUhwFZo~M+k!#-Tj50f zd*M|4h7TF^FEvj|UZeg;l<3Y!6SYe9JpKsjhEcX!U#2h7`9Q}$anRw?bv>*F&(<0C z6pKKT#Nsm__1Yh4^Ni3>#Tvasey`V8*uU41o<anyBM(xd(>bS3wERDVRyxL5S1ye; z@dQUJ9t+H$Lko|g!<|bz6PS9-jLoC{l9y#K-S&<vSW+^fkbc5VdRy9qV{vL>J?yX7 z+*8AAY(5u8^SR2y?fNSDT}QSu#$aLBjUM>JsNpdsxJObQ8;w@yD(A5D`pSJ_S6C00 zmQD;#4{JripgXLU+aI}sJ6Z<Cwn)iD{@6UeU`0iBKK+y~(%bcw^1GId;~fc?V%R?; ztc6*>UazCPBrnf;$SW!uzeaD>mrDGNp+?xxiR<@tNV%AT*iGAB1OZB2OX#Vdw!67R zb5qanBwO#L+&Zngi(ZUqU;bAi?MahpW9GWjz)#a8+L=EP($i@YZOuoBB%8<62KHJ> z*%C^d^KN0^P04p!HR<5DI0H{gljJXy<`dE+W-e3>JT6U=%QYdrP!PqyZjnnu2!faH zPS;ZgeqwdW+aGVlL?H<!pw~a%j14?RxxRpg@%!KFG<Petd!;1!gPgBUhAJ*1^B2%h zc#-aS!NnPeFY;4>zs9uAQ$3rhk_eD>V<LW^>|b?)Xq<t4^e2ddwV$Aj4^=-w(YvTv z`z9vq?_tUboX@X2vY)05q=c98@vAhoEwI7bs-K}!hkb-fd+&bw8^OEZ;jOWFxv)0y zE>Yd4ep(vu45N&WQfW7)_ZmJk;jY(pQ-4Lee`a+Pox6F@rtT-G`%&pWIgHuXL2Ra* zPV+_zB+`(K?4XfW<$tk(lLSQoS6L#0tl<#7p^b!7L8G`#H1HCImEh2BH+8p=UStxV z1#6p4*MAAgWP@w#<@xY1CR^gIgU0kM2-C1O*L3kqKnfKG4wHC+Q(}o5Zz(D<UHe7S za8?;IWGg*{-#X>eA)A!KH(BM<Ap^rA)IP8Nn9C)Ps3eyiFmN#KGOJuVD4|Km&{ny0 zfP7Ub=g|A{u)uhMVYvMA{JdojdYA4qwciTqIg3P9+j{GWR2JTI241jXh!?LgwU0AZ z+cO599RcInTo}(dF!mnO9uqw$Y}Na<ou+n+kd9jxptCJP(=DX8#S@+Ke9ZEM6+;{( zPPmCD7MR*>ViQjsGjKxiuqQ~|Bw^Jere+!CNR}sFvy_qve(!kVRU5|ve4FKoR}CDo zO(5}gI>!?)8+c`e30}!H!OLkA9K<e}&|6tB-n7k;RhPbDlTtbL^BV@<vSG;lbL-OA z4ICW-<7h67*BuzvQYG8Hn$B3`_ytCDp+?hjspi2(&5I{ApJcFqz{*fWFDMPQP)!il z<)c6^=ihp5rDm6Gt-M*nrD<M$QogPi73CGzYgdoz^-Rg#WvJM*N7C@Kbp6=!^m;A5 zja5*_U5*v@Hn!9H%21mxp8ALm<EtZXS`?H7v})bdtoNtCq?4a%)i&86a=x(tf^19; zNaMp{Om%q3+G#NywJZ+5)J^;yv8GUI;6no+i31}trXa)qCb98GXyAQ`n`h+tJvzN7 z&V$%(z0(@_3!&`Uhr672+6WP8l!#^K1BjWtUDCs~BIE-R$Y*i}eoj%xN)Mvm#5^IL zvPdLyhKXrJl9X`Dzz0?!S{My_QO=;v4lCIRwR{Pq8kCjjMS7^n35!g?OwscUquj&p z_p)OGpnvYMHbi>2_DNOokO2Br@bXK&flsXI9^#XEeyKO`u|-MY`YZ!{Y~WMJ02KMO zYRCZeF#lalrHymiw3Dc+ri&!V#`&3n&xD^GX{XZ9EO)u}6R1A*Mtac{@M*GEjFnmm z9@N4z%asU(crM@5m#n<Qd;C~Qe?GMNKwqo2e~-`^=u|uqzjp*btw*QYno4$AjSkB$ z^zE%%zS*WD37YxoA(YDm==J|J{m}$c@K2+8@%K^&J|Dt(r~h+mN`HWyMhqh-G!Yfr zd1%lk$%MRck9U`Qa!{<nH8zTGktatVrfB&>ypt|hzA*5GSn}-Uih(b)(0@ry3w;%x zMlt#n=mg`h416WB=t#s`fnSL-{+fb%<vB#(QJzFCoxi?|>1(TM>^i5`Dq&9Gf-K*a zv+=ZPl<=x3;nm<8t(N|oaykxcbu#UI<Z;p~cT)}R56kSmH0KKX?_nKlB?Q*dcmG`R aU5kt8vxuH%(!VM|`RN~;XJB^yg#QE8`BZ8E diff --git a/Tests/GradientFunction.class b/Tests/GradientFunction.class deleted file mode 100644 index 8648b1d5a58f7ba2bed2dc561cb18398a6673006..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2475 zcmc&!&u<$=6#mBE-LcnpJa*zZcI!fD+S+jvlZ2#gC{-a&!Kg{9rbH@{h&Ik9-QXY9 z#*V~^OYevi5DB>oLcY=pC_f{(q5czGIB?*^p$8N-yxFyr6e?ATijci;-@N(Wd*6IJ zGY=kpw+&zv=XB^u`Edfz>13Yw!;fB$7j&pN89*OSN$)hr8ICkZhJmdx%wMV6t2yJA zQM_s9iq&$tT3OGPjoQu8oKZ1K@2y+wxn*l*#k9>z%`$3MwUV2zmul9AVbjpe@6Roj z%**vkQ9@p3&@NaNt9Fs$M*6>Lk(p;uCacRPL->kSF=y)KCDXoc5DkXVT+JxHJ8j%@ z#?G4i8PpA<RHs=jy^zl=<T<h&10)g0AcH<vt=mQOvL*9luiM75MN4k4XlTvYFoNj7 z5JxVE7cm^f2u6blBE&FtcoFlaO&XGp=3LFL7i)Ffl;vOI=no=>u^`5Amf^L-SN<n; z1|iAkN=9WhH@mcE7HbR_o?iFhXP&2|s@)cY;ri3l55H>|-dH%oUU`C&wEsK{d1(p^ z-n85*v9hsNwR7cq&E3S4)yj&sN_$~(ae8rPmQDjf`Q+^U)U_$fRMUk*=5315yO5U! zK1@F=a+zng$gWkhcGa-yV3zh(kmMH%nLK*w2GGF}peHIfD%}$v@;eYFD`>O<FGYYe z{rAE8@4>T)u%dhe?<e4_i7-W!JC3Vlzk+htDG(vsL5ZL{MZqbYreBms8F+UQhlit+ zqYI4QZ_=|XlUlL%n?47+T@K2x#F7)_7q`8t?zQivi0ZcYWw(EXI_*L<?n1mxBq_oP z;&I7p<SI=l-is6$G@&)|sdQ-~n96Q{h7Xz;rhv~KH}HNFy)@oL%qQHk61RobCj5@` zj!f4Zxay!nLKix9-^8VX)b~(tWVfAoMEHc?Wkvmu%N)N;OGuyEabl||scdTaKD4>p zUe?@|r8f}~0TI|+b3(!c1Sk1J{a->E_?A|OnHDrCf_qRYj|jR@p56X|Pbe)^NQ53o zh4xYUgxW%Nh_H(yW)9;pp-4!FaR>R1lH;0e6O~djnJFT75Q=G1%ZE*j%ZO-28u+b= zKBszI2oZIvJJ>BeXhN4+Tlh()#2T1#fFThRF#>L4ETP6^FR4hU=yIvG#q2sjt&@C5 z%vo8fyMYs}O5LK{snn5BV%lIr{TjY&5|Y?&mJo@5HH(WLw^>_<o&(L|Z5?KBYpnU` zVT)i=B;6ePOcB{5NjUP=gz|;l?~sS&BAqi}04FhsX*w()VF-Va|0hOR3S(>%<IJK< z{$up9-*L_}g7coYFyU$7tmkvQA`cb&8Rw&Vo+G}4C|O;<#C9mGi*Q_x@8TE~=V<lN z9G!b<eYi`1woAwUXmfZhPdiYP@xP#U1_~UB9dwZmOmg(>AVyZYNykkF0+J+SdL)w2 th-4gmk0d1#n4okyODky}eHKs7^~%bO)cPNrJ4(GuYo%-Mn6o90{|)dFD~<pF diff --git a/Tests/Iterator.class b/Tests/Iterator.class deleted file mode 100644 index a209b6b574657a7ac5db7235255a081371c700f4..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2704 zcmb7FNpD+K7(Lh1b37#1&fpBr)TC+RmbxXhWe6orn$XY;>P%at^u>8e+$45z?5JI^ zL!w1u#i}XbP$9hy5(3c{fdqRtY>@Z?h!wC$2-Tc>pBp<gAS%mu_@?`P=X~$p?;m~r zEr3Bx1Q5k@H8_H!0S?D%5W(|mctH&>1~|NAV93DB0n{kN2#yEfcUG^c?XVh77#J}y zYT%@RXZ*tCq<|O^2#;nn>v=Pizi6%$EH_US)Gu2%*9BZxCj@*ON}+f3^wBo&?C9)G zWeb@+1JSNFXDwJcE0eND9ifpb<hZBWld*1a@(rak>HKj4cmKdeN=LKvmO$NPI%7>2 zR_CnTd2?=slJL2_nOdGQ*YsZJJS1Q&nd{R!4&ARX2y@h-cy?gyM#@^tr&$V<(g|x7 z6E@8G4U<W+dfJ`K7IG<TJgtvO=dGNX&*lzZH#f`>_MpeWSP0|j2;o(n3ZY%CI@Qpv zhC}EP=u*bXLO#8coX(yrq?X23tW{RIoq@nW#f0FNQJBikrx(&GQzf}=8$y=~97A&m zEocp)4RL{f?Z0AX7LzA(IrHX3X5P9nQ^?OOj1bxR^=)^7zHDwWX|9>6B`cZAuC5Y* z<f@rp8gw$8C|4*TD=}y0u3IV6(YR_}&*qY=1v1K{lFW4>y-1p7XQyVTX9(Ts%*C;@ zV+7ILKQS?Ig(yVWiePWWQI7^N26rwr@y{Ccnq}yjmFSrma*iq(^_~UmnTT@s(v!F| zQZE}X2sih@?ZiWf#20XFqR!*_3hp~F+%}?=c((M?NPG#;eRwG`ia4%KgN8xVO<F zdVP+k%SI~=eDw6#sN>S>1o61;!^f?^h(;%Z->)MWi3c!jcqTt*V#|0N@33SS_A<2& z7#zFdVZsC0N9_Rh2WXMNEgVE2wI>lS5f5QduZGw7FR?T&aB(AIXUk$o#nQQFDO9-{ z+#?41DPrV=0}Osp-i-V{)06?HklSiqvxO+3@O`9f+aO3eCH9xan_4_e@l{=5T>51| zqoTd;YV|PHLn??iiAbMRI69EWRWySK5=5!iWfVQ`kF~GI{VCIOpz-Mxk7x)w5DrD% zQFp8Rk~qy@iB?XHLimPxVPHQ&b7|JoPH`fp;)l23v+=rGhPDu4T3$u<Cz!G^qNKqp z={+2?ae&fIw8@|h>$JChifFM>`#3@o!EaD=`5^+|sW4G}&Rc33*+Q6B!4HwKkx~*_ zmfXP`HqPkyF)3wK$Je$WV8q5T<)yU|Su5*yf>u`rTCKyF$9+#F;b#&dmBc0@vR>A2 z`!%bx>uF0uLX53XI#>a?iJuEFjB7Z7C5+-1cG~Z}u2j$UqCVKz*d8zfkx0vvn7fSn z;3<J;Xz3&DHSA}>ZcXk+K~sf-#wxHY6f{&xcTmtEo1TJ#wh9HUPf*aZ8wD-0?LR1p z$>wb+b>B8uQ4srg3gR;E_|@9b6vS!EwW2_^Pw?<(gw5%3hk`St;4CRPPYN!Of=mCK z0{1^C;FID|;Ch!=3hzGgn`(m23I!ciU{@$;uafSdpj~!81qEG2wCP3+%P!eP$4vwi zEZKKoH@56id6fQ8Dec)poSM4CWvV^buJGy{OkCoJnYK$mDTD6a4esHTU3#Do>66{E zM`yQNq#`=)(tEocQB*nPZTvW?j_E66Tt^GbKG~;JKI&ZfQQ0f^>hON~$VR)e-b*UI zHX>@>%Qe3&uYBZO`*MG!0TWL&;J|JTI3V}y19ray_Q`&&Rj23%?B|J(FV1~jd-$eQ z-vR1*xg}zv6|&r42?W?{bL_7a`)iR;%Cd-Iofa9<hOAh?n)n%SieFLCJ$D`*&SxJp x0$pAG&3rlz|Al6b7x<W*F8@nBM?EeSmmis(x5Tzi2-lx{;C5aU&+6_U{2K*n4`BcR diff --git a/WLP.hs b/WLP.hs index c4dc1f6..41f368b 100644 --- a/WLP.hs +++ b/WLP.hs @@ -116,12 +116,13 @@ 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) + SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block (addBreak bs)), Break Nothing) + Default -> (true, StmtBlock (Block (addBreak bs)), Empty) + where addBreak bs = bs ++ [BlockStmt (Break Nothing)] -- Adds an explicit break statement add the end of a block (used for the final block) 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 + where otherCases = let (e', s1, s2) = desugarSwitch e sbs' in IfThenElse e' s1 s2 -- Gets the statements from a switch statement switchBlockToBlock :: [SwitchBlock] -> Block -- GitLab