Static checker can't prove ForAll on Roslyn-compiled inline arrays

The static checker can't prove that `ForAll` in `new object[] { 1, 2, 3, 4}', the object is not null.

Code:

```
using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace ContractForAll
{
    public class Program
    {
        public static void Main(string[] args)
        {
            var objects = new object[] { 1, 2, 3, 4 };
            WriteObjects(objects);

            Console.ReadKey();
        }

        static void WriteObjects(IEnumerable<object> objects)
        {
            Contract.Requires(objects != null);
            Contract.Requires(Contract.ForAll(objects, o => o != null));

            foreach (var obj in objects)
            {
                Console.WriteLine(obj);
            }
        }
    }
}
```

VS2013 output:

```
1>------ Rebuild All started: Project: ContractForAll, Configuration: Debug Any CPU ------
CodeContracts: ContractForAll: Schedule static contract analysis.
CodeContracts: ContractForAll: Background contract analysis started.
1>  elapsed time: 147.8448ms
1>  ContractForAll -> C:\Temp\ContractForAll\ContractForAll\bin\Debug\ContractForAll.exe
========== Rebuild All: 1 succeeded, 0 failed, 0 skipped ==========
CodeContracts: ContractForAll: Time spent connecting to the cache: 00:00:01.0910416
CodeContracts: ContractForAll: Cache used: (LocalDb)\MSSQLLocalDB
CodeContracts: ContractForAll: Validated: 100.0%
CodeContracts: ContractForAll: Checked 21 assertions: 21 correct
CodeContracts: ContractForAll: Contract density: 1.57
CodeContracts: ContractForAll: Total methods analyzed 4
CodeContracts: ContractForAll: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractForAll: Method analyses read from the cache 2
CodeContracts: ContractForAll: Methods not found in the cache 2
CodeContracts: ContractForAll: Methods with 0 warnings 4
CodeContracts: ContractForAll: Time spent in internal, potentially costly, operations
CodeContracts: ContractForAll: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0190207 (invoked 3441 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0109988 (invoked 3279 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0170017 (invoked 20 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.1069932 (invoked 83 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0709862 (invoked 42 times)
Overall time spent performing action #Simplex: 00:00:00.0709878 (invoked 302 times)
Overall time spent performing action #SubPolyJoin: 00:00:00.1390107 (invoked 41 times)
Overall time spent performing action #WP: 00:00:00.0490001 (invoked 2 times)
CodeContracts: ContractForAll: Total time 4.448sec. 1112ms/method
CodeContracts: ContractForAll: Retained 0 preconditions after filtering
CodeContracts: ContractForAll: Inferred 0 object invariants
CodeContracts: ContractForAll: Retained 0 object invariants after filtering
CodeContracts: ContractForAll: Discovered 1 postconditions to suggest
CodeContracts: ContractForAll: Retained 0 postconditions after filtering
CodeContracts: ContractForAll: Detected 0 code fixes
CodeContracts: ContractForAll: Proof obligations with a code fix: 0
C:\Program Files (x86)\Microsoft Visual Studio 12.0\Common7\IDE\ContractForAll.exe(1,1): message : CodeContracts: Checked 21 assertions: 21 correct
CodeContracts: ContractForAll: 
CodeContracts: ContractForAll: Background contract analysis done.
```

VS2015 output:

```
1>------ Rebuild All started: Project: ContractForAll, Configuration: Debug Any CPU ------
CodeContracts: ContractForAll: Schedule static contract analysis.
CodeContracts: ContractForAll: Background contract analysis started.
1>  elapsed time: 144.8568ms
1>  ContractForAll -> C:\Temp\ContractForAll\ContractForAll\bin\Debug\ContractForAll.exe
========== Rebuild All: 1 succeeded, 0 failed, 0 skipped ==========
CodeContracts: ContractForAll: Time spent connecting to the cache: 00:00:01.1950455
CodeContracts: ContractForAll: Cache used: (LocalDb)\MSSQLLocalDB
CodeContracts: ContractForAll: Validated:  95.2%
CodeContracts: ContractForAll: Checked 21 assertions: 20 correct 1 unknown
CodeContracts: ContractForAll: Contract density: 1.74
CodeContracts: ContractForAll: Total methods analyzed 4
CodeContracts: ContractForAll: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractForAll: Method analyses read from the cache 2
CodeContracts: ContractForAll: Methods not found in the cache 2
CodeContracts: ContractForAll: Methods with 0 warnings 3
CodeContracts: ContractForAll: Time spent in internal, potentially costly, operations
CodeContracts: ContractForAll: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0249749 (invoked 3743 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0139951 (invoked 3552 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0170028 (invoked 23 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.1080109 (invoked 71 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0699943 (invoked 42 times)
Overall time spent performing action #Simplex: 00:00:00.0810813 (invoked 303 times)
Overall time spent performing action #SubPolyJoin: 00:00:00.1450139 (invoked 41 times)
Overall time spent performing action #WP: 00:00:00.0610050 (invoked 3 times)
CodeContracts: ContractForAll: Total time 5.017sec. 1254ms/method
CodeContracts: ContractForAll: Retained 0 preconditions after filtering
CodeContracts: ContractForAll: Inferred 0 object invariants
CodeContracts: ContractForAll: Retained 0 object invariants after filtering
CodeContracts: ContractForAll: Discovered 1 postconditions to suggest
CodeContracts: ContractForAll: Retained 0 postconditions after filtering
CodeContracts: ContractForAll: Detected 0 code fixes
CodeContracts: ContractForAll: Proof obligations with a code fix: 0
C:\Temp\ContractForAll\ContractForAll\Class1.cs(12,13): warning : CodeContracts: requires unproven: Contract.ForAll(objects, o => o != null)
C:\Temp\ContractForAll\ContractForAll\Class1.cs(20,13): warning :   + location related to previous warning
C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\ContractForAll.exe(1,1): message : CodeContracts: Checked 21 assertions: 20 correct 1 unknown
CodeContracts: ContractForAll: 
CodeContracts: ContractForAll: Background contract analysis done.
```

