summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* refactored og and fixed latest bug reported by chrisGravatar Unknown2013-03-20
* the allocator corresponding to every linear variableGravatar Unknown2013-03-13
* Added explicit mod set analysis calls to OG transform and linear transformGravatar Unknown2013-03-13
* added mod set checking to the linear type checkerGravatar Unknown2013-03-13
* fixed bugs in linear and ogGravatar Unknown2013-03-11
* fixed bug in model printingGravatar Unknown2013-03-11
* Added another constructor to CallCmdGravatar akashlal2013-03-11
* Minor changes to AbstractHoudiniGravatar akashlal2013-03-10
* MergeGravatar Unknown2013-03-09
|\
* | fixed emitter for CallCmd to include asyncGravatar Unknown2013-03-09
| * Refactored MatchCandidateGravatar allydonaldson2013-03-08
| * MergeGravatar allydonaldson2013-03-08
| |\
| * | MatchCandidate modified to match candidates by variable name, rather than by ...Gravatar allydonaldson2013-03-08
* | | MergeGravatar Unknown2013-03-07
|\ \ \ | | |/ | |/|
* | | updated the model parsing (probably caused by some change in Z3's output)Gravatar Unknown2013-03-07
* | | added support for linear sets without useArrayTheory (but there is some incom...Gravatar Unknown2013-03-07
| * | Fix LeastCommonAncestor method in Graph moduleGravatar Nathan Chong2013-03-07
* | | MergeGravatar Unknown2013-03-06
|\ \ \ | | |/ | |/|
* | | in the process of adding support for linear sets without /useArrayTheoryGravatar Unknown2013-03-06
| |/ |/|
* | removing GPUVerify and Dafny.slnGravatar Unknown2013-03-05
* | MergeGravatar Rustan Leino2013-03-05
|\ \
* | | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl...Gravatar Rustan Leino2013-03-05
| * | fixed datatype bug reported by ChrisGravatar Unknown2013-03-05
|/ /
| * MergeGravatar allydonaldson2013-03-05
| |\ | |/ |/|
* | fixed a bug in ogGravatar Unknown2013-03-04
* | fixed bugs in both parallel calls and linear stuff (reported by Chris)Gravatar Unknown2013-03-03
* | bug in OG for parallel callGravatar Unknown2013-03-02
* | added parallel callsGravatar Unknown2013-03-01
| * MergeGravatar allydonaldson2013-03-01
| |\ | |/ |/|
| * Fixed bug with predication, and fixed small problem with model generation rel...Gravatar allydonaldson2013-03-01
* | removed call forall and * args to callsGravatar Unknown2013-02-23
* | CR/LF line ending deltaGravatar Rustan Leino2013-02-19
* | MergeGravatar Rustan Leino2013-02-19
|\ \
* | | Fixed some type bugs in the interval domain.Gravatar Rustan Leino2013-02-19
| * | AbstractHoudini: more details for computing a tighter predicate coverGravatar Unknown2013-02-15
| * | fixed bugs in typechecking of linear setsGravatar Unknown2013-02-13
| * | fixed another bug reported by ChrisHawGravatar Unknown2013-02-12
| * | Further bug fixes in OGGravatar Unknown2013-02-05
| * | fixed bug in OGGravatar Unknown2013-02-01
| * | handling old() in stable assertionsGravatar Unknown2013-01-30
| * | MergeGravatar Unknown2013-01-29
| |\ \
| * | | made a whole bunch of changes to linear and og stuffGravatar Unknown2013-01-29
| | * | Parse integers returned by Z3 into BigNumGravatar akashlal2013-01-29
| |/ /
| * | bug fix reported by ChrisGravatar Unknown2013-01-28
| * | added owicki-gries and linear-set to boogiedriverGravatar Unknown2013-01-25
| * | first check in of Owicki-Gries and linear setsGravatar Unknown2013-01-24
| * | Output to Boogie\Binaries even in the Release versionGravatar Unknown2013-01-25
|/ /
* | Let Boogie clients determine their own version stringGravatar Rustan Leino2013-01-23
* | Refactored code that generates an axiom for a function, and changed the prett...Gravatar Rustan Leino2013-01-17
* | Timeout in AbstractHoudiniGravatar akashlal2013-01-16