{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":14519163,"defaultBranch":"master","name":"verifast","ownerLogin":"verifast","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2013-11-19T08:57:02.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/5978124?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1723469994.0","currentOid":""},"activityList":{"items":[{"before":"eadb3beecbd79bddaf1a4567497f89cf17037c69","after":null,"ref":"refs/heads/bump-actions-checkout","pushedAt":"2024-08-12T13:39:54.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"}},{"before":"c301a4be36adda133b436455b1f3914303c1a1dd","after":"f6c7be46e6c3d6340dfa9cfd66e0be61e83109eb","ref":"refs/heads/master","pushedAt":"2024-08-12T13:39:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Bump actions/checkout, upload-artifact, download-artifact to v4 (#545)","shortMessageHtmlLink":"Bump actions/checkout, upload-artifact, download-artifact to v4 (#545)"}},{"before":null,"after":"eadb3beecbd79bddaf1a4567497f89cf17037c69","ref":"refs/heads/bump-actions-checkout","pushedAt":"2024-08-12T12:27:08.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Bump actions/checkout, upload-artifact, download-artifact to v4","shortMessageHtmlLink":"Bump actions/checkout, upload-artifact, download-artifact to v4"}},{"before":"0771935ede8c3adc1f3f4aec210a8d88fa76d25a","after":"c301a4be36adda133b436455b1f3914303c1a1dd","ref":"refs/heads/master","pushedAt":"2024-08-12T12:12:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[Rust] Fix unsound treatment of alloc/dealloc\n\nThe spec now takes alignment into account.\n\nAlso:\n- Remove special-casing of type Layout\n- Add support for fixpoints with type parameters that carry a typeid.\n- In Rust, try to interpret compound paths as relative to the current module, if interpreting as absolute fails.","shortMessageHtmlLink":"[Rust] Fix unsound treatment of alloc/dealloc"}},{"before":"c2554e602e12b8fae8fc7c0e6fdf8c4a5ca246d3","after":"0771935ede8c3adc1f3f4aec210a8d88fa76d25a","ref":"refs/heads/master","pushedAt":"2024-08-02T09:59:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Stop conflating pointer type typeids","shortMessageHtmlLink":"Stop conflating pointer type typeids"}},{"before":"5c2987a856f9128e90a73177733e60430739e40a","after":"c2554e602e12b8fae8fc7c0e6fdf8c4a5ca246d3","ref":"refs/heads/master","pushedAt":"2024-08-01T08:22:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"close_struct: Check effective type\n\nThis breaking change fixes #540, an unsoundness. You can disable\nthis check by specifying the -fno-strict-aliasing flag.","shortMessageHtmlLink":"close_struct: Check effective type"}},{"before":"ee7547b33b241d9c496a92251981cf440b23c06f","after":"5c2987a856f9128e90a73177733e60430739e40a","ref":"refs/heads/master","pushedAt":"2024-07-31T09:45:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Enforce effective types for (u)intN_t accesses\n\nAlso, *p |-> PAT and p[PAT1..PAT2] |-> PAT3 assertions where\np is of type (u)intN_t* now assert has_type(p, &typeid((u)intN_t)) == true.\n\nThis breaking change fixes #504, an unsoundness. You can disable\neffective types checks by specifying the -fno-strict-aliasing\ncommand-line flag.","shortMessageHtmlLink":"Enforce effective types for (u)intN_t accesses"}},{"before":"3831aabf8419d3cbe4dc27541812f56c048f97f5","after":"ee7547b33b241d9c496a92251981cf440b23c06f","ref":"refs/heads/master","pushedAt":"2024-07-28T08:01:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Fix unsoundness in field_ptr_provenance_injective\n\nWas inconsistent with -assume_no_provenance which assumes\nthat all provenances are equal.","shortMessageHtmlLink":"Fix unsoundness in field_ptr_provenance_injective"}},{"before":"1d4a50d3e21e0fbf261bedda58b95d6079ebe5b2","after":"3831aabf8419d3cbe4dc27541812f56c048f97f5","ref":"refs/heads/master","pushedAt":"2024-07-21T11:44:02.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Produce shift left fact only outside fixpoint (#537)","shortMessageHtmlLink":"Produce shift left fact only outside fixpoint (#537)"}},{"before":"4bcc7b01586427ad8bc072de076f84c29b32a041","after":"1d4a50d3e21e0fbf261bedda58b95d6079ebe5b2","ref":"refs/heads/master","pushedAt":"2024-07-13T22:19:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[Rust] atomics_example.rs\n\nThis commit:\n- Starts spec'ing out AtomicUsize\n- Adds an example that uses AtomicUsize\n- Adds support for verifying programs that refer to variants of\n enums declared in extern crates (including std).\n This involved updates to how the exporter exports aggregates\n and changes in how enum variants are translated.\n- Fixes a bug in the treatment of blocks with ghost declarations\n in the Rust preprocessor.\n- Disables the strict aliasing checks when verifying Rust programs.\n- Adds options -dump_asts and -dump_asts_with_locs to the\n 'verifast' command-line tool","shortMessageHtmlLink":"[Rust] atomics_example.rs"}},{"before":"6b8c37ef767064ea19bb29873729bf1a5583cfe4","after":"4bcc7b01586427ad8bc072de076f84c29b32a041","ref":"refs/heads/master","pushedAt":"2024-07-11T22:29:26.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Busy waiting: tricky client example (Java) (#533)","shortMessageHtmlLink":"Busy waiting: tricky client example (Java) (#533)"}},{"before":"81fec2df863970df772274c54234a3593a6454af","after":"6b8c37ef767064ea19bb29873729bf1a5583cfe4","ref":"refs/heads/master","pushedAt":"2024-07-11T15:40:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Busy-waiting handoff client example","shortMessageHtmlLink":"Busy-waiting handoff client example"}},{"before":"a514a79b30bd061a243befe1a787e54c234cc16c","after":"81fec2df863970df772274c54234a3593a6454af","ref":"refs/heads/master","pushedAt":"2024-07-11T09:47:56.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Add simple aborting handoff client example (#531)","shortMessageHtmlLink":"Add simple aborting handoff client example (#531)"}},{"before":"3bcf0ecf699a4baf45fd3bb0e2d94aeb20204906","after":"a514a79b30bd061a243befe1a787e54c234cc16c","ref":"refs/heads/master","pushedAt":"2024-07-10T06:51:55.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[Rust] Remove frac_borrow_implies (#529)","shortMessageHtmlLink":"[Rust] Remove frac_borrow_implies (#529)"}},{"before":"ae02af5c25cc4e68c4102eaf8f423590b3c6790a","after":"3bcf0ecf699a4baf45fd3bb0e2d94aeb20204906","ref":"refs/heads/master","pushedAt":"2024-07-05T11:17:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[Rust] Rc","shortMessageHtmlLink":"[Rust] Rc<T>"}},{"before":"328e4c8f624617a3a7c1d75d8d9a3b192a6ff58a","after":"ae02af5c25cc4e68c4102eaf8f423590b3c6790a","ref":"refs/heads/master","pushedAt":"2024-07-05T09:44:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[Rust] RcU32 (#523)","shortMessageHtmlLink":"[Rust] RcU32 (#523)"}},{"before":"e1ea410b8618c80bbf0626f089acecb6648c2a91","after":"328e4c8f624617a3a7c1d75d8d9a3b192a6ff58a","ref":"refs/heads/master","pushedAt":"2024-06-18T09:08:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Update `is_permutation_reflexive` for general type (#526)","shortMessageHtmlLink":"Update is_permutation_reflexive
for general type (#526)"}},{"before":"a784056b87673e3aa2c84b9b2d5c62bb7f616c54","after":"e1ea410b8618c80bbf0626f089acecb6648c2a91","ref":"refs/heads/master","pushedAt":"2024-06-10T05:13:10.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Allow unnamed function parameters (#525)","shortMessageHtmlLink":"Allow unnamed function parameters (#525)"}},{"before":"de6a20ad52be739662966526d6024c47c43611a2","after":"a784056b87673e3aa2c84b9b2d5c62bb7f616c54","ref":"refs/heads/master","pushedAt":"2024-06-02T15:12:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"printf, varargs: Support arbitrary integer types\n\nBreaking change: vararg_int and vararg_uint now take the size of the\nargument as an extra argument.\n\nFixes #516","shortMessageHtmlLink":"printf, varargs: Support arbitrary integer types"}},{"before":"ed8e7bca32ebe5e8103f53d33f23194fdbfec3f9","after":"de6a20ad52be739662966526d6024c47c43611a2","ref":"refs/heads/master","pushedAt":"2024-06-02T14:59:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Switch statement default clauses","shortMessageHtmlLink":"Switch statement default clauses"}},{"before":"1a61c8bce2376af4e2a21c10318343db36551907","after":"ed8e7bca32ebe5e8103f53d33f23194fdbfec3f9","ref":"refs/heads/master","pushedAt":"2024-06-02T12:07:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Switch assertion default clauses","shortMessageHtmlLink":"Switch assertion default clauses"}},{"before":"8309e86583cd5d8066eb18776844541c667acc16","after":"1a61c8bce2376af4e2a21c10318343db36551907","ref":"refs/heads/master","pushedAt":"2024-06-02T09:58:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[C++] Deleted and Defaulted functions (#521)","shortMessageHtmlLink":"[C++] Deleted and Defaulted functions (#521)"}},{"before":"12e89029b5628189e7866a368cd54b2a4916af18","after":"8309e86583cd5d8066eb18776844541c667acc16","ref":"refs/heads/master","pushedAt":"2024-05-31T14:18:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[C++] Refine source locations (#520)","shortMessageHtmlLink":"[C++] Refine source locations (#520)"}},{"before":"69cc8653af6c98c4c8b73347813edcfce48c3282","after":"12e89029b5628189e7866a368cd54b2a4916af18","ref":"refs/heads/master","pushedAt":"2024-05-27T08:53:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[C++] Switch statement (#518)","shortMessageHtmlLink":"[C++] Switch statement (#518)"}},{"before":"c7e2c11770188f4bb4dcba2110a555394bde2c3c","after":"69cc8653af6c98c4c8b73347813edcfce48c3282","ref":"refs/heads/master","pushedAt":"2024-05-24T06:25:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"vfide: Add \"Open Recent\" menu (#515)","shortMessageHtmlLink":"vfide: Add \"Open Recent\" menu (#515)"}},{"before":"26f21bfd290b590cbca2fd0aeceeefeadaed1996","after":"c7e2c11770188f4bb4dcba2110a555394bde2c3c","ref":"refs/heads/master","pushedAt":"2024-05-23T15:25:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Fix #513","shortMessageHtmlLink":"Fix #513"}},{"before":"1f28261ed6d7026cb00f43a5406165f0bcbead95","after":"26f21bfd290b590cbca2fd0aeceeefeadaed1996","ref":"refs/heads/master","pushedAt":"2024-05-23T14:07:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Fix #511","shortMessageHtmlLink":"Fix #511"}},{"before":"35d34e5bd782ade0403c74984f5ef4f619ddad69","after":"1f28261ed6d7026cb00f43a5406165f0bcbead95","ref":"refs/heads/master","pushedAt":"2024-05-22T12:31:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[C++] Refactor ast exporter (#509)\n\nForward declarations that were introduced to resolve cyclic dependencies\r\nhave been removed and resolved.\r\n\r\n`AnnotationsStore` has been refactored to `AnnotationManager`.\r\nThis manager is stateless once all annotations have been added.\r\nThis allows to retrieve the same annotations multiple times\r\nand does not force to retrieve annotations in lexical order.\r\n\r\n`std` containers have been replaced by their `llvm` counterparts.\r\n\r\nEnables an easy way to customize source ranges of AST nodes.\r\nE.g., the source range of a function in clang refers to entire span of the function\r\ninstead of only the function's name. This can now be easily overridden in `Location.cpp`.\r\n\r\nRemoved obsolete script to install msvc.\r\n\r\nContracts for constructors are now expected before the initializer list.\r\nBefore:\r\n```\r\nstruct Foo {\r\nint i;\r\n\r\nFoo() : i(0)\r\n//@ requires true;\r\n//@ ensures this->i |-> 0;\r\n{}\r\n};\r\n```\r\nNow:\r\n```\r\nstruct Foo {\r\nint i;\r\n\r\nFoo()\r\n//@ requires true;\r\n//@ ensures this->i |-> 0;\r\n: i(0)\r\n{}\r\n};\r\n```","shortMessageHtmlLink":"[C++] Refactor ast exporter (#509)"}},{"before":"dc0974a18b865875e6da253c6474b299109ca99d","after":"35d34e5bd782ade0403c74984f5ef4f619ddad69","ref":"refs/heads/master","pushedAt":"2024-05-17T13:02:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"Fix #507","shortMessageHtmlLink":"Fix #507"}},{"before":"97701d509f4ab3c20ba6c67dd6157396976b46f0","after":"dc0974a18b865875e6da253c6474b299109ca99d","ref":"refs/heads/master","pushedAt":"2024-05-17T07:34:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"btj","name":"Bart Jacobs","path":"/btj","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1780310?s=80&v=4"},"commit":{"message":"[Rust] Generate is_Send facts","shortMessageHtmlLink":"[Rust] Generate is_Send facts"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEmCiqagA","startCursor":null,"endCursor":null}},"title":"Activity ยท verifast/verifast"}