{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":95797011,"defaultBranch":"main","name":"sea-dsa","ownerLogin":"seahorn","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2017-06-29T16:25:09.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11098044?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1694881787.0","currentOid":""},"activityList":{"items":[{"before":"8fc33bd29b878c8975e958da594e67ba02bb42f4","after":"93edd5deb73d54206c6b382ef3e6e9362b377172","ref":"refs/heads/dev14","pushedAt":"2024-06-13T18:09:15.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: recognize ownsem instrinsic aliases","shortMessageHtmlLink":"feat: recognize ownsem instrinsic aliases"}},{"before":"910fa151f5bc3e67932a6c42394341f96fac3280","after":"8fc33bd29b878c8975e958da594e67ba02bb42f4","ref":"refs/heads/dev14","pushedAt":"2023-09-21T14:54:00.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"doc: updated badge in README","shortMessageHtmlLink":"doc: updated badge in README"}},{"before":"8fc33bd29b878c8975e958da594e67ba02bb42f4","after":"910fa151f5bc3e67932a6c42394341f96fac3280","ref":"refs/heads/dev14","pushedAt":"2023-09-19T03:20: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":"fix: memhavoc should be mem def","shortMessageHtmlLink":"fix: memhavoc should be mem def"}},{"before":"377320334277daf368dbc4ffb2cac1b66d03bb02","after":null,"ref":"refs/heads/master","pushedAt":"2023-09-16T16:29:47.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":"f46a5e38006a4a5d5adf25cbf4da6a85636890c5","after":null,"ref":"refs/heads/llvm-8.0","pushedAt":"2023-09-16T16:26:23.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":"a284e592d0d42137d1fc61673c67230d4f5b926d","after":null,"ref":"refs/heads/dev14-fix-tests","pushedAt":"2023-09-16T16:25:10.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":"a284e592d0d42137d1fc61673c67230d4f5b926d","after":"8fc33bd29b878c8975e958da594e67ba02bb42f4","ref":"refs/heads/main","pushedAt":"2023-09-16T16:24:17.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":"doc: updated badge in README","shortMessageHtmlLink":"doc: updated badge in README"}},{"before":"a284e592d0d42137d1fc61673c67230d4f5b926d","after":"8fc33bd29b878c8975e958da594e67ba02bb42f4","ref":"refs/heads/dev14","pushedAt":"2023-09-16T16:23:30.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":"doc: updated badge in README","shortMessageHtmlLink":"doc: updated badge in README"}},{"before":null,"after":"a284e592d0d42137d1fc61673c67230d4f5b926d","ref":"refs/heads/main","pushedAt":"2023-09-16T16:09:49.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":"fix(complete-cg): remove call graph edges\n\nThe right way to remove an edge in the call graph is by using the\nmethod removeCallEdge. Because this method takes as input an iterator\nwe are forced to remove edges while iterating over them so we need to\nbe careful.\n\nBefore, we were using removeCallEdgeFor that takes as input a call\ninstruction. However, once we start resolving an indirect call we can\nhave multiple edges from the same node and with the same callsite\nattached to the edge. Calling removeCallEdgeFor removes one of the\nedges but it is not clear which one. Probably the code was working\nbecause it was removing the first one which was the indirect call.\n\nFor context, I add here an explanation about how the complete call\ngraph looks like.\n\nA LLVM CallGraph consists of edges between nodes of type\nCallGraphNode. For CallGraphNode n1 and n2, and CallBase CB, an edge\nin CallGraph is a triple (n1, CB, n2)\n\nA _complete_ (seadsa) callgraph is just another LLVM CallGraph.\n\nIf there is an edge E=(n1, CB, n2) where CB is an indirect call and\ntherefore n2 is the (unique) _external node_ then we remove E and add\npossibly multiple edges (n1,CB,n3) where n3 is the CallGraphNode of\neach possible callee function identified by seadsa.","shortMessageHtmlLink":"fix(complete-cg): remove call graph edges"}},{"before":"4faf58ff1fbe1595fc9704331a2e8adf63ffc494","after":"a284e592d0d42137d1fc61673c67230d4f5b926d","ref":"refs/heads/dev14","pushedAt":"2023-09-16T16:05:36.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(complete-cg): remove call graph edges\n\nThe right way to remove an edge in the call graph is by using the\nmethod removeCallEdge. Because this method takes as input an iterator\nwe are forced to remove edges while iterating over them so we need to\nbe careful.\n\nBefore, we were using removeCallEdgeFor that takes as input a call\ninstruction. However, once we start resolving an indirect call we can\nhave multiple edges from the same node and with the same callsite\nattached to the edge. Calling removeCallEdgeFor removes one of the\nedges but it is not clear which one. Probably the code was working\nbecause it was removing the first one which was the indirect call.\n\nFor context, I add here an explanation about how the complete call\ngraph looks like.\n\nA LLVM CallGraph consists of edges between nodes of type\nCallGraphNode. For CallGraphNode n1 and n2, and CallBase CB, an edge\nin CallGraph is a triple (n1, CB, n2)\n\nA _complete_ (seadsa) callgraph is just another LLVM CallGraph.\n\nIf there is an edge E=(n1, CB, n2) where CB is an indirect call and\ntherefore n2 is the (unique) _external node_ then we remove E and add\npossibly multiple edges (n1,CB,n3) where n3 is the CallGraphNode of\neach possible callee function identified by seadsa.","shortMessageHtmlLink":"fix(complete-cg): remove call graph edges"}},{"before":null,"after":"a284e592d0d42137d1fc61673c67230d4f5b926d","ref":"refs/heads/dev14-fix-tests","pushedAt":"2023-09-15T04:00:33.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":"fix(complete-cg): remove call graph edges\n\nThe right way to remove an edge in the call graph is by using the\nmethod removeCallEdge. Because this method takes as input an iterator\nwe are forced to remove edges while iterating over them so we need to\nbe careful.\n\nBefore, we were using removeCallEdgeFor that takes as input a call\ninstruction. However, once we start resolving an indirect call we can\nhave multiple edges from the same node and with the same callsite\nattached to the edge. Calling removeCallEdgeFor removes one of the\nedges but it is not clear which one. Probably the code was working\nbecause it was removing the first one which was the indirect call.\n\nFor context, I add here an explanation about how the complete call\ngraph looks like.\n\nA LLVM CallGraph consists of edges between nodes of type\nCallGraphNode. For CallGraphNode n1 and n2, and CallBase CB, an edge\nin CallGraph is a triple (n1, CB, n2)\n\nA _complete_ (seadsa) callgraph is just another LLVM CallGraph.\n\nIf there is an edge E=(n1, CB, n2) where CB is an indirect call and\ntherefore n2 is the (unique) _external node_ then we remove E and add\npossibly multiple edges (n1,CB,n3) where n3 is the CallGraphNode of\neach possible callee function identified by seadsa.","shortMessageHtmlLink":"fix(complete-cg): remove call graph edges"}},{"before":null,"after":"d53828800460658a67b00105f6e3ebde903026ce","ref":"refs/heads/priyasiddharth-patch-2","pushedAt":"2023-09-08T13:31:21.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"doc: update readme\n\nOn first reading it is confusing to see that a pointer is represented by a cell and so is a struct node. I have tried to make it explicit.","shortMessageHtmlLink":"doc: update readme"}},{"before":"6457da6caaf6a2dd52a03f8306dac8ce0183927d","after":"377320334277daf368dbc4ffb2cac1b66d03bb02","ref":"refs/heads/master","pushedAt":"2023-09-08T13:26:02.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":"doc: update readme","shortMessageHtmlLink":"doc: update readme"}},{"before":null,"after":"02769401084ba17b57fa0f52875ed895abe64d43","ref":"refs/heads/priyasiddharth-patch-1","pushedAt":"2023-09-07T17:17:18.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"priyasiddharth","name":"Siddharth Priya","path":"/priyasiddharth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4746323?s=80&v=4"},"commit":{"message":"doc: update readme","shortMessageHtmlLink":"doc: update readme"}},{"before":"519d8b1f9f379b865c599ee21addeaac4b75b6cd","after":"4faf58ff1fbe1595fc9704331a2e8adf63ffc494","ref":"refs/heads/dev14","pushedAt":"2023-08-10T18:33:03.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(typeaware): treat [0 x i8] as omnichar\n\nRustC seems to use `[0 x i8]*` instead of `i8*`. Treating these types similar in\nsea-dsa to avoid unsoundness.","shortMessageHtmlLink":"fix(typeaware): treat [0 x i8] as omnichar"}},{"before":"fda066eff4271bafa626d0fa425ed34519d1fcaa","after":"519d8b1f9f379b865c599ee21addeaac4b75b6cd","ref":"refs/heads/dev14","pushedAt":"2023-07-15T07:10:54.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: correctly label functions in call graph DOT","shortMessageHtmlLink":"fix: correctly label functions in call graph DOT"}},{"before":"69701184a2b61f242324ca1fb3d19aa59a2b955b","after":"fa7b7ae21059bb79b04a117d3c949ac149e74aa6","ref":"refs/heads/dev13","pushedAt":"2023-04-24T21:03:23.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: incorrect clang-format version","shortMessageHtmlLink":"fix: incorrect clang-format version"}},{"before":"d6d4e5fe24552f9e16b2f7450d1f60b53c5eea6c","after":"fad61891456df3ca2db76f3e571b2159f3c8fd15","ref":"refs/heads/dev12","pushedAt":"2023-03-27T22:19:42.189Z","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":"Small fix to be able to build on Fedora","shortMessageHtmlLink":"Small fix to be able to build on Fedora"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEZLh_UQA","startCursor":null,"endCursor":null}},"title":"Activity ยท seahorn/sea-dsa"}