summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* fixed a completeness problem in houdini with inliningGravatar qadeer2011-12-18
* Fixed the Boogie build.Gravatar wuestholz2011-12-16
* Dafny: Made sure that error locations refer to the Dafny program, even if the...Gravatar wuestholz2011-12-15
* Boogie: Changed Expr.Not to keep swap arguments rather change direction of op...Gravatar Rustan Leino2011-12-12
* MergeGravatar Rustan Leino2011-12-07
|\
| * MergeGravatar Michal Moskal2011-12-07
| |\
| * | Fix atg file and add comment about Set/*Variable*/Gravatar Michal Moskal2011-12-07
| * | Make set iteration order deterministicGravatar Michal Moskal2011-12-07
* | | MergeGravatar Rustan Leino2011-12-05
|\ \ \ | | |/ | |/|
* | | Boogie: Added new abstract interpretation harness, which uses native Boogie E...Gravatar Rustan Leino2011-12-05
| |/ |/|
| * Emit attribute on a requiresGravatar akashlal2011-12-04
|/
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
* MergeGravatar qadeer2011-11-22
|\
| * Boogie: don't resolve ignored types (that is, "extern" types that have been t...Gravatar Rustan Leino2011-11-22
* | added support for handling duplicate axiomsGravatar qadeer2011-11-22
|/
* Added lazy summary computation to stratified inlining (not finished yet)Gravatar akashlal2011-11-20
* commented calls to GC.Collect()Gravatar qadeer2011-11-18
* changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
* Boogie: fixed build error (incorrect type in Contract.Result)Gravatar Rustan Leino2011-11-16
* MergeGravatar akashlal2011-11-16
|\
| * Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
* | Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
|/
* changed inlining code so that candidate preconditions and postconditions are ...Gravatar qadeer2011-11-15
* added the option /inlineDepth:n. This option defaults to -1. If the user prov...Gravatar qadeer2011-11-13
* moved the addition of selectors and testers to program.ResolveGravatar qadeer2011-11-11
* MergeGravatar qadeer2011-11-07
|\
| * Dafny: added a new /inductionHeuristic optionGravatar Rustan Leino2011-11-04
| * Dafny: added options to make Induction Heuristic apply to array index express...Gravatar Rustan Leino2011-11-04
* | deleted unused codeGravatar qadeer2011-11-01
|/
* MergeGravatar Rustan Leino2011-10-29
|\
* | Dafny induction:Gravatar Rustan Leino2011-10-29
| * Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
| * Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
| * 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
|/