-
Notifications
You must be signed in to change notification settings - Fork 436
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Question: the path of SVFG for branches #1306
Comments
@jumormt could you have a look? |
This case is tricky. Different from head2, the conditional free path for head1 should be the if-else branch. It seems that the value-flow guard between p@Line 11 and p@Line 15 should be Regarding why head1 does not pass through the if-then block, the points-to set of head1@Line 11 does not pass to p@Line 13 (i.e., no indirect value-flow between p@Line 11 and p@Line 13) because it is a strong update at Line 13. Therefore, saber removes that redundant indirect value-flow. |
The value-flow guard for 11-15 is missing? If not missing, there is supposed to be a conditional free? |
Due to the holiday a few days ago, I didn't see your reply, sorry. Your update fixes my issue, thank you |
When using Saber to test this test code, the expected results were not obtained
my codes:
The correct result should be that both head1 and head2 report
PartialLeaf
But the test results show that head1 has no memory leak, while head2 reports PartialLeak
I checked the slice diagram and found that the path from the malloc node of head1 to the free node did not pass through
if...then
block, may I ask why this is?The text was updated successfully, but these errors were encountered: