Infer# v1.2: Interprocedural Memory Safety Analysis For C#

Last December, we announced the public preview release of Infer#, which brings the interprocedural static analysis of Infer to the .NET community. The project was open sourced on GitHub under an MIT license.

New Feature Highlights

Infer# 1.2 brings race condition detection, improves performance, provides more ways to use, and expands analysis coverage. The full list of improvements can be found on the release page.

Support for Infer# On Windows via WSL2 (Windows Subsystem for Linux)

As the first step in our initiative to provide Windows support for Infer#, you can now run the analysis in WSL2.

Azure Pipelines Integration

We now support Infer# as an Azure Pipelines plugin.

Race Condition

Infer# now supports race condition detection via Infer’s RacerD analyzer.

public class RaceCondition
{
    private readonly object _object = new object();

    public void TestMethod()
    {
        int FirstLocal;
        FirstLocal = TestClass.StaticIntegerField;
    }

    public void FieldWrite()
    {
        lock (_object)
        {
            {
                TestClass.StaticIntegerField = 1;
            }
        }
    }
}

Assets/RaceCondition.cs:12: warning: Thread Safety Violation
  Read/Write race. Non-private method `RaceCondition.TestMethod()` reads without synchronization from `Assets.TestClass.Cilsil.Test.Assets.TestClass.StaticIntegerField`. Potentially races with write in method `RaceCondition.FieldWrite()`.
 Reporting because another access to the same memory occurs on a background thread, although this access may not.

Exception Code Coverage

Infer# now reports warnings on methods with exception-handling constructs (for example, try-catch-finally, and lock).

public void ResourceLeakExcepHandlingBad() {
    StreamWriter stream = AllocateStreamWriter();
    try
    {
        stream.WriteLine(12);
    }
    catch
    {
        console.log("Fail to write");
    }
    finally
    {
        // FIXME: should close the stream by calling stream.Close().
    }
}

/.../Examples/Program.cs:39: error: Dotnet Resource Leak
  Leaked { %0 -> 1 } resource(s) at type(s) System.IO.StreamWriter.

Using Infer#

You can find the instructions for all supported scenarios on our GitHub landing page.

Please submit your feedback and feature requests to our GitHub repository. We’re looking at all feature requests from the community and will prioritize next steps based on popularity.