IL of `Main`, VS2013, according to ILSpy:

```
.method public hidebysig static 
    void Main (
        string[] args
    ) cil managed 
{
    // Method begins at RVA 0x2048
    // Code size 60 (0x3c)
    .maxstack 3
    .entrypoint
    .locals init (
        [0] object[] objects,
        [1] object[] CS$0$0000
    )

    IL_0000: nop
    IL_0001: ldc.i4.4
    IL_0002: newarr [mscorlib]System.Object
    IL_0007: stloc.1
    IL_0008: ldloc.1
    IL_0009: ldc.i4.0
    IL_000a: ldc.i4.1
    IL_000b: box [mscorlib]System.Int32
    IL_0010: stelem.ref
    IL_0011: ldloc.1
    IL_0012: ldc.i4.1
    IL_0013: ldc.i4.2
    IL_0014: box [mscorlib]System.Int32
    IL_0019: stelem.ref
    IL_001a: ldloc.1
    IL_001b: ldc.i4.2
    IL_001c: ldc.i4.3
    IL_001d: box [mscorlib]System.Int32
    IL_0022: stelem.ref
    IL_0023: ldloc.1
    IL_0024: ldc.i4.3
    IL_0025: ldc.i4.4
    IL_0026: box [mscorlib]System.Int32
    IL_002b: stelem.ref
    IL_002c: ldloc.1
    IL_002d: stloc.0
    IL_002e: ldloc.0
    IL_002f: call void ContractForAll.Program::WriteObjects(class [mscorlib]System.Collections.Generic.IEnumerable`1<object>)
    IL_0034: nop
    IL_0035: call valuetype [mscorlib]System.ConsoleKeyInfo [mscorlib]System.Console::ReadKey()
    IL_003a: pop
    IL_003b: ret
} // end of method Program::Main
```

IL of `Main`, VS2015, according to ILSpy:

```
.method public hidebysig static 
    void Main (
        string[] args
    ) cil managed 
{
    // Method begins at RVA 0x2048
    // Code size 58 (0x3a)
    .maxstack 4
    .entrypoint
    .locals init (
        [0] object[] objects
    )

    IL_0000: nop
    IL_0001: ldc.i4.4
    IL_0002: newarr [mscorlib]System.Object
    IL_0007: dup
    IL_0008: ldc.i4.0
    IL_0009: ldc.i4.1
    IL_000a: box [mscorlib]System.Int32
    IL_000f: stelem.ref
    IL_0010: dup
    IL_0011: ldc.i4.1
    IL_0012: ldc.i4.2
    IL_0013: box [mscorlib]System.Int32
    IL_0018: stelem.ref
    IL_0019: dup
    IL_001a: ldc.i4.2
    IL_001b: ldc.i4.3
    IL_001c: box [mscorlib]System.Int32
    IL_0021: stelem.ref
    IL_0022: dup
    IL_0023: ldc.i4.3
    IL_0024: ldc.i4.4
    IL_0025: box [mscorlib]System.Int32
    IL_002a: stelem.ref
    IL_002b: stloc.0
    IL_002c: ldloc.0
    IL_002d: call void ContractForAll.Program::WriteObjects(class [mscorlib]System.Collections.Generic.IEnumerable`1<object>)
    IL_0032: nop
    IL_0033: call valuetype [mscorlib]System.ConsoleKeyInfo [mscorlib]System.Console::ReadKey()
    IL_0038: pop
    IL_0039: ret
} // end of method Program::Main
```


Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Static checker can't prove ForAll on Roslyn-compiled inline arrays #204

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Static checker can't prove ForAll on Roslyn-compiled inline arrays #204

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions