{"push_id":1308790330,"size":7,"distinct_size":7,"ref":"refs/heads/master","head":"c38729c4b8903caed7265e26e1cef36d10ad48ec","before":"87d31dea2f94e386a62ae7e6956427fc75d7bc6e","commits":[{"sha":"891587b95ab13e9fef2fbfad7bf7f617ce990c74","author":{"name":"RustanLeino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"Ignore Binaries/export and Package folders","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/891587b95ab13e9fef2fbfad7bf7f617ce990c74"},{"sha":"33c67a5335b6fb1b41a90273391b7593f4f2e557","author":{"name":"RustanLeino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"Added \"unchanged\" predicates.\nRemoved \"reads\" clauses for two-state lemmas (the idea is to instead use the more general, and less confusing, \"unchanged\" predicates).","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/33c67a5335b6fb1b41a90273391b7593f4f2e557"},{"sha":"b0089a2265fe8f15277f3b18465115afebc0b811","author":{"name":"RustanLeino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"Syntax highlight bitvector types","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/b0089a2265fe8f15277f3b18465115afebc0b811"},{"sha":"b3cc5696b02f05e04c0335d1baf312ab9926e275","author":{"name":"Rustan Leino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"fixed crash in parser","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/b3cc5696b02f05e04c0335d1baf312ab9926e275"},{"sha":"431dd00cd5fa7c38cb80c4e0d62999bf0e7e720c","author":{"name":"Rustan Leino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"Added \"allocated\" expressions, which say that the argument expression, which can be of any type,\nis available in the state.  The \"allocated\" expression is typically used with \"old\", as in\n\"old(allocated(E))\" (note that \"E\" also sits inside the \"old\" in this example).\n\nChanged \"fresh\" so that no longer is allowed to take a datatype argument (which was kinda bogus\nanyway).  Where \"!fresh(D)\" was used before, try \"old(allocated(D))\" instead.\n\nChanged semantics of \"fresh\", so that its value on a (set/seq) collection is simply the fold\nof \"fresh\" on all of the elements.  In particular, this means that if the collection contains\n\"null\", then \"fresh\" will return \"false\".  This is likely to affect some classes specified with\nalmost-the-standard dynamic-frames idiom -- make sure \"Valid()\" includes a conjunct \"null !in Repr\".\n\nFixed bug in the verification translation of local variables without initializing assignments.\n\nImproved triggers in some \"fresh(S)\" expressions, where \"S\" is a set of references.","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/431dd00cd5fa7c38cb80c4e0d62999bf0e7e720c"},{"sha":"2b9a9e4880c82b232f09e64848a11a245585f8e8","author":{"name":"Rustan Leino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"tests and corrections for unchanged","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/2b9a9e4880c82b232f09e64848a11a245585f8e8"},{"sha":"c38729c4b8903caed7265e26e1cef36d10ad48ec","author":{"name":"RustanLeino","email":"a92f2703da90e09d9b33889cd2a475ffa39cd065@microsoft.com"},"message":"Merge branch 'master' of https://github.com/Microsoft/dafny\n\nMerge.","distinct":true,"url":"https://api.github.com/repos/Microsoft/dafny/commits/c38729c4b8903caed7265e26e1cef36d10ad48ec"}]}
{"actor":{"display_login":"RustanLeino"}}