{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":31487486,"defaultBranch":"main","name":"seahorn","ownerLogin":"seahorn","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-03-01T05:08:17.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11098044?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1690305154.0","currentOid":""},"activityList":{"items":[{"before":"dc16449a40ce8200cbccce30c12834c7a3051a5e","after":"79a7cf212f0123bd3c21fa009997fe32ae5c1aba","ref":"refs/heads/dev14","pushedAt":"2024-05-23T02:27:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"fix: bug #558\n\nCommand `smc` was registered twice in the argparse in sea script.\nOnce as command for SimpleMemoryChecker, and another as a compound\ncommand that runs SimpleMemoryChecker as part of the pipeline.\n\nBefore python3.11, the new command was silently overriding the old.\nAt python3.11, argparse module complains about the conflict.\n\nRenamed smc internal command to `smc-check`, and left `smc` as the\nname for the compound command.","shortMessageHtmlLink":"fix: bug <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2311665291\" data-permission-text=\"Title is private\" data-url=\"https://github.com/seahorn/seahorn/issues/558\" data-hovercard-type=\"issue\" data-hovercard-url=\"/seahorn/seahorn/issues/558/hovercard\" href=\"https://github.com/seahorn/seahorn/issues/558\">#558</a>"}},{"before":"2bab7831960766a0a16f149adcdce55f0651eb8f","after":"36a30812ba8a2921802a648ca171703c98a69a1e","ref":"refs/heads/main","pushedAt":"2024-04-19T19:46:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"refactor: clam changes","shortMessageHtmlLink":"refactor: clam changes"}},{"before":"6855070c34a86d47ffd51dbba63cae4c33ed1c06","after":"dc16449a40ce8200cbccce30c12834c7a3051a5e","ref":"refs/heads/dev14","pushedAt":"2024-04-19T19:26:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"refactor: clam changes","shortMessageHtmlLink":"refactor: clam changes"}},{"before":"43da6e71e60e563ff3f30fbac00022e5cb00bc43","after":"6855070c34a86d47ffd51dbba63cae4c33ed1c06","ref":"refs/heads/dev14","pushedAt":"2024-04-05T18:25:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"feat: ignore compile commands file\n\nadd compile_commands.json file to .gitignore to make git ignore this\nfile when reviewing changes\n\nSigned-off-by: Niv Sulimany <sulimany.niv@campus.technion.ac.il>","shortMessageHtmlLink":"feat: ignore compile commands file"}},{"before":"d0ab0acb1850ae09337addf5ca74debd836081c3","after":"43da6e71e60e563ff3f30fbac00022e5cb00bc43","ref":"refs/heads/dev14","pushedAt":"2024-03-26T16:42:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"feat(opsem): add smax smin intrinsic handlers in opsem","shortMessageHtmlLink":"feat(opsem): add smax smin intrinsic handlers in opsem"}},{"before":"a9924ba37ad0beed40ca9d603b7e574ad6a8b494","after":"d0ab0acb1850ae09337addf5ca74debd836081c3","ref":"refs/heads/dev14","pushedAt":"2024-02-27T18:24:39.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(opsem): only consider ptr address for equality\n\nIn https://github.com/seahorn/seahorn/commit/2eb1ddb2b014bed0c710a588c9aa23f54e1a1fd6 we added consideration for allocation size in equality predicate. This does not match behaviour of memset operation that does not touch metadata part of a pointer stored in memory.\nInstead of now requiring such operations to affect shadow memory, we retrograde to using address to compare pointers.\nThis is also compatible with how ISO C compares with NULL pointers (address == 0).\n\nFurther, this opens up a question of how to model pointer provenance in general. Currently a malloc does not reuse allocations/addresses so <base,offset,size> can stand for provenance. If we introduce re-allocation then this tuple will not suffice. However, that problem is out of scope.","shortMessageHtmlLink":"fix(opsem): only consider ptr address for equality"}},{"before":"c10fc9239dc314bf60f09a56638c01aa3e511f0d","after":"a9924ba37ad0beed40ca9d603b7e574ad6a8b494","ref":"refs/heads/dev14","pushedAt":"2024-02-12T22:51:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"feat(opsem): support umin and umax intrinsics","shortMessageHtmlLink":"feat(opsem): support umin and umax intrinsics"}},{"before":"8425d467934972a4823d7647beb76039e80459ca","after":"c10fc9239dc314bf60f09a56638c01aa3e511f0d","ref":"refs/heads/dev14","pushedAt":"2024-02-01T18:58:19.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix: clang formatting","shortMessageHtmlLink":"fix: clang formatting"}},{"before":"8545c294f2d2f0ffd3cf6e7e6048b671de4e6b9d","after":"8425d467934972a4823d7647beb76039e80459ca","ref":"refs/heads/dev14","pushedAt":"2023-10-24T14:43:55.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"feat(opsem): split simplify flag for mem and non-mem exprs\n\nWe always want to simplify isDeref and memcpy transfer symbolic expressions.\nWe want to sometimes simplify memory expressions.\nThus, splitting these decisions into two flags with the original flag signifying memory writes.","shortMessageHtmlLink":"feat(opsem): split simplify flag for mem and non-mem exprs"}},{"before":"561f54f9458e9b8fdbbfd8b89e68b1992f14d26c","after":"8545c294f2d2f0ffd3cf6e7e6048b671de4e6b9d","ref":"refs/heads/dev14","pushedAt":"2023-10-22T20:39:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(opsem): expect memcpy opsem is called for memmove also","shortMessageHtmlLink":"fix(opsem): expect memcpy opsem is called for memmove also"}},{"before":"27d1f29f1177a0dd6765718c7705a07b8d2fe9f2","after":"561f54f9458e9b8fdbbfd8b89e68b1992f14d26c","ref":"refs/heads/dev14","pushedAt":"2023-10-19T16:11:52.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(opsem): add align constraint on sym length of mem{set,cpy}\n\nAlso unify alignment logic between sp0 and memset, memcpy\n\nThis belongs to memmgr since it can decided on what alignment to use.","shortMessageHtmlLink":"fix(opsem): add align constraint on sym length of mem{set,cpy}"}},{"before":"62e288a19c910c78fe8af56e0d7a4b10942aafc7","after":"27d1f29f1177a0dd6765718c7705a07b8d2fe9f2","ref":"refs/heads/dev14","pushedAt":"2023-10-08T23:34:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat: added resetDB function to HornClauseDB (#536)\n\nDone in order to allow reseting the DB while keeping the same object.\r\n\r\nSigned-off-by: Niv Sulimany <sulimany.niv@campus.technion.ac.il>","shortMessageHtmlLink":"feat: added resetDB function to HornClauseDB (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1920768485\" data-permission-text=\"Title is private\" data-url=\"https://github.com/seahorn/seahorn/issues/536\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/seahorn/seahorn/pull/536/hovercard\" href=\"https://github.com/seahorn/seahorn/pull/536\">#536</a>)"}},{"before":"2eb1ddb2b014bed0c710a588c9aa23f54e1a1fd6","after":"62e288a19c910c78fe8af56e0d7a4b10942aafc7","ref":"refs/heads/dev14","pushedAt":"2023-09-25T17:14:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix: missing list include (#533)\n\nMissing list include in header file houdini.hh\r\n\r\nSigned-off-by: Niv Sulimany <sulimany.niv@campus.technion.ac.il>","shortMessageHtmlLink":"fix: missing list include (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1910767266\" data-permission-text=\"Title is private\" data-url=\"https://github.com/seahorn/seahorn/issues/533\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/seahorn/seahorn/pull/533/hovercard\" href=\"https://github.com/seahorn/seahorn/pull/533\">#533</a>)"}},{"before":"cd425041c370725c0d2599143d8ce3916437110b","after":"2eb1ddb2b014bed0c710a588c9aa23f54e1a1fd6","ref":"refs/heads/dev14","pushedAt":"2023-09-08T21:30:08.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(opsem): fix ptrEq in extrawidememmgr\n\nptrEq should also take ptr size into account. Now it does.","shortMessageHtmlLink":"fix(opsem): fix ptrEq in extrawidememmgr"}},{"before":"5c01ca911a11bbc8399de3d5647c45df7e18e33d","after":"2bab7831960766a0a16f149adcdce55f0651eb8f","ref":"refs/heads/main","pushedAt":"2023-08-14T16:46:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"chore: adapt to changes in Clam API","shortMessageHtmlLink":"chore: adapt to changes in Clam API"}},{"before":"54b9f3acbfa219eb0cd9ba03e682bc21c107cdc7","after":"cd425041c370725c0d2599143d8ce3916437110b","ref":"refs/heads/dev14","pushedAt":"2023-08-13T02:15:55.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"feat(seapp): add option to run sealoopextractorpass","shortMessageHtmlLink":"feat(seapp): add option to run sealoopextractorpass"}},{"before":"3a231e569831b137c01505040c8059aaff7e756d","after":"54b9f3acbfa219eb0cd9ba03e682bc21c107cdc7","ref":"refs/heads/dev14","pushedAt":"2023-08-11T01:38:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(sea): help for reduce-main flag","shortMessageHtmlLink":"fix(sea): help for reduce-main flag"}},{"before":"33968d8c16c448fdae68b8ba2eabf3ac2b71e215","after":"3a231e569831b137c01505040c8059aaff7e756d","ref":"refs/heads/dev14","pushedAt":"2023-08-11T00:50:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"chore: adapt to changes in Clam API","shortMessageHtmlLink":"chore: adapt to changes in Clam API"}},{"before":"72065844c13ccb30dd2dff7ae340b2c9d89d169a","after":"33968d8c16c448fdae68b8ba2eabf3ac2b71e215","ref":"refs/heads/dev14","pushedAt":"2023-08-10T10:42:47.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(loop): more logging","shortMessageHtmlLink":"fix(loop): more logging"}},{"before":"ac627ca3ea39ce896bfa3f32739d5636c054cca5","after":"72065844c13ccb30dd2dff7ae340b2c9d89d169a","ref":"refs/heads/dev14","pushedAt":"2023-08-03T03:08:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"fix(seapp): issue #511","shortMessageHtmlLink":"fix(seapp): issue <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1834181260\" data-permission-text=\"Title is private\" data-url=\"https://github.com/seahorn/seahorn/issues/511\" data-hovercard-type=\"issue\" data-hovercard-url=\"/seahorn/seahorn/issues/511/hovercard\" href=\"https://github.com/seahorn/seahorn/issues/511\">#511</a>"}},{"before":"6bed4e57797799aef942ba853ba92f05337984a8","after":null,"ref":"refs/heads/promote-nondet-undef","pushedAt":"2023-07-25T17:12:34.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"}},{"before":"21695b65807fde6e1b3a4d8f8bc4fe5ae0df0905","after":"ac627ca3ea39ce896bfa3f32739d5636c054cca5","ref":"refs/heads/dev14","pushedAt":"2023-07-25T17:10:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat(py): option promote-nondet-undef (#503)\n\nThe default behavior is the same as before.","shortMessageHtmlLink":"feat(py): option promote-nondet-undef (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1817281471\" data-permission-text=\"Title is private\" data-url=\"https://github.com/seahorn/seahorn/issues/503\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/seahorn/seahorn/pull/503/hovercard\" href=\"https://github.com/seahorn/seahorn/pull/503\">#503</a>)"}},{"before":"f61ea7bd1df44af6ab398e0d1ffdbadca6fa583f","after":"6bed4e57797799aef942ba853ba92f05337984a8","ref":"refs/heads/promote-nondet-undef","pushedAt":"2023-07-25T16:35:39.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat(py): option promote-nondet-undef\nThe default behavior is the same as before.","shortMessageHtmlLink":"feat(py): option promote-nondet-undef"}},{"before":"c9c496f3ecef274742d1c3f6ca8324d02d44e183","after":"21695b65807fde6e1b3a4d8f8bc4fe5ae0df0905","ref":"refs/heads/dev14","pushedAt":"2023-07-25T16:24:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"fix(gsa): generate undef value when if both incoming undef\n\nCurrently we assert that only one of the incoming values must be undef, this is only caught in debug mode.\nRust compiler appears to generate undef values on both incoming edges.\nAs such, we should deal with gracefully. This is the simplest attempt at doing so.","shortMessageHtmlLink":"fix(gsa): generate undef value when if both incoming undef"}},{"before":null,"after":"f61ea7bd1df44af6ab398e0d1ffdbadca6fa583f","ref":"refs/heads/promote-nondet-undef","pushedAt":"2023-07-23T20:08:54.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat(py): option promote-nondet-undef\nThe default behavior is the same as before.","shortMessageHtmlLink":"feat(py): option promote-nondet-undef"}},{"before":"8bfaa6450bdb60460db6b8c9afb5aaf7f753de3b","after":"c9c496f3ecef274742d1c3f6ca8324d02d44e183","ref":"refs/heads/dev14","pushedAt":"2023-07-18T21:42:25.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"fix: clang format","shortMessageHtmlLink":"fix: clang format"}},{"before":"8bfaa6450bdb60460db6b8c9afb5aaf7f753de3b","after":null,"ref":"refs/heads/dev14-no-vectorization","pushedAt":"2023-07-04T17:39:28.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"}},{"before":null,"after":"8bfaa6450bdb60460db6b8c9afb5aaf7f753de3b","ref":"refs/heads/dev14-no-vectorization","pushedAt":"2023-07-04T17:38:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"fix(sea): disable vectorization by default\n\nLLVM12 or above broke our hack to disable vectorization.\nThis fixes the option and vectorization is disabled by default.","shortMessageHtmlLink":"fix(sea): disable vectorization by default"}},{"before":"08b60d6ea76336e89ef16800488a5ff6bb9ef32b","after":"8bfaa6450bdb60460db6b8c9afb5aaf7f753de3b","ref":"refs/heads/dev14","pushedAt":"2023-07-04T17:37:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agurfinkel","name":"Arie Gurfinkel","path":"/agurfinkel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6082023?s=80&v=4"},"commit":{"message":"fix(sea): disable vectorization by default\n\nLLVM12 or above broke our hack to disable vectorization.\nThis fixes the option and vectorization is disabled by default.","shortMessageHtmlLink":"fix(sea): disable vectorization by default"}},{"before":"e970fb6541f8298d90e8e58290fa091a1007070f","after":"08b60d6ea76336e89ef16800488a5ff6bb9ef32b","ref":"refs/heads/dev14","pushedAt":"2023-06-16T20:04:34.889Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"fix(dummymainpass): run only once since pass is not idempotent\n\nEarlier this pass used to add a main if one was absent.\nNow we are more aggressive and replace main.\nThis means that if we run more than once then we will undo the work of first run in second run.\nAdd to this, that inlining runs inbetween the passes -- we end up with a main that is a NOP.","shortMessageHtmlLink":"fix(dummymainpass): run only once since pass is not idempotent"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEUYnZKwA","startCursor":null,"endCursor":null}},"title":"Activity · seahorn/seahorn"}