summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Boogie: removed unreachable or unused codeGravatar Rustan Leino2011-10-27
* Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
* Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-10-27
* Boogie: Changed default /prover to SMTLIBGravatar Rustan Leino2011-10-27
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* MergeGravatar Rustan Leino2011-09-28
|\
| * bitvector fixesGravatar qadeer2011-09-24
| * Dafny: Fixed an assertion violation in the "Checked" configuration.Gravatar wuestholz2011-09-20
* | MergeGravatar Rustan Leino2011-09-17
|\ \
| | * Dafny: Added support for attributes on methods and constructors.Gravatar wuestholz2011-09-16
| | * Fixed test failures in the "Checked" configuration.Gravatar wuestholz2011-09-19
| |/
| * Added "free call" statements that don't check the precondition in the caller.Gravatar wuestholz2011-09-14
* | Dafny: generate a compiler error upon encountering an assume statementGravatar Rustan Leino2011-09-11
|/
* further editsGravatar qadeer2011-09-01
* improved bitvector analysisGravatar qadeer2011-09-01
* MergeGravatar qadeer2011-08-29
|\
* | more changes to bitvector analysisGravatar qadeer2011-08-29
| * MergeGravatar Michal Moskal2011-08-29
| |\ | |/ |/|
| * Add PROVER_PATH prover option (to base options, but currently only used by SM...Gravatar Michal Moskal2011-08-29
* | Fixed a bug with "don't care" return value on an async callGravatar Unknown2011-08-24
|/
* Support for irreducible graphs (with extractLoops)Gravatar Unknown2011-08-24
* reverting irreducible handling temporarilyGravatar qadeer2011-08-21
|\
* | added code to handle irreducible graphsGravatar qadeer2011-08-20
* | deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
* | Added "procedure-copy bounding" for lazy inliningGravatar Unknown2011-08-10
* | further updates to bit vector analysisGravatar qadeer2011-08-09
* | more changes to bitvector analysisGravatar qadeer2011-08-09
* | another bug fix in bctGravatar qadeer2011-08-08
* | added a new file and fixed a bug in bctGravatar qadeer2011-08-08
* | various changes to boogie for bitvector analysis and bctproviderGravatar qadeer2011-08-08
* | cleaned up houdini optionsGravatar qadeer2011-08-04
* | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed so...Gravatar wuestholz2011-07-15
* | async call return value is either int or bv32Gravatar qadeer2011-07-09
* | ExtractLoops calls the same code for eliminating unreachable blocks that norm...Gravatar qadeer2011-07-05
* | MergeGravatar Michal Moskal2011-07-05
|\ \
| * | Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to th...Gravatar Unknown2011-07-05
| * | Added the /noCheating option. (treats assume as assert and drops free.)Gravatar Jason Koenig2011-07-01
* | | Allow : instead of = in optionsGravatar Michal Moskal2011-06-30
| |/ |/|
| * Added option to force Dafny compilation, even if verification fails.Gravatar Jason Koenig2011-06-30
|/
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
* early clearing of live variables and incarnation mapsGravatar qadeer2011-06-24
* implementation of iterative LetVCGravatar qadeer2011-06-23
* bug fix in live variable analysisGravatar qadeer2011-06-14
* Boogie: white-space formatingGravatar Rustan Leino2011-06-05
* close the file stream opened by the parserGravatar Unknown2011-05-19
* convert assert to requiresGravatar qadeer2011-05-16
* Boogie: added features to help with modular verification. In particular, defi...Gravatar Rustan Leino2011-05-13
* fixed a bug in block coalescer. previously, an unreachable block could have a...Gravatar qadeer2011-05-04
* fixed a bug in ComputeAllLabelsGravatar qadeer2011-04-27
* Changed label checking for goto targets in StmtList so that they can be any l...Gravatar qadeer2011-04-21