| Commit message (Expand) | Author | Age |
* | fixed bug in model printing | Unknown | 2013-03-11 |
* | 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 |
* | | | 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 incom... | Unknown | 2013-03-07 |
| * | | Fix LeastCommonAncestor method in Graph module | Nathan Chong | 2013-03-07 |
* | | | Merge | Unknown | 2013-03-06 |
|\ \ \
| | |/
| |/| |
|
* | | | in the process of adding support for linear sets without /useArrayTheory | 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 Codepl... | Rustan Leino | 2013-03-05 |
| * | | fixed datatype bug reported by Chris | Unknown | 2013-03-05 |
|/ / |
|
| * | 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 |
* | | 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 rel... | allydonaldson | 2013-03-01 |
* | | 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 |
| * | | fixed another bug reported by ChrisHaw | Unknown | 2013-02-12 |
| * | | Further bug fixes in OG | Unknown | 2013-02-05 |
| * | | fixed bug in OG | Unknown | 2013-02-01 |
| * | | handling old() in stable assertions | Unknown | 2013-01-30 |
| * | | 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 |
| * | | added owicki-gries and linear-set to boogiedriver | Unknown | 2013-01-25 |
| * | | 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 prett... | Rustan Leino | 2013-01-17 |
* | | Timeout in AbstractHoudini | akashlal | 2013-01-16 |
* | | Allow attributes on procedure formals, function formals, and bound variables | Unknown | 2013-01-07 |
* | | Some code clean-up | Unknown | 2013-01-07 |
* | | Removed old comments about "BASEMOVE" and other constructor calls, where the ... | Unknown | 2013-01-07 |
* | | bug fix for interaction between inlining and loops | Unknown | 2013-01-04 |
* | | bug fix in model printing | Unknown | 2013-01-04 |