{"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:1726771562.0","currentOid":""},"activityList":{"items":[{"before":"e7220f64a4f55e11675ec0f265247718a341efe7","after":null,"ref":"refs/heads/release-6.3.1","pushedAt":"2024-09-19T18:46:02.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":"e7220f64a4f55e11675ec0f265247718a341efe7","ref":"refs/heads/release-6.3.1","pushedAt":"2024-09-19T16:26:45.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":"Release CBMC 6.3.1\n\nThis patch release addresses build failures on Apple Silicon (via PR #8461).","shortMessageHtmlLink":"Release CBMC 6.3.1"}},{"before":"9c9b52efa28a349bb9ab9c8068794ba14f7cd96d","after":null,"ref":"refs/heads/fix-aarch64-va_list","pushedAt":"2024-09-19T16:26:24.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":"02322ae19789ea10a52861baf700242854b8cf8e","after":"9c9b52efa28a349bb9ab9c8068794ba14f7cd96d","ref":"refs/heads/fix-aarch64-va_list","pushedAt":"2024-09-19T15:34:16.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: Apple does not adhere to aarch64 ABI\n\nThe fix from #8366 must not be used on macOS as that platform still uses\n`__builtin_va_list` instead of the ARM-mandated struct.","shortMessageHtmlLink":"C library: Apple does not adhere to aarch64 ABI"}},{"before":null,"after":"02322ae19789ea10a52861baf700242854b8cf8e","ref":"refs/heads/fix-aarch64-va_list","pushedAt":"2024-09-19T12:49:29.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: Apple does not adhere to aarch64 ABI\n\nThe fix from #8366 must not be used on macOS as that platform still uses\n`__builtin_va_list` instead of the ARM-mandated struct.","shortMessageHtmlLink":"C library: Apple does not adhere to aarch64 ABI"}},{"before":"e8610a5280d28d4d206e4fa3bc8f1b30a06f6513","after":null,"ref":"refs/heads/release-6.3.0","pushedAt":"2024-09-19T09:29:17.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":"e8610a5280d28d4d206e4fa3bc8f1b30a06f6513","ref":"refs/heads/release-6.3.0","pushedAt":"2024-09-19T08:37:05.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":"Release CBMC 6.3.0\n\nThis release addresses build failures on aarch64 (64-bit ARM) platforms\n(via PR #8366) and for some CMake configurations (via PR #8435). Users\nof loop invariants with dynamic frames have two changes to their user\nexperience:\n1) Users will no longer need to give unwinding specifications for `do {\n   ... } while(0)` loops.\n2) Loop invariants that are conjunctions will be turned into more\n   fine-grained properties to ease debugging of loop invariants when\n   they aren't successfully proved.","shortMessageHtmlLink":"Release CBMC 6.3.0"}},{"before":"40a3dbbe6af4c54a186a2e8ec829935108ec7145","after":null,"ref":"refs/heads/fix-8357-va_list","pushedAt":"2024-09-19T08:12:10.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":"20e7cef3ca0b2ff8433b7b5cdef1a75a2c0e3bb5","after":"40a3dbbe6af4c54a186a2e8ec829935108ec7145","ref":"refs/heads/fix-8357-va_list","pushedAt":"2024-09-18T10:50:59.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: fix use of va_list for AARCH64\n\nThis is a fixup to \"C model library: Support ARM64 va_list types\" that\n1) only changed only a subset of the code locations that required change\n   and\n2) did so with a crude workaround.\n\nReally, we need to abide by ARM's procedure call standard for ARM64,\nwhich mandates that `va_list` be a particular struct. See\n\nhttps://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#definition-of-va-list\nand\nhttps://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#the-va-arg-macro\n\nWhile at it, also add the necessary define for Visual Studio's support\nof ARM64.\n\nFixes: #8357","shortMessageHtmlLink":"C library: fix use of va_list for AARCH64"}},{"before":"eb5466d875afacf8c8379be318986e07f89c7d38","after":null,"ref":"refs/heads/loop-invariants-conjunction-splitting","pushedAt":"2024-09-17T21:04:49.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":"b47bb51e37ec7f4d4da081aa3deb510566faea9a","after":"eb5466d875afacf8c8379be318986e07f89c7d38","ref":"refs/heads/loop-invariants-conjunction-splitting","pushedAt":"2024-09-17T18:42: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":"Contracts/DFCC: split conjunctions in loop invariants\n\nEmitting one assertion (and assumption) per conjunct simplifies\ndebugging when proving a loop invariant fails. It also appears to\nimprove performance when using Bitwuzla, taking one example from more\nthan 30 minutes down to 8 seconds. On the same example, performance\nusing Z3 was not substantially different.","shortMessageHtmlLink":"Contracts/DFCC: split conjunctions in loop invariants"}},{"before":"d4afdd2a45208fbae83b0a1aba769fa41d3a2cab","after":null,"ref":"refs/heads/contracts-remove-do-while-0","pushedAt":"2024-09-17T17:33:02.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":"0639facdd6e37dadfd48e13898ff83d727d8a38f","after":"d4afdd2a45208fbae83b0a1aba769fa41d3a2cab","ref":"refs/heads/contracts-remove-do-while-0","pushedAt":"2024-09-17T13:23:03.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":"Contracts: always remove spurious do {... } while(0) loops\n\nNone of our contracts instrumentation should spuriously get confused by\nthese pseudo-loops (suggesting to users that they need to unwind those\nloops). We already used to do this for non-DFCC code, now also apply it\nwith dynamic frames.","shortMessageHtmlLink":"Contracts: always remove spurious do {... } while(0) loops"}},{"before":null,"after":"0639facdd6e37dadfd48e13898ff83d727d8a38f","ref":"refs/heads/contracts-remove-do-while-0","pushedAt":"2024-09-17T12:58:48.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":"Contracts: always remove spurious do {... } while(0) loops\n\nNone of our contracts instrumentation should spuriously get confused by\nthese pseudo-loops (suggesting to users that they need to unwind those\nloops). We already used to do this for non-DFCC code, now also apply it\nwith dynamic frames.","shortMessageHtmlLink":"Contracts: always remove spurious do {... } while(0) loops"}},{"before":null,"after":"b47bb51e37ec7f4d4da081aa3deb510566faea9a","ref":"refs/heads/loop-invariants-conjunction-splitting","pushedAt":"2024-09-17T11:49:55.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":"Contracts/DFCC: split conjunctions in loop invariants\n\nEmitting one assertion (and assumption) per conjunct simplifies\ndebugging when proving a loop invariant fails. It also appears to\nimprove performance when using Bitwuzla, taking one example from more\nthan 30 minutes down to 8 seconds. On the same example, performance\nusing Z3 was not substantially different.","shortMessageHtmlLink":"Contracts/DFCC: split conjunctions in loop invariants"}},{"before":"f63dfa91ce7f8d4dfb6356c527895fbdcb6af2ff","after":null,"ref":"refs/heads/use-boolean_negate","pushedAt":"2024-09-13T16:34:43.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":"497b7e32263ed4a282d1e91624a6fb27b58b4b12","ref":"refs/heads/protect-value_is_zero_string","pushedAt":"2024-09-13T15:49:19.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":"Mark constant_exprt::value_is_zero_string protected\n\nThe value representation is an implementation detail. Callers should use\nmethods at a higher level of abstraction.","shortMessageHtmlLink":"Mark constant_exprt::value_is_zero_string protected"}},{"before":"eb098bb6c4be1044da353efc65810bb4c201d717","after":"8ca6411774e5afae5134bc3cf06a98f3db266604","ref":"refs/heads/no-make_and","pushedAt":"2024-09-13T15:30:59.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":"Deprecate make_and in favour of conjunction(expr, expr)\n\n`make_and` does not necessarily produce an `and_exprt`, so its name is\nmisleading. We already have `conjunction(exprt::operandst)`, and will\nnow have a variant thereof that takes exactly two operands.","shortMessageHtmlLink":"Deprecate make_and in favour of conjunction(expr, expr)"}},{"before":"9f9f6c0b1388714c914d64d1c86658bc84746e98","after":"f63dfa91ce7f8d4dfb6356c527895fbdcb6af2ff","ref":"refs/heads/use-boolean_negate","pushedAt":"2024-09-13T15:27: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":"Use boolean_negate for immediate simplification\n\nWhen the operand can be a Boolean constant we can don't need to wait for\nsimplify_exprt to clean up the avoidable not_exprt.","shortMessageHtmlLink":"Use boolean_negate for immediate simplification"}},{"before":null,"after":"5eea045dd8b26422a7ddc5895b014fa7ff0414d9","ref":"refs/heads/fix-8443-attributes","pushedAt":"2024-09-13T15:25:34.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 processing of alignment and packing attributes\n\nPacking needs to be evaluated as part of the definition of the type\nwhile alignment applies also when using a type. The position of the\nattribute also requires extra care as some positions are accepted by GCC\n(and warned about by Clang) while actually being ignored.\n\nFixes: #8443","shortMessageHtmlLink":"C front-end: fix processing of alignment and packing attributes"}},{"before":"92d737647aa5356bab87fee6fb43b3009e0d4901","after":"9f9f6c0b1388714c914d64d1c86658bc84746e98","ref":"refs/heads/use-boolean_negate","pushedAt":"2024-09-13T12:21:08.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":"Deprecate make_and in favour of conjunction(expr, expr)\n\n`make_and` does not necessarily produce an `and_exprt`, so its name is\nmisleading. We already have `conjunction(exprt::operandst)`, and will\nnow have a variant thereof that takes exactly two operands.","shortMessageHtmlLink":"Deprecate make_and in favour of conjunction(expr, expr)"}},{"before":"1aa2d83ad03b59dda40e17bbfec04be9e1014c00","after":null,"ref":"refs/heads/move-make_with_expr","pushedAt":"2024-09-13T12:13:21.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":"24abb5e833dc1e922e8a07e211ac24e73410e999","after":"92d737647aa5356bab87fee6fb43b3009e0d4901","ref":"refs/heads/use-boolean_negate","pushedAt":"2024-09-13T10:02:32.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":"Deprecate make_and in favour of conjunction(expr, expr)\n\n`make_and` does not necessarily produce an `and_exprt`, so its name is\nmisleading. We already have `conjunction(exprt::operandst)`, and will\nnow have a variant thereof that takes exactly two operands.","shortMessageHtmlLink":"Deprecate make_and in favour of conjunction(expr, expr)"}},{"before":"63701a71af187f675108f92b9c4ac7c06059ea7a","after":"1aa2d83ad03b59dda40e17bbfec04be9e1014c00","ref":"refs/heads/move-make_with_expr","pushedAt":"2024-09-13T09:56:41.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 make_with_expr to update_exprt\n\nThis will eventually remove one of the functions from the expr_util\ntranslation unit, which is supposed to be deprecated.","shortMessageHtmlLink":"Move make_with_expr to update_exprt"}},{"before":"7b47e9f7ba88870c5b100558f56ae87adb004844","after":null,"ref":"refs/heads/move-is_null_pointer","pushedAt":"2024-09-13T09:51:25.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":"3fef02a35d79b12a64561abbbb4b7c44b1fdca7f","after":null,"ref":"refs/heads/lazy_goto_model-no-dynamic_cast","pushedAt":"2024-09-13T09:49: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":"68c39bd9c3c644848850396426052002bac59c2a","after":null,"ref":"refs/heads/fix-missing-locs","pushedAt":"2024-09-11T08:23: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":"447e986983562bfe1fa4570ec1b6d71e5aafc78d","after":"132fe24622b04066accc32b6b6c963dc7067f802","ref":"refs/heads/no-renamedt","pushedAt":"2024-09-10T14:59: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":"Remove renamedt from symex_targett interface\n\nWe did not consistently use it, and the three methods that did so can\neasily be adjusted to match the remaining ones in directly taking\n`exprt` instead.","shortMessageHtmlLink":"Remove renamedt from symex_targett interface"}},{"before":"42b70b26c470c700588ce6bffda408a8d3df6189","after":"7b47e9f7ba88870c5b100558f56ae87adb004844","ref":"refs/heads/move-is_null_pointer","pushedAt":"2024-09-10T14:56:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tautschnig","name":"Michael Tautschnig","path":"/tautschnig","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1144736?s=80&v=4"},"commit":{"message":"is_null_pointer: remove code path that is no longer necessary\n\nIt seems all front-ends have been updated.","shortMessageHtmlLink":"is_null_pointer: remove code path that is no longer necessary"}},{"before":"f2a0d98e25746538f25128726647501405e7b80f","after":"42b70b26c470c700588ce6bffda408a8d3df6189","ref":"refs/heads/move-is_null_pointer","pushedAt":"2024-09-10T14:53: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 is_null_pointer to constant_exprt\n\nRemoves one of the functions from the expr_util translation unit that is\nsupposed to be deprecated.","shortMessageHtmlLink":"Move is_null_pointer to constant_exprt"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xOVQxODo0NjowMi4wMDAwMDBazwAAAAS7Nl9G","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xOVQxODo0NjowMi4wMDAwMDBazwAAAAS7Nl9G","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xMFQxNDo1MzoxOS4wMDAwMDBazwAAAASyMdrq"}},"title":"Activity · tautschnig/cbmc"}