pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'f28faad627'
${ noResults }
infer_clone/infer/tests/codetoanalyze/cpp/pulse/issues.exp

18 lines
2.6 KiB
Raw Normal View History Unescape

[pulse] join of memory graphs Summary: Instead of the non-sensical piecewise join we had until now write a proper one. Hopefully the comments explain what it does. Main one: ``` (* high-level idea: maintain some union-find data structure to identify locations in one heap with locations in the other heap. Build the initial join state as follows: - equate all locations that correspond to identical variables in both stacks, eg joining stacks {x=1} and {x=2} adds "1=2" to the unification. - add all addresses reachable from stack variables to the join state heap This gives us an abstract state that is the union of both abstract states, but more states can still be made equal. For instance, if 1 points to 3 in the first heap and 2 points to 4 in the second heap and we deduced "1 = 2" from the stacks already (as in the example just above) then we can deduce "3 = 4". Proceed in this fashion until no more equalities are discovered, and return the abstract state where a canonical representative has been chosen consistently for each equivalence class (this is what the union-find data structure gives us). *) ``` Reviewed By: mbouaziz Differential Revision: D10483978 fbshipit-source-id: f6ffd7528
6 years ago
codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here]
codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here]
[pulse] rename `Location` -> `Address` and better reporting Summary: `Location` was clashing with the `Location` module, so use `Address` instead. When invalidating an address, remember the "actor" of its invalidation, i.e. the access expression leading to the address and the source location of the corresponding instruction. When checking accesses, also pass the actor responsible for the access, so that when we raise an error we know: 1. when and why a location was invalidated 2. when and why we tried to read it after that Reviewed By: mbouaziz Differential Revision: D10446282 fbshipit-source-id: 3ca4fb3d4
6 years ago
codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `x` here,accessed `x` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
[pulse] join of memory graphs Summary: Instead of the non-sensical piecewise join we had until now write a proper one. Hopefully the comments explain what it does. Main one: ``` (* high-level idea: maintain some union-find data structure to identify locations in one heap with locations in the other heap. Build the initial join state as follows: - equate all locations that correspond to identical variables in both stacks, eg joining stacks {x=1} and {x=2} adds "1=2" to the unification. - add all addresses reachable from stack variables to the join state heap This gives us an abstract state that is the union of both abstract states, but more states can still be made equal. For instance, if 1 points to 3 in the first heap and 2 points to 4 in the second heap and we deduced "1 = 2" from the stacks already (as in the example just above) then we can deduce "3 = 4". Proceed in this fashion until no more equalities are discovered, and return the abstract state where a canonical representative has been chosen consistently for each equivalence class (this is what the union-find data structure gives us). *) ``` Reviewed By: mbouaziz Differential Revision: D10483978 fbshipit-source-id: f6ffd7528
6 years ago
codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `v.__internal_array[_]` here]
[pulse] rename `Location` -> `Address` and better reporting Summary: `Location` was clashing with the `Location` module, so use `Address` instead. When invalidating an address, remember the "actor" of its invalidation, i.e. the access expression leading to the address and the source location of the corresponding instruction. When checking accesses, also pass the actor responsible for the access, so that when we raise an error we know: 1. when and why a location was invalidated 2. when and why we tried to read it after that Reviewed By: mbouaziz Differential Revision: D10446282 fbshipit-source-id: 3ca4fb3d4
6 years ago
codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_throw_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_exit_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s->f` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s->f` here]
[pulse] join of memory graphs Summary: Instead of the non-sensical piecewise join we had until now write a proper one. Hopefully the comments explain what it does. Main one: ``` (* high-level idea: maintain some union-find data structure to identify locations in one heap with locations in the other heap. Build the initial join state as follows: - equate all locations that correspond to identical variables in both stacks, eg joining stacks {x=1} and {x=2} adds "1=2" to the unification. - add all addresses reachable from stack variables to the join state heap This gives us an abstract state that is the union of both abstract states, but more states can still be made equal. For instance, if 1 points to 3 in the first heap and 2 points to 4 in the second heap and we deduced "1 = 2" from the stacks already (as in the example just above) then we can deduce "3 = 4". Proceed in this fashion until no more equalities are discovered, and return the abstract state where a canonical representative has been chosen consistently for each equivalence class (this is what the union-find data structure gives us). *) ``` Reviewed By: mbouaziz Differential Revision: D10483978 fbshipit-source-id: f6ffd7528
6 years ago
codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `result` here,accessed `*(result)` here]
[pulse] rename `Location` -> `Address` and better reporting Summary: `Location` was clashing with the `Location` module, so use `Address` instead. When invalidating an address, remember the "actor" of its invalidation, i.e. the access expression leading to the address and the source location of the corresponding instruction. When checking accesses, also pass the actor responsible for the access, so that when we raise an error we know: 1. when and why a location was invalidated 2. when and why we tried to read it after that Reviewed By: mbouaziz Differential Revision: D10446282 fbshipit-source-id: 3ca4fb3d4
6 years ago
codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(x).__internal_array[_]` here,accessed `*(y)` here]