You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jul 15, 2023. It is now read-only.
It appears that Contract.ForAll never validates statically in Visual Studio 2015 while the same code is validated without a problem in Visual Studio 2012 (did not test in Visual Studio 2013).
Here's a minimal application to illustrate the issue:
usingSystem;usingSystem.Diagnostics.Contracts;namespaceArrays{classProgram{staticvoidMain(string[]args){Contract.Assume(args!=null);Contract.Assume(args.Length>0);Contract.Assume(Contract.ForAll(args, a =>a!=null));Console.WriteLine(Method(args));}staticintMethod(string[]args){Contract.Requires(args!=null);Contract.Requires(args.Length>0);Contract.Requires(Contract.ForAll(args, a =>a!=null));returnargs[0].Length;}}}
When compiling in Visual Studio 2012, the output is as follows:
CodeContracts: Arrays: Run static contract analysis.
C:\Projects\Contracts\Arrays\Arrays\Program.cs(10,13): message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert.
C:\Projects\Contracts\Arrays\Arrays\Program.cs(12,13): message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert.
CodeContracts: Arrays: Validated: 100.0 %
CodeContracts: Arrays: Checked 13 assertions: 13 correct
CodeContracts: Arrays: Contract density: 1.65
CodeContracts: Arrays: Total methods analyzed 4
CodeContracts: Arrays: Methods analyzed with a faster abstract domain 0
CodeContracts: Arrays: Methods with 0 warnings 4
CodeContracts: Arrays: Time spent in internal, potentially costly, operations
CodeContracts: Arrays: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0180010 (invoked 526 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0200009 (invoked 1255 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0200011 (invoked 15 times)
Overall time spent performing action #Simplex: 00:00:00.0910052 (invoked 35 times)
Overall time spent performing action #WP: 00:00:00.1160064 (invoked 4 times)
CodeContracts: Arrays: Total time 6.961sec. 1740ms/method
CodeContracts: Arrays: Retained 0 preconditions after filtering
CodeContracts: Arrays: Inferred 0 object invariants
CodeContracts: Arrays: Retained 0 object invariants after filtering
CodeContracts: Arrays: Detected 0 code fixes
CodeContracts: Arrays: Proof obligations with a code fix: 0
C:\Program Files (x86)\Microsoft Visual Studio 11.0\Common7\IDE\Arrays.exe(1,1): message : CodeContracts: Checked 13 assertions: 13 correct
CodeContracts: Arrays:
CodeContracts: Arrays: Static contract analysis done.
When compiling in Visual Studio 2015, the output is different:
CodeContracts: Arrays: Run static contract analysis.
C:\Projects\Arrays\Arrays\Program.cs(10,13): message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert.
CodeContracts: Arrays: Validated: 84.6 %
CodeContracts: Arrays: Checked 13 assertions: 11 correct 2 unknown
CodeContracts: Arrays: Contract density: 1.64
CodeContracts: Arrays: Total methods analyzed 4
CodeContracts: Arrays: Methods analyzed with a faster abstract domain 0
CodeContracts: Arrays: Methods with 0 warnings 2
CodeContracts: Arrays: Time spent in internal, potentially costly, operations
CodeContracts: Arrays: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0210344 (invoked 666 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0180034 (invoked 1571 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0190029 (invoked 18 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.0860030 (invoked 3 times)
Overall time spent performing action #Simplex: 00:00:00.0510336 (invoked 50 times)
Overall time spent performing action #SubPolyJoin: 00:00:00.2000088 (invoked 3 times)
Overall time spent performing action #WP: 00:00:00.4369996 (invoked 7 times)
CodeContracts: Arrays: Total time 4.843sec. 1210ms/method
CodeContracts: Arrays: Retained 0 preconditions after filtering
CodeContracts: Arrays: Inferred 0 object invariants
CodeContracts: Arrays: Retained 0 object invariants after filtering
CodeContracts: Arrays: Detected 0 code fixes
CodeContracts: Arrays: Proof obligations with a code fix: 0
C:\Projects\Arrays\Arrays\Program.cs(23,13): warning : CodeContracts: Possibly calling a method on a null reference
C:\Projects\Arrays\Arrays\Program.cs(14,13): warning : CodeContracts: requires unproven: Contract.ForAll(args, a => a != null)
C:\Projects\Arrays\Arrays\Program.cs(21,13): warning : + location related to previous warning
C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\Arrays.exe(1,1): message : CodeContracts: Checked 13 assertions: 11 correct 2 unknown
CodeContracts: Arrays:
CodeContracts: Arrays: Static contract analysis done.
Note that it behaves as if Contract.Assume(Contract.ForAll(args, a => a != null)); has no effect.
I've changed the logic for ccrewriter to understand new IL code pattern, but my assumption was that cccheck is using the same logic. Apparently, I was wrong. I'll take a look at this issue, because I've already fixed similar one for ccrewrite.
It appears that Contract.ForAll never validates statically in Visual Studio 2015 while the same code is validated without a problem in Visual Studio 2012 (did not test in Visual Studio 2013).
Here's a minimal application to illustrate the issue:
When compiling in Visual Studio 2012, the output is as follows:
When compiling in Visual Studio 2015, the output is different:
Note that it behaves as if
Contract.Assume(Contract.ForAll(args, a => a != null));
has no effect.Full project source code is available at https://www.dropbox.com/s/3xbs3q819xx0l90/Arrays.zip?dl=0.
The text was updated successfully, but these errors were encountered: