packages feed

sbv 0.9.20 → 0.9.21

raw patch · 19 files changed

+73/−26 lines, 19 files

Files

Data/SBV/BitVectors/STree.hs view
@@ -27,7 +27,7 @@ -- elements of type i. Note that these are full-trees, and their -- their shapes remain constant. There is no API provided that -- can change the shape of the tree. These structures are useful--- when dealing -- with data-structures that are indexed with symbolic+-- when dealing with data-structures that are indexed with symbolic -- values where access time is important. 'STree' structures provide -- logarithmic time reads and writes. type STree i e = STreeInternal (SBV i) (SBV e)
Data/SBV/Compilers/C.hs view
@@ -182,8 +182,11 @@ genMake fn dn =      text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!"   $$ text ""+  $$ text "# include any user-defined .mk file in the current directory."+  $$ text "-include *.mk"+  $$ text ""   $$ text "CC=gcc"-  $$ text "CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer"+  $$ text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer"   $$ text ""   $$ text "all:" <+> nmd   $$ text ""@@ -515,8 +518,11 @@ genLibMake libName fs =      text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!"   $$ text ""+  $$ text "# include any user-defined .mk file in the current directory."+  $$ text "-include *.mk"+  $$ text ""   $$ text "CC=gcc"-  $$ text "CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer"+  $$ text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer"   $$ text "AR=ar"   $$ text "ARFLAGS=cr"   $$ text ""
Data/SBV/Examples/CodeGeneration/AddSub.hs view
@@ -25,8 +25,11 @@ -- -- > # Makefile for addSub. Automatically generated by SBV. Do not edit! -- > +-- > # include any user-defined .mk file in the current directory.+-- > -include *.mk+-- >  -- > CC=gcc--- > CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+-- > CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer -- >  -- > all: addSub_driver -- >
Data/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -192,8 +192,11 @@ -- -- > # Makefile for popCount. Automatically generated by SBV. Do not edit! -- > +-- > # include any user-defined .mk file in the current directory.+-- > -include *.mk+-- >  -- > CC=gcc--- > CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+-- > CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer -- >  -- > all: popCount_driver -- >
README view
@@ -115,8 +115,5 @@  Thanks ======-[Galois, Inc.](http://www.galois.com) has contributed to the development of SBV,-by providing time and computing machinery.- The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.
SBVUnitTest/GoldFiles/addSub.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for addSub. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: addSub_driver
SBVUnitTest/GoldFiles/aes128Dec.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for aes128Dec. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: aes128Dec_driver
SBVUnitTest/GoldFiles/aes128Enc.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for aes128Enc. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: aes128Enc_driver
SBVUnitTest/GoldFiles/aes128Lib.gold view
@@ -3733,8 +3733,11 @@ == BEGIN: "Makefile" ================ # Makefile for aes128Lib. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer AR=ar ARFLAGS=cr
SBVUnitTest/GoldFiles/codeGen1.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for foo. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: foo_driver
SBVUnitTest/GoldFiles/fib1.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for fib1. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: fib1_driver
SBVUnitTest/GoldFiles/fib2.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for fib2. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: fib2_driver
SBVUnitTest/GoldFiles/gcd.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for sgcd. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: sgcd_driver
SBVUnitTest/GoldFiles/legato_c.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for legatoMult. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: legatoMult_driver
SBVUnitTest/GoldFiles/popCount1.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for popCount. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: popCount_driver
SBVUnitTest/GoldFiles/popCount2.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for popCount. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: popCount_driver
SBVUnitTest/GoldFiles/selChecked.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for selChecked. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: selChecked_driver
SBVUnitTest/GoldFiles/selUnchecked.gold view
@@ -1,8 +1,11 @@ == BEGIN: "Makefile" ================ # Makefile for selUnChecked. Automatically generated by SBV. Do not edit! +# include any user-defined .mk file in the current directory.+-include *.mk+ CC=gcc-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer  all: selUnChecked_driver
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       0.9.20+Version:       0.9.21 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis:      Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description:   Express properties about bit-precise Haskell programs and automatically prove@@ -51,10 +51,9 @@                SBV is hosted at GitHub: <http://github.com/LeventErkok/sbv>. Comments,                bug reports, and patches are always welcome.                .-               Galois, Inc. (<http://www.galois.com>) has contributed to the development of SBV,-               by providing time and computing machinery. The following people reported bugs,-               provided comments/feedback, or contributed to the development of SBV in various ways:-               Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson.+               The following people reported bugs, provided comments/feedback, or contributed to the+               development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki,+               Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.  Copyright:     Levent Erkok, 2010-2011 License:       BSD3