index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
Commit message (
Expand
)
Author
Age
*
(no commit message)
schaef
2009-11-20
*
Support {:PossiblyUnreachable} attribute on asserts
MichalMoskal
2009-11-20
*
Fixed bug in inlining (procedure *definitions* had been traversed by Standard...
rustanleino
2009-11-19
*
doomed stuff: minor bug fixes / improved output / more test cases
schaef
2009-11-19
*
modified the doom checking. It is now able to report only the relevant statem...
schaef
2009-11-18
*
Start (some parsing and resolution) of adding algebraic datatypes to Dafny.
rustanleino
2009-11-08
*
Fixes crash when modifies set includes a variable twice.
mkawa
2009-11-07
*
Added a sequence update expression in Dafny.
rustanleino
2009-11-06
*
Redesigned the encoding of Dafny generics, including the built-in types set a...
rustanleino
2009-11-06
*
The Dafny call statement now automatically declares left-hand sides as local ...
rustanleino
2009-11-05
*
Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "...
rustanleino
2009-11-05
*
Look for Boogie.exe also in Program Files (x86)
MichalMoskal
2009-11-03
*
vc:doomed does not use the console anymore to report results
schaef
2009-11-02
*
Fixed PreLoopHeap counting bug.
rustanleino
2009-10-31
*
Use the new F# names for bigint type
MichalMoskal
2009-10-30
*
Fixed problem where Dafny filenames with unusual characters in filenames had ...
rustanleino
2009-10-29
*
Changed how Boogie looks for Z3: first look in the directory where Boogie is...
rustanleino
2009-10-14
*
Evidently, Z3 does not like QID's to start with a digit. If a Boogie filenam...
rustanleino
2009-10-14
*
Fixed bugs in inlining, and added a test case.
rustanleino
2009-10-14
*
In the TypeDeclCollector, call RegisterType for the bound variables in a quan...
stobies
2009-10-12
*
Added /z3lets switch, which governs which kinds of LET expressions are sent t...
rustanleino
2009-10-04
*
Handle new Z3 'Memout' message.
stobies
2009-09-30
*
Fixed some bugs in the generation of bitvector input for Z3.
rustanleino
2009-09-29
*
Use type-erased result type to make decision about whether or not to include ...
rustanleino
2009-09-27
*
Optimized the number of Z3 queries in doomed program point detection.
schaef
2009-09-25
*
Added antecedent to select-of-store axioms to make them sound even when trigg...
rustanleino
2009-09-24
*
Added /z3multipleErrors flag for generation of multiple counterexamples per a...
mkawa
2009-09-23
*
* Boogie and Dafny: added /cev:<file> option
rustanleino
2009-09-15
*
Dafny: Added axioms for division and modulo.
rustanleino
2009-09-15
*
Dafny:
rustanleino
2009-09-14
*
Report prover warnings during smoke test via the VerifierCallback
stobies
2009-09-07
*
Use callback mechanism to report prover warnings; do not just write them to s...
stobies
2009-09-07
*
Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other bit...
stobies
2009-09-07
*
Full (?) support in Dafny for Counterexample Visualizer predicates.
rustanleino
2009-08-19
*
Improve token-dumping in the inspector interface
MichalMoskal
2009-08-18
*
Also sign AbsInt.dll
stobies
2009-08-18
*
Sign assemblies
stobies
2009-08-17
*
Incorporated Counterexample Visualizer (CEV) information in the generated Boo...
rustanleino
2009-08-15
*
Fixed bug where the remove-empty-blocks optimization had not updated the star...
rustanleino
2009-08-13
*
Changes needed in order to build Boogie using a freshly built Spec# compiler ...
mikebarnett
2009-08-10
*
Fixed problem where nullary function with definition had caused a crash.
rustanleino
2009-08-07
*
Fixed bug that used != instead of == in one translation of fresh.
rustanleino
2009-08-06
*
Made trigger more liberal for int_2_U U_2_int axiom.
rustanleino
2009-07-30
*
Deleting another stray file.
mikebarnett
2009-07-15
*
Deleting the individual user options files.
mikebarnett
2009-07-15
*
Initial set of files.
mikebarnett
2009-07-15