language-boogie 0.1 → 0.1.1

raw patch · 3 files changed

+8/−6 lines, 3 filesdep ~base

Dependency ranges changed: base

Files

• Language/Boogie/TypeChecker.hs +2/−1
• Tests.hs +1/−1
• language-boogie.cabal +5/−4

@@ -699,7 +699,8 @@ -- | Check that where-part is a valid boolean expression
 checkWhere :: Context -> IdTypeWhere -> Checked Context
 checkWhere c var = do
-  compareType c "where clause" BoolType (itwWhere var)
+   -- Where clauses are always in single-state context:
+  compareType c { ctxTwoState = False } "where clause" BoolType (itwWhere var)
   return c { ctxWhere = M.insert (itwId var) (itwWhere var) (ctxWhere c) }
 
 -- | Check that identifiers in parents are distinct constants of a proper type and do not occur among ids

@@ -21,7 +21,7 @@ typeCheckerTests = TestLabel "TypeChecker" $ TestList [
   testCase (typeCheckerFailure 8)   "BadLabels",
   testCase (typeCheckerFailure 4)   "Orderings",
-  testCase (typeCheckerFailure 2)   "WhereResolution",
+  testCase (typeCheckerFailure 4)   "WhereResolution",
   testCase (typeCheckerFailure 35)  "Arrays",
   testCase (typeCheckerFailure 15)  "Frame",
   testCase (typeCheckerFailure 3)   "FunBody",

@@ -1,5 +1,5 @@ name:                language-boogie
-version:             0.1
+version:             0.1.1
 synopsis:            Interpreter and language infrastructure for Boogie.
 description:         Boogaloo is an interpreter and run-time assertion checker for the Boogie intermediate verification language.
                      The package also provides a language infrastructure library, including a Boogie AST, parser, type checker, and pretty-printer.
@@ -9,6 +9,7 @@ author:              Nadia Polikarpova
 maintainer:          nadia.polikarpova@gmail.com
 category:            Language
+tested-with:         GHC==7.4.1 
 build-type:          Simple
 cabal-version:       >=1.8
 
@@ -27,17 +28,17 @@ library
   exposed-modules:     Language.Boogie.Util, Language.Boogie.TypeChecker, Language.Boogie.Tokens, Language.Boogie.Tester, Language.Boogie.PrettyPrinter, Language.Boogie.Position, Language.Boogie.Parser, Language.Boogie.Interpreter, Language.Boogie.BasicBlocks, Language.Boogie.AST, Language.Boogie.DataFlow, Language.Boogie.NormalForm, Language.Boogie.Intervals
   -- other-modules:       
-  build-depends:       base ==4.5.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, containers ==0.4.*, mtl ==2.1.*, pretty ==1.1.*, parsec ==3.1.*, transformers ==0.3.*
+  build-depends:       base ==4.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, containers ==0.4.*, mtl ==2.1.*, pretty ==1.1.*, parsec ==3.1.*, transformers ==0.3.*
   
 executable boogaloo
   main-is:             Boogaloo.hs             
-  build-depends:       base ==4.5.*, language-boogie ==0.1.*, containers ==0.4.*, parsec ==3.1.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*  
+  build-depends:       base ==4.*, language-boogie ==0.1.*, containers ==0.4.*, parsec ==3.1.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*  
   If !flag(boogaloo)
     buildable: False  
   
 executable boogaloo-tests
   main-is:             Tests.hs
-  build-depends:       base ==4.5.*, language-boogie ==0.1.*, containers ==0.4.*, filepath ==1.3.*, parsec ==3.1.*, HUnit ==1.2.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*    
+  build-depends:       base ==4.*, language-boogie ==0.1.*, containers ==0.4.*, filepath ==1.3.*, parsec ==3.1.*, HUnit ==1.2.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*    
   If !flag(tests)
     buildable: False