infer_clone/infer/tests/codetoanalyze/c/pulse/issues.exp

codetoanalyze/c/pulse/frontend.c, assign_implicit_cast_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/frontend.c, assign_paren_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid2_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `call_if_freed_invalid_latent`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
codetoanalyze/c/pulse/interprocedural.c, test_modified_value_then_error_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, interprocedural_nop_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, interprocedural_read_in_callee_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,when calling `read_int_ref` here,parameter `p` of read_int_ref,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, interprocedural_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f2` created,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, interprocedural_uninit_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [passed as argument to `uninit`,return from call to `uninit`,assigned,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),assigned,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, nested_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `g1.f1` created,when calling `read_g1_f1` here,parameter `x` of read_g1_f1,read to uninitialized value occurs here]
codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
[pulse] Adapting error messages Summary: Adapting error messages in Pulse so that they become more intuitive for developers. Reviewed By: jvillard Differential Revision: D26887140 fbshipit-source-id: 896970ba2 4 years ago			`codetoanalyze/c/pulse/frontend.c, assign_implicit_cast_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
			`codetoanalyze/c/pulse/frontend.c, assign_paren_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
			codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid2_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `call_if_freed_invalid_latent`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
			codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [* LATENT *,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
ISL tests Reviewed By: jvillard Differential Revision: D24433559 fbshipit-source-id: 4d7a4c221 4 years ago			codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [* LATENT *,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
[pulse] discard "pruned" atoms that refer to variables outside the pre Summary: See added test: pulse sometimes insisted that an issue was latent even though the condition that made it latent could not be influenced (hence could the issue could never become manifest) by callers because it was unrelated to the pre, i.e. it came from a mutation inside the function. In these cases, we want to report the issue straight away instead of keeping it latent. Reviewed By: skcho Differential Revision: D28002725 fbshipit-source-id: ce9e6f190 4 years ago			`codetoanalyze/c/pulse/interprocedural.c, test_modified_value_then_error_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
[pulse] Enable pulse memory leaks and disable biabduction one Summary: The new memory leaks analysis is now ready to be enabled by default and turned on in production. This also replaces the biabduction one which is now disabled. Reviewed By: jvillard Differential Revision: D21998666 fbshipit-source-id: 9cd95e894 5 years ago			codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
			codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
			codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
[pulse][isl] manifest errors Reviewed By: jvillard Differential Revision: D27405377 fbshipit-source-id: e69e02c0d 4 years ago			`codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
[pulse] make sure we do not leak local mutations of formals into the summary Summary: Before returning a summary, restore formals to their initial values. This gets rid of a false latent because the value in the path condition is now garbage-collected. Added a test for the tricky case of structs passed as values. Reviewed By: skcho Differential Revision: D28001229 fbshipit-source-id: 23dda5b43 4 years ago			`codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
[pulse][isl] manifest errors Reviewed By: jvillard Differential Revision: D27405377 fbshipit-source-id: e69e02c0d 4 years ago			`codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
[pulse] Adapting error messages Summary: Adapting error messages in Pulse so that they become more intuitive for developers. Reviewed By: jvillard Differential Revision: D26887140 fbshipit-source-id: 896970ba2 4 years ago			codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
[pulse] use term_eqs Summary: Whenever an equality "t = v" (t an arbitrary term, v a variable) is added (or "v = t"), remember the "t -> v" mapping after canonicalising t and v. Use this to detect when two variables are equal to the same term: `t = v` and `t = v'` now yields `v = v'` to be added to the equality relation of variables. This increases the precision of the arithmetic engine. Interestingly, the impact on most code I've tried is: 1. mostly same perfs as before, if a bit slower (could be within noise) 2. slightly more (latent) bugs reported in absolute numbers I would have expected it to be more expensive and yield fewer bugs (as fewer false positives), but there could be second-order effects at play here where we get more coverage. We definitely get more latent issues due to dereferencing pointers after testing nullness, as can be seen in the unit tests as well, which may alone explain (2). There's some complexity when adding term equalities where the term is linear, as we also need to add it to `linear_eqs` but `term_eqs` and `linear_eqs` are interested in slightly different normal forms. Reviewed By: skcho Differential Revision: D27331336 fbshipit-source-id: 7314e127a 4 years ago			codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [* LATENT *,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here]
[pulse] Adapting error messages Summary: Adapting error messages in Pulse so that they become more intuitive for developers. Reviewed By: jvillard Differential Revision: D26887140 fbshipit-source-id: 896970ba2 4 years ago			`codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]`
[pulse] Revise trace of uninitialized value check Summary: This diff revises the trace generation of the uninitialized value checker, by introducing a new diagnostics for it. Reviewed By: jvillard Differential Revision: D25433775 fbshipit-source-id: 1279c0de4 4 years ago			codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
			codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here]
			codetoanalyze/c/pulse/uninit.c, interprocedural_nop_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
			codetoanalyze/c/pulse/uninit.c, interprocedural_read_in_callee_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,when calling `read_int_ref` here,parameter `p` of read_int_ref,read to uninitialized value occurs here]
[pulse] Uninitialized check for struct fields Reviewed By: jvillard Differential Revision: D25371929 fbshipit-source-id: 966f333e3 4 years ago			codetoanalyze/c/pulse/uninit.c, interprocedural_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f2` created,read to uninitialized value occurs here]
[pulse] Revise trace of uninitialized value check Summary: This diff revises the trace generation of the uninitialized value checker, by introducing a new diagnostics for it. Reviewed By: jvillard Differential Revision: D25433775 fbshipit-source-id: 1279c0de4 4 years ago			codetoanalyze/c/pulse/uninit.c, interprocedural_uninit_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [passed as argument to `uninit`,return from call to `uninit`,assigned,read to uninitialized value occurs here]
			codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),assigned,read to uninitialized value occurs here]
[uninit] Revise error message to include access paths Summary: This diff finds a declared variable name or declared field names from trace, then constructs an error message including access paths. Reviewed By: jvillard Differential Revision: D26544275 fbshipit-source-id: 135c90a1b 4 years ago			codetoanalyze/c/pulse/uninit.c, nested_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `g1.f1` created,when calling `read_g1_f1` here,parameter `x` of read_g1_f1,read to uninitialized value occurs here]
[pulse] Revise trace of uninitialized value check Summary: This diff revises the trace generation of the uninitialized value checker, by introducing a new diagnostics for it. Reviewed By: jvillard Differential Revision: D25433775 fbshipit-source-id: 1279c0de4 4 years ago			codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]