From f398c13bafc18b48d64de95c8cf2effe252bd8e2 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sun, 29 Jan 2017 20:50:25 +0100
Subject: [PATCH] fixed a bug concerning library functions with a return type
---
..._returnValueVar == returnValue_True_True_1 | 94 +++++++++++++++++++
Verifier.hs | 17 ++--
2 files changed, 104 insertions(+), 7 deletions(-)
create mode 100644 Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1
diff --git a/Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1 b/Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1
new file mode 100644
index 0000000..844c699
--- /dev/null
+++ b/Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1
@@ -0,0 +1,94 @@
+testFile: arrays1
+postCondVoid: true
+postCondRefType: returnValue != null
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: True
+ignoreMainMethod: True
+nrOfUnroll: 1
+erronous mutations detected:
+96 findAndPrintPairs
+93 findAndPrintPairs
+90 findAndPrintPairs
+85 findAndPrintPairs
+82 goodResize
+80 goodResize
+79 goodResize
+78 goodResize
+77 goodResize
+76 goodResize
+75 goodResize
+74 goodResize
+71 goodResize
+68 goodResize
+67 goodResize
+65 goodResize
+60 badResize
+59 badResize
+58 badResize
+57 badResize
+55 badResize
+52 badResize
+49 badResize
+48 badResize
+46 badResize
+39 findMin
+38 findMin
+36 findMin
+35 findMin
+34 findMin
+33 findMin
+30 findMin
+28 findMin
+24 findMin
+217 bubblesort
+217 isAscending
+215 isAscending
+214 isAscending
+213 isAscending
+212 isAscending
+211 isAscending
+210 isAscending
+209 isAscending
+208 isAscending
+207 isAscending
+206 isAscending
+203 isAscending
+201 isAscending
+196 isAscending
+192 bubblesort
+192 isAscending
+191 isAscending
+189 isAscending
+188 isAscending
+187 bubblesort
+187 isAscending
+186 bubblesort
+186 isAscending
+185 isAscending
+184 bubblesort
+184 isAscending
+173 bubblesort
+170 bubblesort
+167 bubblesort
+164 bubblesort
+156 bubblesort
+153 bubblesort
+149 bubblesort
+147 bubblesort
+137 bubblesort
+134 bubblesort
+132 bubblesort
+130 bubblesort
+129 bubblesort
+128 bubblesort
+126 bubblesort
+125 bubblesort
+124 bubblesort
+121 bubblesort
+120 bubblesort
+114 bubblesort
+112 bubblesort
+109 bubblesort
+107 bubblesort
+Total number of mutants: 217
+Number of mutants in which we found an error: 79
\ No newline at end of file
diff --git a/Verifier.hs b/Verifier.hs
index b9114cd..73f6e84 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -96,14 +96,17 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ArrayIndex e _ -> foldExp expAssertAlgebra e env decls
fExpName name env decls = do
symbol <- mkStringSymbol (prettyPrint name)
- case lookupType decls env name of
- PrimType BooleanT -> mkBoolVar symbol
- PrimType FloatT -> mkRealVar symbol
- PrimType DoubleT -> mkRealVar symbol
- PrimType IntT -> mkIntVar symbol
- RefType _ -> mkIntVar symbol
+ case prettyPrint name of
-- For now, we assume library methods return ints. Fixing this would require type information of library methods.
- t -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
+ '$':_ -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error "introduced variable in WLP expression"
+ -- If we're not dealing with library methods, we should be able to get the type from the type environment
+ _ -> case lookupType decls env name of
+ PrimType BooleanT -> mkBoolVar symbol
+ PrimType FloatT -> mkRealVar symbol
+ PrimType DoubleT -> mkRealVar symbol
+ PrimType IntT -> mkIntVar symbol
+ RefType _ -> mkIntVar symbol
+ t -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
--
GitLab