Infer# is an interprocedural and scalable static code analyzer for C#. Via the capabilities of Facebook's Infer, this tool detects null dereferences, resource leaks, and thread-safety violations. It also performs taint flow tracking to detect critical security vulnerabilities like SQL injections.
Methods that return a task which wraps a class that has underlying resources can cause Infer# to report a false positive on the underlying resources. In this case, it reports on the FileStream object here.
This happens because the ultimate TakeAndDispose object is not actually returned (the compiler-generated "MoveNext()" method actually returns null), but is rather still reachable within the broader program space via the method "_fun_Void AsyncTaskMethodBuilder`1<!0>.SetResult(!0)" as seen here:
There is at present no model for SetResult, so it is unknown and hence Infer doesn't actually know that TakeAndDispose (and therefore its underlying FileStream) are still reachable in the program space. TakeAndDispose will not be reported upon because Infer suppresses the reporting of types that are passed to unknown functions as in this case. However, the FileStream doesn't also get suppressed and therefore gets reported.
Methods that return a task which wraps a class that has underlying resources can cause Infer# to report a false positive on the underlying resources. In this case, it reports on the FileStream object here.
This happens because the ultimate TakeAndDispose object is not actually returned (the compiler-generated "MoveNext()" method actually returns null), but is rather still reachable within the broader program space via the method "_fun_Void AsyncTaskMethodBuilder`1<!0>.SetResult(!0)" as seen here:
n$18=_fun_Void AsyncTaskMethodBuilder
1<!0>.SetResult(!0)(n$15.InferResourceLeakTests$d__1.<>t__builder:System.Runtime.CompilerServices.AsyncTaskMethodBuilder1,n$17:TakeAndDispose) [line 136, column 5];There is at present no model for SetResult, so it is unknown and hence Infer doesn't actually know that TakeAndDispose (and therefore its underlying FileStream) are still reachable in the program space. TakeAndDispose will not be reported upon because Infer suppresses the reporting of types that are passed to unknown functions as in this case. However, the FileStream doesn't also get suppressed and therefore gets reported.