Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵ | Rustan Leino | 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 | Rustan Leino | 2014-02-10 |
| | |||
* | bug fix in error trace printing | qadeer | 2014-02-05 |
| | | | | added a class for Token elimination (not done yet) | ||
* | added syntax for par call and ParCallCmd | qadeer | 2013-12-16 |
| | |||
* | Merge | qadeer | 2013-10-15 |
|\ | |||
* | | bug fix in yield inference in modset analysis | qadeer | 2013-10-15 |
| | | |||
| * | Merge | Pantazis Deligiannis | 2013-10-09 |
| |\ | |/ |/| | |||
| * | more changes towards parallelisation of Houdini | Pantazis Deligiannis | 2013-09-29 |
| | | |||
* | | fixed the linear type checking related to globals | qadeer | 2013-09-04 |
| | | | | | | | | | | fixed the modset analysis so that it infers the stable predicate also added more information to type error messages | ||
| * | Merge | Pantazis Deligiannis | 2013-08-20 |
| |\ | |/ |/| | |||
| * | new option for reversing the topological order - this could potentially help ↵ | Pantazis Deligiannis | 2013-08-19 |
| | | | | | | | | to speedup houdini refutation of candidates | ||
* | | cleaned up the OG code | qadeer | 2013-08-07 |
|/ | | | | enabled it to be always on | ||
* | Removed the remaining pure collections. | wuestholz | 2013-07-23 |
| | |||
* | CmdSeq: farewell | Ally Donaldson | 2013-07-22 |
| | |||
* | Started to remove ...Seq classes | Ally Donaldson | 2013-07-22 |
| | |||
* | More refactoring towards replacing PureCollections.Sequence with List | Ally Donaldson | 2013-07-22 |
| | |||
* | Merge | allydonaldson | 2013-04-30 |
|\ | |||
* | | Staged Houdini | allydonaldson | 2013-04-30 |
| | | |||
| * | Fix mod-set traversal to do visit code inside code expressions. | Rustan Leino | 2013-04-18 |
|/ | |||
* | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | Unknown | 2013-01-07 |
| | | | | conversion from Spec# into C# moved a constructor call | ||
* | bunch of refactorings | Unknown | 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 | qadeer | 2011-06-14 |
| | |||
* | fixed a bug in block coalescer. previously, an unreachable block could have ↵ | qadeer | 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 ↵ | mikebarnett | 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 | akashlal | 2010-12-16 |
| | |||
* | fixed a couple of issues: | qadeer | 2010-12-16 |
| | | | | | 1. eliminated special case for alloc 2. added iteration over out parameters in VisitCallCmd | ||
* | Changed the behavior of /doModSetAnalysis so that | qadeer | 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 | qadeer | 2010-12-01 |
| | |||
* | Get rid of some CCI dependencies in Driver | MichalMoskal | 2010-10-07 |
| | |||
* | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | tabarbe | 2010-08-27 |
| | | | | fewer error messages when compiling with runtime checking on. | ||
* | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |