{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":24187206,"defaultBranch":"master","name":"CompCert","ownerLogin":"AbsInt","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-09-18T12:27:33.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/8820208?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1725377271.0","currentOid":""},"activityList":{"items":[{"before":"fd48dc8680286ab91ad79c1c8b1ca9ec2f516e64","after":"32dba0760c003cc5886059d937fa065b3daee7dd","ref":"refs/heads/master","pushedAt":"2024-09-08T16:31:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Add missing temp_env parameter to documentation of Clight.eval_expr (#523)","shortMessageHtmlLink":"Add missing temp_env parameter to documentation of Clight.eval_expr (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2511061696\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/523\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/523/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/523\">#…</a>"}},{"before":"3e18c8a47951a32c54e37eafeaf537e6c9ebe396","after":"4fd5338cb427256daf9997b6814ae927b3c7e5f7","ref":"refs/heads/backslash-newline","pushedAt":"2024-09-06T15:01:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Also check for trigraph-backslash-newline\n\nThere's a trigraph for backslash `??/`, and the sequence `??/`-newline\nin a preprocessed file is highly suspicious.","shortMessageHtmlLink":"Also check for trigraph-backslash-newline"}},{"before":"18ecb24cea319ac2b1ccd4743dd633d6a01cf81a","after":"fd48dc8680286ab91ad79c1c8b1ca9ec2f516e64","ref":"refs/heads/master","pushedAt":"2024-09-04T17:07:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Return `Btop` for undefined pointer comparisons in non-strict mode\n\nComparing pointers from different blocks with `< <= > >=`\nis undefined behavior in CompCert and in ISO C.  So, it is sound to\nanalyze such comparisons as `Bnone`.\n\nHowever, these comparisons occur in real code, and produce\nstatically-unpredictable Boolean results, so it is safer and more\nconsistent with other parts of the value analysis to return `Btop` in\nnon-strict mode.\n\nCurrently, this should make no difference to the generated code, since\nCompCert does not optimize based on the absence of undefined\ncomparisons.","shortMessageHtmlLink":"Return <code>Btop</code> for undefined pointer comparisons in non-strict mode"}},{"before":"7e0fdb927d11ab2526debe978bb8fdd2eb4dc23c","after":"496ae6dcc17fc7a217abf9ddb9cb34fcbecc8683","ref":"refs/heads/value-analysis-mul-div","pushedAt":"2024-09-04T09:37:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Improve value analysis for `mods`\n\nA signed interval can be inferred for the result if the second\nargument is known.","shortMessageHtmlLink":"Improve value analysis for <code>mods</code>"}},{"before":null,"after":"7e0fdb927d11ab2526debe978bb8fdd2eb4dc23c","ref":"refs/heads/value-analysis-mul-div","pushedAt":"2024-09-03T15:27:51.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Improve value analysis for `divu` and `divs`\n\nSome unsigned or signed intervals can be inferred for the result.","shortMessageHtmlLink":"Improve value analysis for <code>divu</code> and <code>divs</code>"}},{"before":"82ef8858b394718e21a6a36793bc6a796cdd1c3e","after":"18ecb24cea319ac2b1ccd4743dd633d6a01cf81a","ref":"refs/heads/master","pushedAt":"2024-09-02T15:21:08.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Value analysis: reduce `Uns p 0` to `IU Int.zero`\n\nA zero-bit unsigned integer is either Vint Int.zero or Vundef.","shortMessageHtmlLink":"Value analysis: reduce <code>Uns p 0</code> to <code>IU Int.zero</code>"}},{"before":"facbe118dca12cb6f72a7b6e877ff38f35a561d1","after":"82ef8858b394718e21a6a36793bc6a796cdd1c3e","ref":"refs/heads/master","pushedAt":"2024-09-02T07:34:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Mark stack as non-executable in binaries produced by ccomp\n\nOn Linux and BSD, add \"stack not executable\" annotations to every asm file\nproduced by ccomp or hand-written in the runtime support library.\n\nLeft for future work: adding the annotation to runtime/powerpc*/*.s .\n(These files are not preprocessed, and must remain compatible with Diab.)","shortMessageHtmlLink":"Mark stack as non-executable in binaries produced by ccomp"}},{"before":"bd3813f3f648994c689b416871e9aa0fe6d1be08","after":"facbe118dca12cb6f72a7b6e877ff38f35a561d1","ref":"refs/heads/master","pushedAt":"2024-08-30T14:20:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Support Coq 8.19.2","shortMessageHtmlLink":"Support Coq 8.19.2"}},{"before":"67cdb366d472fd52c0ee87698ebc4e703b0f26c2","after":"3e18c8a47951a32c54e37eafeaf537e6c9ebe396","ref":"refs/heads/backslash-newline","pushedAt":"2024-08-28T12:10:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Leave trigraphs in peace","shortMessageHtmlLink":"Leave trigraphs in peace"}},{"before":null,"after":"67cdb366d472fd52c0ee87698ebc4e703b0f26c2","ref":"refs/heads/backslash-newline","pushedAt":"2024-08-28T07:32:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Check that preprocessed source do not contain backslash-newline nor trigraphs\n\nThis is normally ensured by the preprocessor, as translation phases 1 and 2\n(ISO C99, 5.1.1.2).  However, these sequences could occur in\nhand-written .i files and confuse the CompCert lexer.","shortMessageHtmlLink":"Check that preprocessed source do not contain backslash-newline nor t…"}},{"before":"f3f1dc29e9f527acebf0f71afca1a964bba1f5cb","after":null,"ref":"refs/heads/value-analysis-IU","pushedAt":"2024-08-26T14:21:28.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"4063933d8ff1af15b187997800771aa3705ed8e2","after":null,"ref":"refs/heads/xor-cmp","pushedAt":"2024-08-26T14:21:16.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"7c87292df2a780126ff77b5ee5656bf56e20ad95","after":"bd3813f3f648994c689b416871e9aa0fe6d1be08","ref":"refs/heads/master","pushedAt":"2024-08-26T14:18:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"CombineOp: optimize `(x ^ n) != 0` into `x != n`\n\nLikewise for `(x ^ n) == 0` that becomes `x == n`.\n\nDo this only when we're sure it results in smaller code:\n\n- On RISC-V, the optimization is useless, as there is no conditional\n  branch instruction for != n and == n conditions, just for != 0 and == 0.\n\n- On ARM, AArch64, PowerPC: we limit the optimization to values of n\n  that are small enough to not need extra instructions to load the\n  immediate n in a register.","shortMessageHtmlLink":"CombineOp: optimize <code>(x ^ n) != 0</code> into <code>x != n</code>"}},{"before":"d351f4b5ca1524ded884b22fa4fcb1e4b7a2f1d1","after":"7c87292df2a780126ff77b5ee5656bf56e20ad95","ref":"refs/heads/master","pushedAt":"2024-08-25T07:47:02.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"m-schmidt","name":"Michael Schmidt","path":"/m-schmidt","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1093186?s=80&v=4"},"commit":{"message":"Merge pull request #521 from ebresafegaga/patch-1\n\nFix typo in the documentation of the `Stacking` pass","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2484173685\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/521\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/521/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/521\">#521</a> from ebresafegaga/patch-1"}},{"before":"1031c65ac836d53b01a1ec150481f2f70b1af5a7","after":"4063933d8ff1af15b187997800771aa3705ed8e2","ref":"refs/heads/xor-cmp","pushedAt":"2024-08-22T15:35:44.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"CombineOp: limit optimization of `(x ^ n) != 0` to profitable cases\n\nRISC-V: turn it off, since it brings no improvement in code size\nARM, AArch64, PowerPC: limit it to values of n small enough to not\nneed extra instructions to load the immediate n in a register.","shortMessageHtmlLink":"CombineOp: limit optimization of <code>(x ^ n) != 0</code> to profitable cases"}},{"before":"84fb063b61b81ebe4d8bfaeecb73b2890469fa13","after":null,"ref":"refs/heads/size_stmt_heuristic","pushedAt":"2024-08-22T08:20:39.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"d6503ff2e352f9e8af91ced1735d82e95e47d8ed","after":null,"ref":"refs/heads/if-conversion-more-cautious","pushedAt":"2024-08-22T08:20:16.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"af83e9a907756dc62efdd938f784356d1b528c9d","after":"d351f4b5ca1524ded884b22fa4fcb1e4b7a2f1d1","ref":"refs/heads/master","pushedAt":"2024-08-22T08:01:48.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Merge pull request #520 from AbsInt/value-analysis-IU\n\nMore precise value analysis for \"known integer or Vundef\" results","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2477305487\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/520\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/520/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/520\">#520</a> from AbsInt/value-analysis-IU"}},{"before":"8ce7997ed23814456f976ae2d3f918775fb5d8e1","after":"af83e9a907756dc62efdd938f784356d1b528c9d","ref":"refs/heads/master","pushedAt":"2024-08-22T07:54:40.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Selection: refined heuristic for if-conversion\n\nTurn if-conversion off in some cases where it would prevent later\noptimization of conditional branches in the continuation of the `if`.","shortMessageHtmlLink":"Selection: refined heuristic for if-conversion"}},{"before":"0ffc5167bbf259eced5230eb1ff343c42d349a00","after":"8ce7997ed23814456f976ae2d3f918775fb5d8e1","ref":"refs/heads/master","pushedAt":"2024-08-22T07:51:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Bound the recursion depth of size_stmt (#519)\n\nLimit recursive calls on if-then-else statements to avoid quadratic behaviors.\r\n\r\nAlso: put a fixed upper limit on the return value of size_stmt, since\r\nlarge values of the size are meaningless and make the `more_likely` criterion\r\nunstable.","shortMessageHtmlLink":"Bound the recursion depth of size_stmt (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2472683857\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/519\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/519/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/519\">#519</a>)"}},{"before":null,"after":"8dc666d6d0d67f0fefbfd23aa39719fa2306ecae","ref":"refs/heads/non-executable-stack","pushedAt":"2024-08-21T07:59:34.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Mark stack as non-executable in binaries produced by ccomp\n\nOn Linux and BSD, add \"stack not executable\" annotations to every asm file\nproduced by ccomp or hand-written in the runtime support library.","shortMessageHtmlLink":"Mark stack as non-executable in binaries produced by ccomp"}},{"before":null,"after":"f3f1dc29e9f527acebf0f71afca1a964bba1f5cb","ref":"refs/heads/value-analysis-IU","pushedAt":"2024-08-21T07:20:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Constant propagation: optimize \"known integer or Vundef\" results\n\nResults that analyze to `IU n` are turned into\n`load-integer-immediate(n)` operations.\n\nThis is semantically safe, and enables compile-time evaluation of some\npointer comparisons (e.g. `&x == &x` where `x` is a global variable or\na stack-allocated variable).","shortMessageHtmlLink":"Constant propagation: optimize \"known integer or Vundef\" results"}},{"before":"c4c9153d72a574a2aa0857f65439975f74d56836","after":null,"ref":"refs/heads/ci-golf","pushedAt":"2024-08-21T07:09:41.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"406ae8bb2508655fc0a2b79e966e31afd9f92115","after":"0ffc5167bbf259eced5230eb1ff343c42d349a00","ref":"refs/heads/master","pushedAt":"2024-08-20T17:01:22.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"GHA CI: use qemu-user from backports\n\nThis solves the PPC testing issue.\nThe ARM testing issue is solved by the updated test suite.","shortMessageHtmlLink":"GHA CI: use qemu-user from backports"}},{"before":"013e235e20d3e0297fb450a84a2f8cccbd39002f","after":"c4c9153d72a574a2aa0857f65439975f74d56836","ref":"refs/heads/ci-golf","pushedAt":"2024-08-20T16:44:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Reactivate ARM testing, should be OK now","shortMessageHtmlLink":"Reactivate ARM testing, should be OK now"}},{"before":"77accaa7ecb53252c8e4914a1acdcde1be6558c4","after":"013e235e20d3e0297fb450a84a2f8cccbd39002f","ref":"refs/heads/ci-golf","pushedAt":"2024-08-20T09:04:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"ARM is still failing, let's try PPC","shortMessageHtmlLink":"ARM is still failing, let's try PPC"}},{"before":"4be6113686e0e8812b2d7d0979e6b70b04a09f8a","after":"77accaa7ecb53252c8e4914a1acdcde1be6558c4","ref":"refs/heads/ci-golf","pushedAt":"2024-08-20T08:54:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Re-activate ARM and PPC testing","shortMessageHtmlLink":"Re-activate ARM and PPC testing"}},{"before":"f57fcf504d5a02524c0305f950449c121eb67086","after":"4be6113686e0e8812b2d7d0979e6b70b04a09f8a","ref":"refs/heads/ci-golf","pushedAt":"2024-08-20T08:41:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Wrong backport repo, try again","shortMessageHtmlLink":"Wrong backport repo, try again"}},{"before":"de631f5469fb496c47536a9412b7530f72032e22","after":"f57fcf504d5a02524c0305f950449c121eb67086","ref":"refs/heads/ci-golf","pushedAt":"2024-08-20T08:34:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Use qemu-user from backports, more recent","shortMessageHtmlLink":"Use qemu-user from backports, more recent"}},{"before":"38148035c31f32311735388d566288bec1a48883","after":null,"ref":"refs/heads/Oselimm","pushedAt":"2024-08-19T14:36:00.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEsC-QAgA","startCursor":null,"endCursor":null}},"title":"Activity · AbsInt/CompCert"}