| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Rename DLLs to non-generic names by prefixing "Boogie". Project names and |  akashlal | 2016-04-15 |
| | | | | | namespaces remain the same. | ||
| * | Normalise line endings using a .gitattributes file. Unfortunately |  Dan Liew | 2015-06-28 |
| | | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | ||
| * | Fix Boogie so it compiled with mono. Patch by Dan Liew. |  Ally Donaldson | 2014-01-14 |
| | | |||
| * | added the QED build configuration | qadeer | 2013-12-02 |
| | | |||
| * | Fixes to predication. Patch by Jeroen Ketema. | Ally Donaldson | 2013-11-06 |
| | | |||
| * | new option for reversing the topological order - this could potentially help ↵ |  Pantazis Deligiannis | 2013-08-19 |
| | | | | | to speedup houdini refutation of candidates | ||
| * | merge | Pantazis Deligiannis | 2013-07-06 |
| |\ | |||
| | * | Adapted method for computing dual of graph so that it copes with graphs that ↵ | allydonaldson | 2013-06-28 |
| | | | | | | | | | exhibit exit-free cycles | ||
| * | | CVC4 Parser | pantazis | 2013-06-12 |
| |/ | |||
| * | Staged Houdini | allydonaldson | 2013-04-30 |
| | | |||
| * | Fix LeastCommonAncestor method in Graph module |  Nathan Chong | 2013-03-07 |
| | | | | | | | | | | | | | | | | | Solves a problem with Uniformity Analysis in GPUVerify. "The least common ancestor of two nodes u and v in a rooted tree T is a node w that is an ancestor of both u and v and that has the greatest depth in T" (CLR). This is needed when computing the control dependence relation of a CFG. In this case, we need the least common ancestor of a pair of nodes in the dominator tree so we can reuse the 'intersect' function given by Cooper et al in "A Simple, Fast Dominance Algorithm." The old code picked the ancestor of both u and v that has the *least* depth in T. This caused uniformity analysis, in GPUVerify, to be imprecise (adding blocks as non-uniform when they were infact uniform). | ||
| * | CR/LF line ending delta | Rustan Leino | 2013-02-19 |
| | | |||
| * | 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 | ||
| * | Uniformity analysis. Patch by Peter Collingbourne. |  Unknown | 2012-09-18 |
| | | |||
| * | Graph: make DomRelation and DominatorMap public |  Peter Collingbourne | 2012-07-11 |
| | | |||
| * | Boogie: add /printCFG command line option, which prints each ↵ | Peter Collingbourne | 2012-06-06 |
| | | | | | implementation's CFG in Graphviz format | ||
| * | Fix DomRelation.DominatedBy for the case where the dominator is the source | Peter Collingbourne | 2012-05-22 |
| | | |||
| * | added code to handle irreducible graphs |  qadeer | 2011-08-20 |
| | | |||
| * | full port of houdini project | qadeer | 2011-08-04 |
| | | |||
| * | Call PostOrderVisitIterative by default |  Unknown | 2011-06-26 |
| | | |||
| * | Added an iterative version of PostOrderVisit (but it is not called) | Unknown | 2011-06-26 |
| | | |||
| * | Re-enabled quantifier checking in the Checked configuration. | mikebarnett | 2011-03-16 |
| | | |||
| * | Turn off quantifier checking in the runtime checking. | mikebarnett | 2011-03-14 |
| | | |||
| * | Replaced all dictionaries that mapped to bool (i.e., were being used to ↵ | mikebarnett | 2011-03-10 |
| | | | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. | ||
| * | 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. | ||
| * | Added a new solution configuration, Checked, that builds the Checked ↵ | mikebarnett | 2011-03-07 |
| | | | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration. | ||
| * | Added version.cs as link to those projects that were missing it | stobies | 2010-12-06 |
| | | | | | Select 4.0 client profile on all projects | ||
| * | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | qadeer | 2010-12-01 |
| | | |||
| * | Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵ | qadeer | 2010-11-27 |
| | | | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0. | ||
| * | Update to VS2010. | MichalMoskal | 2010-10-07 |
| | | |||
| * | fixed bug in extract loops by ensuring that loop extraction is done in ↵ | qadeer | 2010-09-01 |
| | | | | | nesting order | ||
| * | created a new build target called z3apidebug. | qadeer | 2010-08-29 |
| | | | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver. | ||
| * | Boogie: Removed some errors with code contracts (commenting out ↵ | tabarbe | 2010-08-27 |
| | | | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however). | ||
| * | Boogie: Changed the cce classes into one separate project, which every other ↵ | tabarbe | 2010-08-27 |
| | | | | | project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods. | ||
| * | Boogie: Graph port 2/3: Committing new source file, deleting old one | tabarbe | 2010-08-27 |
| | | |||
| * | Boogie: Graph port 1/3: Committing new sources | tabarbe | 2010-08-27 |
| | | |||
| * | Boogie: Renaming the Graph files in preparation for the commit of my port. | tabarbe | 2010-08-27 |
| | | |||
| * | Boogie: Removed trailing spaces in code | tabarbe | 2010-08-04 |
| | | |||
| * | * Added "deprecated" comment in help message about /interprocInfer switch. ↵ | rustanleino | 2010-02-18 |
| | | | | | | | | The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods | ||
| * | Sign assemblies | stobies | 2009-08-17 |
| | | |||
| * | Initial set of files. | mikebarnett | 2009-07-15 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |