summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* Boogie:Gravatar rustanleino2010-02-20
* added an option /doModSetAnalysis specially for ZvonimirGravatar qadeer2010-02-20
* Fix up the polymorphic case for lambda; it probably still isn't quite correct.Gravatar MichalMoskal2010-02-19
* Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda expressions;...Gravatar MichalMoskal2010-02-19
* Boogie (Util): Added an Emacs flymake extension for BoogiePL.Gravatar wuestholz2010-02-19
* Boogie (Emacs mode): Added an alternative Emacs mode for BoogiePL. It support...Gravatar wuestholz2010-02-19
* Update to F# 1.9.9.9.Gravatar MichalMoskal2010-02-18
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
* * Added "deprecated" comment in help message about /interprocInfer switch. T...Gravatar rustanleino2010-02-18
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linea...Gravatar qadeer2010-02-16
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
* Boogie: Peephole optimization to reduce depth of formulas created during VC ...Gravatar rustanleino2010-02-15
* eliminated the line printing version number in the golden outputGravatar qadeer2010-02-13
* Dafny:Gravatar rustanleino2010-02-13
* (no commit message)Gravatar qadeer2010-02-12
* 1. Fixed bug in StandardVisitor.sscGravatar qadeer2010-02-09
* Boogie: /useArrayTheory currently implies /monomorphizeGravatar rustanleino2010-02-09
* Fix a bug in checking for {:inline} procedure attribute. Resolves #6993.Gravatar MichalMoskal2010-02-08
* Use reflection to read version string from assembly when displaying logo info...Gravatar stobies2010-02-08
* Removed Unicode chars from Assembly attributes - they are not liked too much ...Gravatar stobies2010-02-08
* Preparing Isabelle plugin sources for VCC release.Gravatar stobies2010-02-08
* Dafny: Added if-then-else expressions (replacing and extending the previous b...Gravatar rustanleino2010-02-04
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
* Dafny: Added support for big integers.Gravatar rustanleino2010-01-28
* bugfixGravatar schaef2010-01-28
* Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebu...Gravatar schaef2010-01-28
* Fixed bug in DEFTYPE declarations for maps. Made sure that argument and resu...Gravatar qadeer2010-01-28
* Implemented the command line switch /useArrayTheory. This switch should be u...Gravatar qadeer2010-01-21
* Chalice: Implemented -vs switch, for use when running Chalice from inside Vi...Gravatar rustanleino2010-01-15
* Dafny:Gravatar rustanleino2010-01-14
* Dafny: updated to reflect Boogie's new parsing of function argumentsGravatar rustanleino2010-01-07
* Chalice: updated Prelude to match new Boogie parsing of function parameters; ...Gravatar rustanleino2010-01-06
* Doomed checking now uses the counterexample trace to minimize the number of t...Gravatar schaef2009-12-18
* Allow ":" in addition to "returns" in function definitions. Make the pretty-p...Gravatar MichalMoskal2009-12-17
* Add makefile for running tests, allows "make -j4" to utilize multiple cores.Gravatar MichalMoskal2009-12-17
* Remove vcc1 testcase that never worked with Boogie2 and is testing obsolete b...Gravatar MichalMoskal2009-12-17
* Added prover plugin for Isabelle/HOL.Gravatar sboehme2009-12-14
* Revert the matching depth limit change from previous checkin: would break VCC.Gravatar MichalMoskal2009-12-10
* Z3 parameters to help it bail out of fruitless searches fasterGravatar mkawa2009-12-05
* print attributes in AssertCmd.EmitGravatar mkawa2009-12-02
* Added code to (once again) print out prover warnings (under the /proverWarnin...Gravatar rustanleino2009-11-26
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
* Added resolution and translation of algebraic datatypes and (in function bodi...Gravatar rustanleino2009-11-20
* Setting up test cases for BCTGravatar schaef2009-11-20
* (no commit message)Gravatar schaef2009-11-20
* Support {:PossiblyUnreachable} attribute on assertsGravatar MichalMoskal2009-11-20
* Fixed bug in inlining (procedure *definitions* had been traversed by Standard...Gravatar rustanleino2009-11-19
* doomed stuff: minor bug fixes / improved output / more test casesGravatar schaef2009-11-19
* modified the doom checking. It is now able to report only the relevant statem...Gravatar schaef2009-11-18
* Update use of CCI's API for decompiling the IL model to the Code Model.Gravatar mikebarnett2009-11-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-10 02:34:56 +0000