Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | fixed bug in model printing | Unknown | 2013-03-11 |
| | | | | reverted a previous erroneous fix I had made in model parsing | ||
* | Added another constructor to CallCmd | akashlal | 2013-03-11 |
| | |||
* | Minor changes to AbstractHoudini | akashlal | 2013-03-10 |
| | |||
* | Merge | Unknown | 2013-03-09 |
|\ | |||
* | | fixed emitter for CallCmd to include async | Unknown | 2013-03-09 |
| | | |||
| * | Refactored MatchCandidate | allydonaldson | 2013-03-08 |
| | | |||
| * | Merge | allydonaldson | 2013-03-08 |
| |\ | |||
| * | | MatchCandidate modified to match candidates by variable name, rather than by ↵ | allydonaldson | 2013-03-08 |
| | | | | | | | | | | | | variable identity. ApplyAssignment method added, which takes a program (not necessarily the same program on which Houdini was invoked, but a program that has the same candidate set), and applies the Houdini assignment to the program. | ||
* | | | Merge | Unknown | 2013-03-07 |
|\ \ \ | | |/ | |/| | |||
* | | | updated the model parsing (probably caused by some change in Z3's output) | Unknown | 2013-03-07 |
| | | | |||
* | | | added support for linear sets without useArrayTheory (but there is some ↵ | Unknown | 2013-03-07 |
| | | | | | | | | | | | | incompletness) | ||
| * | | 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). | ||
* | | | Merge | Unknown | 2013-03-06 |
|\ \ \ | | |/ | |/| | |||
* | | | in the process of adding support for linear sets without /useArrayTheory | Unknown | 2013-03-06 |
| |/ |/| | |||
* | | removed Test\GPUVerify | Unknown | 2013-03-06 |
| | | |||
* | | removing GPUVerify and Dafny.sln | Unknown | 2013-03-05 |
| | | |||
* | | Merge | Rustan Leino | 2013-03-05 |
|\ \ | |||
* | | | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵ | Rustan Leino | 2013-03-05 |
| | | | | | | | | | | | | Codeplex repositories. | ||
* | | | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵ | Rustan Leino | 2013-03-05 |
| | | | | | | | | | | | | Codeplex repositories. | ||
| * | | fixed datatype bug reported by Chris | Unknown | 2013-03-05 |
|/ / | | | | | | | fixed function body referring to globals bug | ||
| * | Merge | allydonaldson | 2013-03-05 |
| |\ | |/ |/| | |||
* | | fixed a bug in og | Unknown | 2013-03-04 |
| | | |||
* | | fixed bugs in both parallel calls and linear stuff (reported by Chris) | Unknown | 2013-03-03 |
| | | | | | | | | also added improved error reporting suggested by Chris | ||
* | | bug in OG for parallel call | Unknown | 2013-03-02 |
| | | |||
* | | added parallel calls | Unknown | 2013-03-01 |
| | | |||
| * | Merge | allydonaldson | 2013-03-01 |
| |\ | |/ |/| | |||
| * | Fixed bug with predication, and fixed small problem with model generation ↵ | allydonaldson | 2013-03-01 |
| | | | | | | | | related to casting | ||
* | | removed call forall and * args to calls | Unknown | 2013-02-23 |
| | | |||
* | | CR/LF line ending delta | Rustan Leino | 2013-02-19 |
| | | |||
* | | Merge | Rustan Leino | 2013-02-19 |
|\ \ | |||
* | | | Fixed some type bugs in the interval domain. | Rustan Leino | 2013-02-19 |
| | | | |||
| * | | AbstractHoudini: more details for computing a tighter predicate cover | Unknown | 2013-02-15 |
| | | | |||
| * | | fixed bugs in typechecking of linear sets | Unknown | 2013-02-13 |
| | | | | | | | | | | | | | | | added regressions to linear sets removed the need to supply the builtin map operations manually | ||
| * | | Add another test file | Unknown | 2013-02-12 |
| | | | |||
| * | | fixed another bug reported by ChrisHaw | Unknown | 2013-02-12 |
| | | | | | | | | | | | | Added an answer file | ||
| * | | finished the sample | Unknown | 2013-02-05 |
| | | | |||
| * | | Further bug fixes in OG | Unknown | 2013-02-05 |
| | | | | | | | | | | | | Added another sample | ||
| * | | fixed bug in OG | Unknown | 2013-02-01 |
| | | | | | | | | | | | | added another OG sample illustrating rely-guarantee encoding | ||
| * | | handling old() in stable assertions | Unknown | 2013-01-30 |
| | | | | | | | | | | | | bug fix in linear | ||
| * | | Merge | Unknown | 2013-01-29 |
| |\ \ | |||
| * | | | made a whole bunch of changes to linear and og stuff | Unknown | 2013-01-29 |
| | | | | |||
| | * | | Parse integers returned by Z3 into BigNum | akashlal | 2013-01-29 |
| |/ / | |||
| * | | bug fix reported by Chris | Unknown | 2013-01-28 |
| | | | |||
| * | | updated answer files | Unknown | 2013-01-25 |
| | | | | | | | | | | | | og and linear creates some rearrangement of blocks | ||
| * | | added owicki-gries and linear-set to boogiedriver | Unknown | 2013-01-25 |
| | | | | | | | | | | | | cleaned up the async type checking | ||
| * | | first check in of Owicki-Gries and linear sets | Unknown | 2013-01-24 |
| | | | |||
| * | | Output to Boogie\Binaries even in the Release version | Unknown | 2013-01-25 |
|/ / | |||
* | | Let Boogie clients determine their own version string | Rustan Leino | 2013-01-23 |
| | | |||
* | | Refactored code that generates an axiom for a function, and changed the ↵ | Rustan Leino | 2013-01-17 |
| | | | | | | | | pretty printing to always reflect when a function body is inlined | ||
* | | Timeout in AbstractHoudini | akashlal | 2013-01-16 |
| | |