{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":52358391,"defaultBranch":"develop","name":"cbmc","ownerLogin":"tautschnig","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2016-02-23T12:48:00.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1144736?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1717407177.0","currentOid":""},"activityList":{"items":[{"before":"fc31dfcef4d6698817198121d5b7a1a630456e7f","after":null,"ref":"refs/heads/bugfixes/c++-attributes-tag-less","pushedAt":"2024-06-03T09:32:57.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"16b9b9085789838427bb62e555a442a3c53ef7b6","after":null,"ref":"refs/heads/bugfixes/c++-decl-code","pushedAt":"2024-05-16T14:38:46.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"7a432e71f8a67254169cbe1a1875f66ce7c264dd","after":null,"ref":"refs/heads/bugfixes/c++-alignas","pushedAt":"2024-05-13T19:10:16.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"4bd13f21404412b9cf272d01c5a984038d724eeb","after":null,"ref":"refs/heads/bugfixes/c++-nodiscard","pushedAt":"2024-05-11T17:48:28.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"ac4bb2efe1a01d582bd9c4c918f0a4992fd03ca8","after":null,"ref":"refs/heads/bugfixes/c++-using","pushedAt":"2024-05-11T15:29:40.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":null,"after":"bc0ce46901229e16e77ef257c9b67fc95f3cc6e5","ref":"refs/heads/bugfixes/c++-shift-vs-template","pushedAt":"2024-05-11T14:34:04.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: fix parsing of >> as closing template args\n\nWe also need to pop one token, not just replace the existing ones.","shortMessageHtmlLink":"C++ front-end: fix parsing of >> as closing template args"}},{"before":null,"after":"16b9b9085789838427bb62e555a442a3c53ef7b6","ref":"refs/heads/bugfixes/c++-decl-code","pushedAt":"2024-05-11T14:32:52.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: not all declarators are code-typed\n\nThe example included as regression test has a bool instead.","shortMessageHtmlLink":"C++ front-end: not all declarators are code-typed"}},{"before":null,"after":"fc31dfcef4d6698817198121d5b7a1a630456e7f","ref":"refs/heads/bugfixes/c++-attributes-tag-less","pushedAt":"2024-05-11T14:30:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: support attributes with tag-less structs\n\nSeen in GCC's STL.","shortMessageHtmlLink":"C++ front-end: support attributes with tag-less structs"}},{"before":null,"after":"7a432e71f8a67254169cbe1a1875f66ce7c264dd","ref":"refs/heads/bugfixes/c++-alignas","pushedAt":"2024-05-11T14:29:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: fix parentheses matching for alignas parsing\n\nWe had parentheses consumed by rCommaExpression while still expecting to\nfind one after this rule executed.","shortMessageHtmlLink":"C++ front-end: fix parentheses matching for alignas parsing"}},{"before":"be31f38ff385c2ebde7d0f371f589c7cc533c400","after":"4bd13f21404412b9cf272d01c5a984038d724eeb","ref":"refs/heads/bugfixes/c++-nodiscard","pushedAt":"2024-05-11T14:28:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: support [[__nodiscard__]] and [[nodiscard]]\n\nRequired to parse cassert (which in turn includes stdlib.h) on macOS in\nC++11 mode.","shortMessageHtmlLink":"C++ front-end: support [[__nodiscard__]] and [[nodiscard]]"}},{"before":null,"after":"be31f38ff385c2ebde7d0f371f589c7cc533c400","ref":"refs/heads/bugfixes/c++-nodiscard","pushedAt":"2024-05-11T14:19:49.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: support [[__nodiscard__]] and [[nodiscard]]\n\nRequired to parse cassert (which in turn includes stdlib.h) on macOS in\nC++11 mode.","shortMessageHtmlLink":"C++ front-end: support [[__nodiscard__]] and [[nodiscard]]"}},{"before":null,"after":"ac4bb2efe1a01d582bd9c4c918f0a4992fd03ca8","ref":"refs/heads/bugfixes/c++-using","pushedAt":"2024-05-11T14:15:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: permit GCC attributes in using declarations\n\nLLVM's standard library uses these in type_traits.","shortMessageHtmlLink":"C++ front-end: permit GCC attributes in using declarations"}},{"before":"bb79589eae48663379baebbabcd019e2e2b75354","after":"04bcc9125e0b227aa91b7bd8819d49aafddfd228","ref":"refs/heads/bugfixes/cpp-constexpr","pushedAt":"2024-05-11T14:13:31.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: parse template parameter packs\n\nAttach the \"ellipsis\" information to the declarator and not to the type.","shortMessageHtmlLink":"C++ front-end: parse template parameter packs"}},{"before":"98d09fb042deee5d1b3738ffe62124fa5420a20c","after":null,"ref":"refs/heads/features/tolower","pushedAt":"2024-05-10T19:31:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"f4916a1a68e13edcf78605371935f57eff5b52cc","after":"bb79589eae48663379baebbabcd019e2e2b75354","ref":"refs/heads/bugfixes/cpp-constexpr","pushedAt":"2024-05-10T15:03:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: More work on brace init","shortMessageHtmlLink":"C++ front-end: More work on brace init"}},{"before":"4622ed5e1175cf04f1931dcb17f76d5762a1af0f","after":"98d09fb042deee5d1b3738ffe62124fa5420a20c","ref":"refs/heads/features/tolower","pushedAt":"2024-05-10T13:03:06.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C library: add __to{lower,upper} as alternative names for {tolower,toupper}\n\nmacOS eventually calls a function called `__tolower` (`__toupper`).\nRename our previous implementation to `__CPROVER_tolower`\n(`__CPROVER_toupper`) and make both `tolower` (`toupper`) and\n`__tolower` (`__toupper`)  use this. Also enable their regression tests.","shortMessageHtmlLink":"C library: add __to{lower,upper} as alternative names for {tolower,to…"}},{"before":"b56a95b3e92d4a8e3dbbb8afb5e0ba133d8ad4e9","after":"4622ed5e1175cf04f1931dcb17f76d5762a1af0f","ref":"refs/heads/features/tolower","pushedAt":"2024-05-10T13:00:26.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C library: add __to{lower,upper} as alternative names for {tolower,toupper}\n\nmacOS eventually calls a function called `__tolower` (`__toupper`).\nRename our previous implementation to `__CPROVER_tolower`\n(`__CPROVER_toupper`) and make both `tolower` (`toupper`) and\n`__tolower` (`__toupper`)  use this. Also enable their regression tests.","shortMessageHtmlLink":"C library: add __to{lower,upper} as alternative names for {tolower,to…"}},{"before":null,"after":"b56a95b3e92d4a8e3dbbb8afb5e0ba133d8ad4e9","ref":"refs/heads/features/tolower","pushedAt":"2024-05-10T12:56:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C library: add __tolower as alternative name for tolower\n\nmacOS eventually calls a function called `__tolower`. Rename our\nprevious implementation to `__CPROVER_tolower` and make both `tolower`\nand `__tolower` use this. Also enable the regression test of it.","shortMessageHtmlLink":"C library: add __tolower as alternative name for tolower"}},{"before":"790e44f6bca2979427b99155361dab1869e9deef","after":"2c13d8260570dd705e67b459903bd0765b1464dc","ref":"refs/heads/bugfixes/uif-in-quantifier","pushedAt":"2024-05-10T12:56:11.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Move __CPROVER_uninterpreted_* conversion to C type checker\n\nWe already had type checking of mathematical_function types to support\nlambda expressions. Special-case symbols with name\n`__CPROVER_uninterpreted_*` will now also produce these types. GOTO\nconversion will no longer give specific treatment to function calls with\nsymbol name `__CPROVER_uninterpreted_*`.","shortMessageHtmlLink":"Move __CPROVER_uninterpreted_* conversion to C type checker"}},{"before":null,"after":"790e44f6bca2979427b99155361dab1869e9deef","ref":"refs/heads/bugfixes/uif-in-quantifier","pushedAt":"2024-05-09T19:26:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Move __CPROVER_uninterpreted_* conversion to C type checker\n\nWe already had type checking of mathematical_function types to support\nlambda expressions. Special-case symbols with name\n`__CPROVER_uninterpreted_*` will now also produce these types. GOTO\nconversion will no longer give specific treatment to function calls with\nsymbol name `__CPROVER_uninterpreted_*`.","shortMessageHtmlLink":"Move __CPROVER_uninterpreted_* conversion to C type checker"}},{"before":"8a0782bbdd9d7bd752a5f7345d6693d8cf90afb5","after":null,"ref":"refs/heads/cleanup/no-follow-solvers","pushedAt":"2024-05-09T18:45:40.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"74cfc8b19b7b5f371cbcb0052000c8b8d9f7bbf9","after":null,"ref":"refs/heads/cleanup/no-follow-jbmc","pushedAt":"2024-05-09T18:45:20.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"}},{"before":"f755e0030fb1e0822022f75bdfbdbda0625b21d4","after":"d05703f808d3111a73106d8a0e90441fe743415d","ref":"refs/heads/bugfixes/7706-va-start","pushedAt":"2024-05-08T11:34:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Variadic args/va_arg: handle unexpected va_list types\n\nOur regression test has `void*` lists when we'd expected `void**`. This,\nhowever, went unnoticed as we only tried to access the first element.\nAttempts to access the second element would have been misaligned, and\nfailed an invariant as of 35cc503 (we don't handle pointer arithmetic\nover void pointers in the back-end anymore).\n\nWe now make sure that we always increment by size-of-`void*`.\n\nFixes: #7706","shortMessageHtmlLink":"Variadic args/va_arg: handle unexpected va_list types"}},{"before":"a6df679031c573b59e92dfbfb3d00da83ee2b1cf","after":"3dad36dcea17f77a1848296153c9a6d359c1ef06","ref":"refs/heads/feature/bits-bytes","pushedAt":"2024-05-08T11:32:13.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Introduce bitst and bytest to avoid bit/byte mix-up\n\nUse mp_integers with a unit to clarify when an mp_integer holds a number\nof bits or a number of bytes. This makes sure that type-inconsistent\ncomparisons as fixed in #7411 result in compile-time errors.","shortMessageHtmlLink":"Introduce bitst and bytest to avoid bit/byte mix-up"}},{"before":"79490c5c8e7d7df73cea87b87d1c3482eeda978f","after":"a6df679031c573b59e92dfbfb3d00da83ee2b1cf","ref":"refs/heads/feature/bits-bytes","pushedAt":"2024-05-08T11:31:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Introduce bitst and bytest to avoid bit/byte mix-up\n\nUse mp_integers with a unit to clarify when an mp_integer holds a number\nof bits or a number of bytes. This makes sure that type-inconsistent\ncomparisons as fixed in #7411 result in compile-time errors.","shortMessageHtmlLink":"Introduce bitst and bytest to avoid bit/byte mix-up"}},{"before":"f30da5c6deaba38c7a5be14eaf6f461a6f566b04","after":"7e712c2abfbf19381f24cf826e406353ea8f6d6e","ref":"refs/heads/rounding-mode-symbol","pushedAt":"2024-05-08T11:22:19.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Move rounding_mode_identifier() to configt\n\nThis removes a goto-programs dependency from linking/, which is all\nabout symbol tables, not goto programs.","shortMessageHtmlLink":"Move rounding_mode_identifier() to configt"}},{"before":"851f23f76dd16761a932e6a28ee0c8165e7e5bdb","after":"f4916a1a68e13edcf78605371935f57eff5b52cc","ref":"refs/heads/bugfixes/cpp-constexpr","pushedAt":"2024-05-07T10:44:53.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"Revert \"DEBUG\"\n\nThis reverts commit 4c299cc716f9e0bf639411296f1ee5f2c5d96300.","shortMessageHtmlLink":"Revert \"DEBUG\""}},{"before":"3a22380f4f5f85bf679b202b2d5d2a6fa2dae6fb","after":"851f23f76dd16761a932e6a28ee0c8165e7e5bdb","ref":"refs/heads/bugfixes/cpp-constexpr","pushedAt":"2024-05-07T07:55:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: not all declarators are code-typed\n\nThe example included as regression test has a bool instead.","shortMessageHtmlLink":"C++ front-end: not all declarators are code-typed"}},{"before":"2d444a5d9fb486cd3a2c114d35ed7e3565a67dde","after":"3a22380f4f5f85bf679b202b2d5d2a6fa2dae6fb","ref":"refs/heads/bugfixes/cpp-constexpr","pushedAt":"2024-05-07T03:17:46.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: WIP (needs test)","shortMessageHtmlLink":"C++ front-end: WIP (needs test)"}},{"before":null,"after":"2d444a5d9fb486cd3a2c114d35ed7e3565a67dde","ref":"refs/heads/bugfixes/cpp-constexpr","pushedAt":"2024-05-07T01:21:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"C++ front-end: WIP (needs test)","shortMessageHtmlLink":"C++ front-end: WIP (needs test)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEWsA7BgA","startCursor":null,"endCursor":null}},"title":"Activity · tautschnig/cbmc"}