summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* 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
* boogie.exe: allow to reset the command line options so we can re-use the boog...Gravatar stobies2011-04-01
* Minor fixesGravatar schaef2011-03-27
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Made CallCmd.callee public for easy manipulation of un-resolved programsGravatar akashlal2011-03-21
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
* new algorithm for dead code detection (vc:doomed)Gravatar schaef2011-03-15
* Add labels to extracted procedures for loopsGravatar akashlal2011-03-14
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Added a new solution configuration, Checked, that builds the Checked configur...Gravatar mikebarnett2011-03-07
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
* Add IEnumerable.Concat1 method.Gravatar MichalMoskal2011-02-23
* Fix help for /mvGravatar MichalMoskal2011-02-18
* Boogie: Fixed problem with binding power of .[.] versus type coercions in pre...Gravatar rustanleino2011-02-17
* Provide /p: as the short form of /proverOpt:.Gravatar MichalMoskal2011-02-17
* Add IEnumerable.IterGravatar MichalMoskal2011-02-17
* Stratified inlining: Added concrete values to error traces. Added an extra fl...Gravatar akashlal2011-02-17
* Add some extension methods to IEnumberable<T>Gravatar MichalMoskal2011-02-15
* Fix a bug in cloning of nested lambda expressions in AI engineGravatar MichalMoskal2011-02-11
* Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP prove...Gravatar MichalMoskal2011-02-11
* Get rid of some warnings.Gravatar MichalMoskal2011-02-11
* Changed the API for Declaration.AddAttribute so it takes a params argument so...Gravatar mikebarnett2011-02-09
* Added a new method StratifiedVC for refinement.Gravatar akashlal2011-02-08
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
* Boogie: Eliminated a couple of warnings by removing unused variable declarati...Gravatar wuestholz2011-01-21
* Add description of {:selective_checking} to the /attrHelp. Fix the testcase.Gravatar MichalMoskal2011-01-13
* fixed a small bug in inline codeGravatar qadeer2010-12-20
* A couple of bug fixesGravatar akashlal2010-12-16
* fixed a couple of issues:Gravatar qadeer2010-12-16
* Cleanup up the inlining codeGravatar qadeer2010-12-15
* Changed the behavior of /doModSetAnalysis so thatGravatar qadeer2010-12-15
* Add ToString() overrides to help in debuggingGravatar MichalMoskal2010-12-10
* z3api: Bug fix with timeout. Use CheckAssumptions.Gravatar akashlal2010-12-07
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
* Factored out the ParserHelper class into a separate project and updated the f...Gravatar wuestholz2010-12-02
* Get rid of F# dependencies - use System.Numerics and a custom Rational struct...Gravatar MichalMoskal2010-12-02