Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merging complete. Everything looks good *crosses fingers* | 2016-06-06 | |
| | |||
* | Made 2 invariants of class 'VariableCollector' robust by: | 2015-01-09 | |
| | | | | | | - making field protected - exposing IEnumerables (with help from David Rohr) | ||
* | Worked on the verification result caching. | 2014-11-05 | |
| | |||
* | Worked on the verification result caching. | 2014-10-17 | |
| | |||
* | Did some refactoring. | 2014-10-16 | |
| | |||
* | Did more refactoring and addressed several todos. | 2014-09-23 | |
| | |||
* | Did some refactoring. | 2014-09-23 | |
| | |||
* | Implemented an optimization for assignments to assumption variables that are ↵ | 2014-07-04 | |
| | | | | injected by the verification result caching for calls within loops. | ||
* | Fixed a bug in revised mod set analysis | 2014-06-06 | |
| | |||
* | Refactored modset analysis to avoid the use of static fields. Static fields ↵ | 2014-06-06 | |
| | | | | cause data races when we run parts of Boogie that both do mod set analysis at the same time. | ||
* | checkpoint | 2014-05-03 | |
| | |||
* | (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵ | 2014-02-24 | |
| | | | | | | of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor. | ||
* | Fixed errors in the use of Code Contracts | 2014-02-10 | |
| | |||
* | bug fix in error trace printing | 2014-02-05 | |
| | | | | added a class for Token elimination (not done yet) | ||
* | added syntax for par call and ParCallCmd | 2013-12-16 | |
| | |||
* | Merge | 2013-10-15 | |
|\ | |||
* | | bug fix in yield inference in modset analysis | 2013-10-15 | |
| | | |||
| * | Merge | 2013-10-09 | |
| |\ | |/ |/| | |||
| * | more changes towards parallelisation of Houdini | 2013-09-29 | |
| | | |||
* | | fixed the linear type checking related to globals | 2013-09-04 | |
| | | | | | | | | | | fixed the modset analysis so that it infers the stable predicate also added more information to type error messages | ||
| * | Merge | 2013-08-20 | |
| |\ | |/ |/| | |||
| * | new option for reversing the topological order - this could potentially help ↵ | 2013-08-19 | |
| | | | | | | | | to speedup houdini refutation of candidates | ||
* | | cleaned up the OG code | 2013-08-07 | |
|/ | | | | enabled it to be always on | ||
* | Removed the remaining pure collections. | 2013-07-23 | |
| | |||
* | CmdSeq: farewell | 2013-07-22 | |
| | |||
* | Started to remove ...Seq classes | 2013-07-22 | |
| | |||
* | More refactoring towards replacing PureCollections.Sequence with List | 2013-07-22 | |
| | |||
* | Merge | 2013-04-30 | |
|\ | |||
* | | Staged Houdini | 2013-04-30 | |
| | | |||
| * | Fix mod-set traversal to do visit code inside code expressions. | 2013-04-18 | |
|/ | |||
* | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | 2013-01-07 | |
| | | | | conversion from Spec# into C# moved a constructor call | ||
* | bunch of refactorings | 2012-10-03 | |
| | | | | | | | | | - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs | ||
* | bug fix in live variable analysis | 2011-06-14 | |
| | |||
* | fixed a bug in block coalescer. previously, an unreachable block could have ↵ | 2011-05-04 | |
| | | | | as a target a block that was coalesced. this caused a contract to fail downstream (under checked build). in the new behavior, the new blocks after coalescing only contain reachable blocks. | ||
* | Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵ | 2011-03-10 | |
| | | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked. | ||
* | A couple of bug fixes | 2010-12-16 | |
| | |||
* | fixed a couple of issues: | 2010-12-16 | |
| | | | | | 1. eliminated special case for alloc 2. added iteration over out parameters in VisitCallCmd | ||
* | Changed the behavior of /doModSetAnalysis so that | 2010-12-15 | |
| | | | | | (1) Boogie errors due to modifies clause mismatch are suppressed (2) modset analysis is performed and modifies clauses of procedures with implementations are updated | ||
* | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | 2010-12-01 | |
| | |||
* | Get rid of some CCI dependencies in Driver | 2010-10-07 | |
| | |||
* | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | 2010-08-27 | |
| | | | | fewer error messages when compiling with runtime checking on. | ||
* | Boogie: Committing changed source files | 2010-08-20 | |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | 2010-08-20 | |