{"push_id":1410464110,"size":10,"distinct_size":10,"ref":"refs/heads/master","head":"b37e0b0384fd6fa64ae669edbf1652f4a6fa18af","before":"cdc8cab7d4cd0b5996212d9e0a3b6bac2393e6f7","commits":[{"sha":"37815e45b1855f0fade7ca9a21b0150335196822","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Allow produce_lemma_function_pointer_chunk blocks to call local lemmas","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/37815e45b1855f0fade7ca9a21b0150335196822"},{"sha":"34082d95720231fff8fab26f3a16e99cb71464ea","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Basic termination verification for Java\n\n- 'terminates' clause in method/constructor contracts\n- Upcalls (statically bound calls of methods declared earlier in the\n  program text) are allowed; other calls consume a call permission chunk\n  of the form call_perm_(c) where c is the Class object of the target\n  class.\n- Loops that do not have a 'decreases' clause consume a call_perm_(c)\n  chunk at the end of each iteration, where c is the class containing the\n  loop.\n- The 'produce_call_below_perm_();' ghost statement produces a\n  call_below_perm_(c) chunk, where c is the Class object of the current\n  class.\n- The axioms for deriving call_perm_ chunks from call_below_perm_ chunks\n  are not hardcoded into the tool. A simple example set of axioms is shown\n  in _call_perms.javaspec, which is based on the approach described in our\n  ECOOP 2015 paper. See PlusOneFunc.java for an example of how these\n  axioms can be used to modularly verify a program involving dynamically\n  bound method calls.\n\nTODO:\n- Emit Class_lt facts\n- More examples","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/34082d95720231fff8fab26f3a16e99cb71464ea"},{"sha":"f06cf4829fcb4485b2de03bd1e3fbfa14351da44","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Fix func_lt axiomatization\n\nWeakens the axiomatization to avoid unsound implications. In\nparticular, prevents a module that imports a module that\ndeclares functions 'foo' and 'bar' from being able to prove\n!func_lt(foo, bar) and !func_lt(bar, foo).","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/f06cf4829fcb4485b2de03bd1e3fbfa14351da44"},{"sha":"b9f274da6d2046b5e613ecb112c5ecd9d8345824","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Improve readability of test suite report\n\nBy default, mysh now produces more concise and more readable output.\nYou can get the old output by supplying the -verbose option.\nYou can get even more concise output by supplying the -dots option.\n\nTODO:\n- Extend the mysh input language with explicit sequential blocks and parallel\n  blocks. Support sequential blocks within parallel blocks.\n- Replace the (long-running) nested mysh calls in the test suite by\n  includes to get more fine-grained reporting.\n- Investigate the longest-running test cases to see if they can be made to\n  run faster.","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/b9f274da6d2046b5e613ecb112c5ecd9d8345824"},{"sha":"fa443e583dbc0ebf55170b3f3a2c5f617c0ded1d","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Improve typechecking of shift operators","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/fa443e583dbc0ebf55170b3f3a2c5f617c0ded1d"},{"sha":"ccd7051c79e2af6df845354e3eff65a0ce6c7645","author":{"name":"Martin Vassor","email":"a44e2c8ff33719fc0ec3ea3e76d54139c18ebb0d@epfl.ch"},"message":"sizeof(long long); llong pointee and array predicates (#58)","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/ccd7051c79e2af6df845354e3eff65a0ce6c7645"},{"sha":"f2c5325032750a1cc5658cc164bae339cca98006","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Allow shift by unsigned int\n\nFixes #60.","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/f2c5325032750a1cc5658cc164bae339cca98006"},{"sha":"88b4f8b1049b538b80eb8feef368d731616e761b","author":{"name":"Jan Tobias Muehlberg","email":"320b12eac18142fd596b7c7806cd3125f48b3af7@gmail.com"},"message":"Minor: Updated build instructions.","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/88b4f8b1049b538b80eb8feef368d731616e761b"},{"sha":"61fadb8d11b75ff0527b53bf3de0cb3320a9d2b5","author":{"name":"Bart Jacobs","email":"ca4e65b12769f54f0b60581b479b8ea6b73a7ff7@cs.kuleuven.be"},"message":"Update README.md","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/61fadb8d11b75ff0527b53bf3de0cb3320a9d2b5"},{"sha":"b37e0b0384fd6fa64ae669edbf1652f4a6fa18af","author":{"name":"Martin Vassor","email":"a44e2c8ff33719fc0ec3ea3e76d54139c18ebb0d@epfl.ch"},"message":"Add predicate \"ullongs\" (#63)\n\nand move \"llongs\" predicate for better placement (leave ints and uints\r\nclose to each other).","distinct":true,"url":"https://api.github.com/repos/gijsvanspauwen/verifast/commits/b37e0b0384fd6fa64ae669edbf1652f4a6fa18af"}]}
{"actor":{"display_login":"gijsvanspauwen"}}