From dca9f67890888e2f230275f6a5f731d7ea45a7f1 Mon Sep 17 00:00:00 2001 From: Francesco Logozzo Date: Sun, 19 Jul 2015 12:18:20 -0500 Subject: [PATCH] Reformat code in ClousotCacheTests This reformat operation used dotnet/codeformatter@1d719e4e with /rule-:FieldNames /c:FIRST. --- .../Properties/AssemblyInfo.cs | 17 +- .../ClousotCacheTests/Sources/DB.cs | 84 ++- .../Sources/SemanticBaseliningTests.cs | 535 +++++++++--------- .../Sources/Serialization.cs | 265 +++++---- .../Sources/SerializationInferred.cs | 338 ++++++----- .../ClousotCacheTests/Sources/Test.cs | 397 +++++++------ .../ClousotCacheTests/Sources/Test2.cs | 317 +++++------ .../Sources/TestQuantifiers.cs | 71 +-- .../RegressionTest/ClousotCacheTests/Tests.cs | 305 +++++----- 9 files changed, 1115 insertions(+), 1214 deletions(-) diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Properties/AssemblyInfo.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Properties/AssemblyInfo.cs index 985a03e9..621b032f 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Properties/AssemblyInfo.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Properties/AssemblyInfo.cs @@ -1,16 +1,5 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System.Reflection; using System.Runtime.CompilerServices; @@ -24,7 +13,7 @@ [assembly: AssemblyConfiguration("")] [assembly: AssemblyCompany("Microsoft")] [assembly: AssemblyProduct("ClousotCacheTests")] -[assembly: AssemblyCopyright("Copyright © Microsoft 2010")] +[assembly: AssemblyCopyright("Copyright \u00A9 Microsoft 2010")] [assembly: AssemblyTrademark("")] [assembly: AssemblyCulture("")] diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/DB.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/DB.cs index c6e1c969..3c294aaf 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/DB.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/DB.cs @@ -1,67 +1,57 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; // Stressing the function name maximum length that can be stored in the DB + namespace Caching { - using A = IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName.IAmAGenericClassWithARelativelyLongName; - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName - { - class IAmAGenericClassWithARelativelyLongName { } - } - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName - { - using B = IAmAGenericClassWithARelativelyLongName; - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName2 + using A = IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName.IAmAGenericClassWithARelativelyLongName; + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName + { + internal class IAmAGenericClassWithARelativelyLongName { } + } + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName { - using C = IAmAGenericClassWithARelativelyLongName; - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName3 - { - using D = IAmAGenericClassWithARelativelyLongName; - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName4 + using B = IAmAGenericClassWithARelativelyLongName; + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName2 { - using E = IAmAGenericClassWithARelativelyLongName; - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName5 - { - using F = IAmAGenericClassWithARelativelyLongName; - namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName6 + using C = IAmAGenericClassWithARelativelyLongName; + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName3 { - using G = IAmAGenericClassWithARelativelyLongName; + using D = IAmAGenericClassWithARelativelyLongName; + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName4 + { + using E = IAmAGenericClassWithARelativelyLongName; + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName5 + { + using F = IAmAGenericClassWithARelativelyLongName; + namespace IAmANamespaceWithARelativelyLongNameContainingAGenericClassWithARelativelyLongName6 + { + using G = IAmAGenericClassWithARelativelyLongName; - class IAmAStaticClassWithARelativelyLongName - { - [ClousotRegressionTest] + internal class IAmAStaticClassWithARelativelyLongName + { + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("No entry found in the cache")] // we won't save this as it is too long - // [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("No entry found in the cache")] // we won't save this as it is too long + // [RegressionOutcome("An entry has been found in the cache")] #endif - public static void IAmAFunctionWithARelativelyLongNameUsingTheGenericClassWithARelativelyLongName(G x) - { - Contract.Requires(x != null); - Console.WriteLine(x); + public static void IAmAFunctionWithARelativelyLongNameUsingTheGenericClassWithARelativelyLongName(G x) + { + Contract.Requires(x != null); + Console.WriteLine(x); + } + } + } + } } - } } - } } - } } - } } diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SemanticBaseliningTests.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SemanticBaseliningTests.cs index 19385aa9..0ab073e7 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SemanticBaseliningTests.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SemanticBaseliningTests.cs @@ -1,52 +1,40 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -class Obj +internal class Obj { - public Obj() { } - public extern int FooBar(); - public static extern Obj MakeObj(); - public int f; - public int g; + public Obj() { } + public extern int FooBar(); + public static extern Obj MakeObj(); + public int f; + public int g; } -class Test +internal class Test { - #if !CLOUSOT2 - // check for persisting inferred assume across versions to maintain suppression - [ClousotRegressionTest] + // check for persisting inferred assume across versions to maintain suppression + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly calling a method on a null reference 'b'", PrimaryILOffset = 1, MethodILOffset = 0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on FooBar that the static checker is unaware of? ",PrimaryILOffset=14,MethodILOffset=0)] - public int Test1(Obj b) - { - int tmp = b.FooBar(); - Contract.Assert(tmp >= 0); - return 7; - } - + [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly calling a method on a null reference 'b'", PrimaryILOffset = 1, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on FooBar that the static checker is unaware of? ", PrimaryILOffset = 14, MethodILOffset = 0)] + public int Test1(Obj b) + { + int tmp = b.FooBar(); + Contract.Assert(tmp >= 0); + return 7; + } + #else [RegressionOutcome("No entry found in the cache")] // can't find method by hash... [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=1,MethodILOffset=0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 1, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 20, MethodILOffset = 0)] public int Test1(Obj b) { @@ -58,289 +46,296 @@ public int Test1(Obj b) } #endif - // check that a new warning of the same type that should be reported is still reported - [ClousotRegressionTest] + // check that a new warning of the same type that should be reported is still reported + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possibly accessing a field on a null reference 'o2'. Are you making some assumption on MakeObj that the static checker is unaware of? ",PrimaryILOffset=7,MethodILOffset=0)] - public int Test2(Obj o1, int j) - { - Obj o2 = Obj.MakeObj(); - return o2.f + j; - } - + [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly accessing a field on a null reference 'o2'. Are you making some assumption on MakeObj that the static checker is unaware of? ", PrimaryILOffset = 7, MethodILOffset = 0)] + public int Test2(Obj o1, int j) + { + Obj o2 = Obj.MakeObj(); + return o2.f + j; + } + #else - [RegressionOutcome("No entry found in the cache")] // can't find method by hash... - [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as field receiver)", PrimaryILOffset = 13, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly accessing a field on a null reference 'o1'", PrimaryILOffset = 20, MethodILOffset = 0)] - public int Test2(Obj o1, int j) - { - Obj o2 = Obj.MakeObj(); - j++; - return j + o2.f + o1.g; - } + [RegressionOutcome("No entry found in the cache")] // can't find method by hash... + [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as field receiver)", PrimaryILOffset = 13, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly accessing a field on a null reference 'o1'", PrimaryILOffset = 20, MethodILOffset = 0)] + public int Test2(Obj o1, int j) + { + Obj o2 = Obj.MakeObj(); + j++; + return j + o2.f + o1.g; + } #endif - // check if multiple variables in the assume() are hanlded correctly - [ClousotRegressionTest] + // check if multiple variables in the assume() are hanlded correctly + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on Obj.FooBar() that the static checker is unaware of? ",PrimaryILOffset=14,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possibly calling a method on a null reference 'b'",PrimaryILOffset=1,MethodILOffset=0)] - public int Test3(Obj b, int i) - { - int tmp = b.FooBar(); - Contract.Assert(tmp >= i); - return 7; - } - + [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on Obj.FooBar() that the static checker is unaware of? ", PrimaryILOffset = 14, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference 'b'", PrimaryILOffset = 1, MethodILOffset = 0)] + public int Test3(Obj b, int i) + { + int tmp = b.FooBar(); + Contract.Assert(tmp >= i); + return 7; + } + #else - [RegressionOutcome("No entry found in the cache")] // can't find method by hash... - [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=1,MethodILOffset=0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 20, MethodILOffset = 0)] - public int Test3(Obj b, int i) - { - int tmp = b.FooBar(); - int j = 0; - j++; - Contract.Assert(tmp >= i); - return 7; - } + [RegressionOutcome("No entry found in the cache")] // can't find method by hash... + [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 1, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 20, MethodILOffset = 0)] + public int Test3(Obj b, int i) + { + int tmp = b.FooBar(); + int j = 0; + j++; + Contract.Assert(tmp >= i); + return 7; + } #endif - // see if using a parameter as a return value is handled correctly - [ClousotRegressionTest] + // see if using a parameter as a return value is handled correctly + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly calling a method on a null reference 'b'", PrimaryILOffset = 3, MethodILOffset = 0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on FooBar that the static checker is unaware of? ",PrimaryILOffset=17,MethodILOffset=0)] - public int Test4(Obj b, int i) - { - int tmp = 2; - i = b.FooBar(); - Contract.Assert(tmp >= i); - return 7; - } - + [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly calling a method on a null reference 'b'", PrimaryILOffset = 3, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on FooBar that the static checker is unaware of? ", PrimaryILOffset = 17, MethodILOffset = 0)] + public int Test4(Obj b, int i) + { + int tmp = 2; + i = b.FooBar(); + Contract.Assert(tmp >= i); + return 7; + } + #else - [RegressionOutcome("No entry found in the cache")] // can't find method by hash... - [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=3,MethodILOffset=0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 23, MethodILOffset = 0)] - public int Test4(Obj b, int i) - { - int tmp = 2; - i = b.FooBar(); - int j = 0; - j++; - Contract.Assert(tmp >= i); - return 7; - } + [RegressionOutcome("No entry found in the cache")] // can't find method by hash... + [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 3, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 23, MethodILOffset = 0)] + public int Test4(Obj b, int i) + { + int tmp = 2; + i = b.FooBar(); + int j = 0; + j++; + Contract.Assert(tmp >= i); + return 7; + } #endif - // see if using a parameter as a return value is handled correctly - [ClousotRegressionTest] - [RegressionOutcome("No entry found in the cache")] + // see if using a parameter as a return value is handled correctly + [ClousotRegressionTest] + [RegressionOutcome("No entry found in the cache")] #if FIRST - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possibly calling a method on a null reference 'b' (Fixing this warning may solve one additional issue in the code)",PrimaryILOffset=7,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possibly calling a method on a null reference 'b'",PrimaryILOffset=16,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on FooBar that the static checker is unaware of? ",PrimaryILOffset=29,MethodILOffset=0)] - public int Test5(Obj b, int i) - { - int tmp = 2; - int x; - if (i > 0) { - x = b.FooBar(); - } - else { - x = b.FooBar(); + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference 'b' (Fixing this warning may solve one additional issue in the code)", PrimaryILOffset = 7, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference 'b'", PrimaryILOffset = 16, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on FooBar that the static checker is unaware of? ", PrimaryILOffset = 29, MethodILOffset = 0)] + public int Test5(Obj b, int i) + { + int tmp = 2; + int x; + if (i > 0) + { + x = b.FooBar(); + } + else + { + x = b.FooBar(); + } + Contract.Assert(tmp >= x); + return 7; } - Contract.Assert(tmp >= x); - return 7; - } - + #else - [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=7,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=16,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=33,MethodILOffset=0)] - public int Test5(Obj b, int i) - { - int tmp = 2; - int x; - if (i > 0) { - x = b.FooBar(); - } - else { - x = b.FooBar(); - x--; + [RegressionOutcome("Assumes have been found in the cache.")] // but do find assume's + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 7, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 16, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 33, MethodILOffset = 0)] + public int Test5(Obj b, int i) + { + int tmp = 2; + int x; + if (i > 0) + { + x = b.FooBar(); + } + else + { + x = b.FooBar(); + x--; + } + Contract.Assert(tmp >= x); + return 7; } - Contract.Assert(tmp >= x); - return 7; - } #endif - [ContractVerification(false)] - static int UnknownFunction(int z) - { - return System.Environment.TickCount; - } - - int a; - - [ClousotRegressionTest] - [RegressionOutcome("No entry found in the cache")] + [ContractVerification(false)] + private static int UnknownFunction(int z) + { + return System.Environment.TickCount; + } + + private int a; + + [ClousotRegressionTest] + [RegressionOutcome("No entry found in the cache")] #if FIRST - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on UnknownFunction that the static checker is unaware of? ",PrimaryILOffset=19,MethodILOffset=0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on UnknownFunction that the static checker is unaware of? ", PrimaryILOffset = 19, MethodILOffset = 0)] #else - [RegressionOutcome("Assumes have been found in the cache.")] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=19,MethodILOffset=0)] + [RegressionOutcome("Assumes have been found in the cache.")] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 19, MethodILOffset = 0)] #endif - public void TestLocal() - { - var i = 0; - - var local = UnknownFunction(i); - - if (local < 100) { - Contract.Assert(local > 10); + public void TestLocal() + { + var i = 0; + + var local = UnknownFunction(i); + + if (local < 100) + { + Contract.Assert(local > 10); + } } - } - [ClousotRegressionTest] - [RegressionOutcome("No entry found in the cache")] + [ClousotRegressionTest] + [RegressionOutcome("No entry found in the cache")] #if FIRST - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=9,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=15,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on UnknownFunction that the static checker is unaware of? ",PrimaryILOffset=31,MethodILOffset=0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 9, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 15, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on UnknownFunction that the static checker is unaware of? ", PrimaryILOffset = 31, MethodILOffset = 0)] #else - [RegressionOutcome("Assumes have been found in the cache.")] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=9,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=15,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=31,MethodILOffset=0)] + [RegressionOutcome("Assumes have been found in the cache.")] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 9, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 15, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 31, MethodILOffset = 0)] #endif - public void TestField() - { - var i = 0; - - this.a = UnknownFunction(i); - - var local = this.a; - - if (local < 100) { - Contract.Assert(local > 10); + public void TestField() + { + var i = 0; + + a = UnknownFunction(i); + + var local = a; + + if (local < 100) + { + Contract.Assert(local > 10); + } } - } - - int[] data; - [ClousotRegressionTest] - [RegressionOutcome("No entry found in the cache")] + private int[] data; + + [ClousotRegressionTest] + [RegressionOutcome("No entry found in the cache")] #if FIRST - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=10,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=16,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=28,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=30,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=36,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Array creation : ok",PrimaryILOffset=5,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=28,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=28,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=36,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=36,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven. Are you making some assumption on UnknownFunction that the static checker is unaware of? ",PrimaryILOffset=48,MethodILOffset=0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 10, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 16, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 28, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 30, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 36, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Array creation : ok", PrimaryILOffset = 5, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 28, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 28, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 36, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 36, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven. Are you making some assumption on UnknownFunction that the static checker is unaware of? ", PrimaryILOffset = 48, MethodILOffset = 0)] #else - [RegressionOutcome("Assumes have been found in the cache.")] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=10,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=16,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=28,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=30,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=36,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Array creation : ok",PrimaryILOffset=5,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=28,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=28,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=36,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=36,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=48,MethodILOffset=0)] + [RegressionOutcome("Assumes have been found in the cache.")] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 10, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 16, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 28, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 30, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 36, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Array creation : ok", PrimaryILOffset = 5, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 28, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 28, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 36, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 36, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 48, MethodILOffset = 0)] #endif - public void TestArray() - { - var i = 0; - this.data = new int[10]; - - this.data[5] = UnknownFunction(i); - - var local = this.data[5]; - - if (local < 100) { - Contract.Assert(local > 10); + public void TestArray() + { + var i = 0; + data = new int[10]; + + data[5] = UnknownFunction(i); + + var local = data[5]; + + if (local < 100) + { + Contract.Assert(local > 10); + } + } + + public void OtherFunc(int x) + { + Contract.Requires(x > 10); } - } - - public void OtherFunc(int x) { - Contract.Requires(x > 10); - } - - [ClousotRegressionTest] - [RegressionOutcome("No entry found in the cache")] + + [ClousotRegressionTest] + [RegressionOutcome("No entry found in the cache")] #if FIRST - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=9,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="requires unproven: x > 10",PrimaryILOffset=5,MethodILOffset=9)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 9, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "requires unproven: x > 10", PrimaryILOffset = 5, MethodILOffset = 9)] #else - [RegressionOutcome("Assumes have been found in the cache.")] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=9,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="requires is valid",PrimaryILOffset=5,MethodILOffset=9)] -#endif - public void TestChain() { - var i = 0; - - OtherFunc(UnknownFunction(i)); - - } - - [ContractVerification(false)] - static int RelationOnResult(out int[] array) - { - array = new int[10]; - return System.Environment.TickCount; - } - - [ClousotRegressionTest] - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("Assumes have been found in the cache.")] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 9, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 5, MethodILOffset = 9)] +#endif + public void TestChain() + { + var i = 0; + + OtherFunc(UnknownFunction(i)); + } + + [ContractVerification(false)] + private static int RelationOnResult(out int[] array) + { + array = new int[10]; + return System.Environment.TickCount; + } + + [ClousotRegressionTest] + [RegressionOutcome("No entry found in the cache")] #if FIRST - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possible use of a null array 'data'",PrimaryILOffset=11,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Array access might be below the lower bound. Are you making some assumption on RelationOnResult that the static checker is unaware of? ",PrimaryILOffset=11,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Array access might be above the upper bound. Are you making some assumption on Test.RelationOnResult(System.Int32[]@) that the static checker is unaware of? ",PrimaryILOffset=11,MethodILOffset=0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possible use of a null array 'data'", PrimaryILOffset = 11, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Array access might be below the lower bound. Are you making some assumption on RelationOnResult that the static checker is unaware of? ", PrimaryILOffset = 11, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Array access might be above the upper bound. Are you making some assumption on Test.RelationOnResult(System.Int32[]@) that the static checker is unaware of? ", PrimaryILOffset = 11, MethodILOffset = 0)] #else - [RegressionOutcome("Assumes have been found in the cache.")] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=11,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=11,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=11,MethodILOffset=0)] + [RegressionOutcome("Assumes have been found in the cache.")] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 11, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 11, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 11, MethodILOffset = 0)] #endif - public void TestRelation() { - - int[] data; - var i = RelationOnResult(out data); - - data[i] = 0; - } - -# else + public void TestRelation() + { + int[] data; + var i = RelationOnResult(out data); + + data[i] = 0; + } + +#else // if CCI2 // dummy test to prevent above tests from failing on CCI2 [ClousotRegressionTest] - #if FIRST +#if FIRST [RegressionOutcome("No entry found in the cache")] public void Dummy() { } - #else +#else [RegressionOutcome("An entry has been found in the cache")] public void Dummy() { } - #endif #endif - +#endif } diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Serialization.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Serialization.cs index 9c1654d3..63bb5ea9 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Serialization.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Serialization.cs @@ -1,141 +1,130 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Collections.Generic; using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -class Test +internal class Test { - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Type_Primitive() - { - Contract.Ensures(Contract.Result() == true); - return true; - } + private bool Type_Primitive() + { + Contract.Ensures(Contract.Result() == true); + return true; + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - object Type_Object() - { - Contract.Ensures(Contract.Result() != null); - return new Object(); - } + private object Type_Object() + { + Contract.Ensures(Contract.Result() != null); + return new Object(); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - T Type_FormalMethodParamter() - where T : new() - { - Contract.Ensures(Contract.Result() != null); - return new T(); - } - - [ClousotRegressionTest] + private T Type_FormalMethodParamter() + where T : new() + { + Contract.Ensures(Contract.Result() != null); + return new T(); + } + + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - int[] Type_Array() - { - Contract.Ensures(Contract.Result() != null); - return new int[0]; - } + private int[] Type_Array() + { + Contract.Ensures(Contract.Result() != null); + return new int[0]; + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - int[,,] Type_Array3() - { - Contract.Ensures(Contract.Result() != null); - return new int[0,0,0]; - } + private int[,,] Type_Array3() + { + Contract.Ensures(Contract.Result() != null); + return new int[0, 0, 0]; + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - List Type_Specialized() - { - Contract.Ensures(Contract.Result>() != null); - return new List(); - } - - class DummyClass - { - public class NestedClass + private List Type_Specialized() + { + Contract.Ensures(Contract.Result>() != null); + return new List(); + } + + private class DummyClass { - public object DummyField; + public class NestedClass + { + public object DummyField; + } } - } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - DummyClass.NestedClass Type_NestedType() - { - Contract.Ensures(Contract.Result() != null); - return new DummyClass.NestedClass(); - } + private DummyClass.NestedClass Type_NestedType() + { + Contract.Ensures(Contract.Result() != null); + return new DummyClass.NestedClass(); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - object Type_NestedType(DummyClass.NestedClass x) - { - Contract.Requires(x != null); - Contract.Ensures(Contract.Result() == x.DummyField); - return x.DummyField; - } - - [ClousotRegressionTest] + private object Type_NestedType(DummyClass.NestedClass x) + { + Contract.Requires(x != null); + Contract.Ensures(Contract.Result() == x.DummyField); + return x.DummyField; + } + + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Parameters(object x, object y) - { - Contract.Ensures(Contract.Result() == ((x == this) || (x == y))); - return x == this || x == y; - } + private bool Parameters(object x, object y) + { + Contract.Ensures(Contract.Result() == ((x == this) || (x == y))); + return x == this || x == y; + } } public class GenericClass @@ -143,73 +132,73 @@ public class GenericClass where C : class where T : class { - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - T Type_FormalTypeParameter() - { - Contract.Ensures(Contract.Result() == default(T)); - return default(T); - } + private T Type_FormalTypeParameter() + { + Contract.Ensures(Contract.Result() == default(T)); + return default(T); + } - [Pure] - C c(A a) { return a; } + [Pure] + private C c(A a) { return a; } - [Pure] - static C sc(A a) { return a; } + [Pure] + private static C sc(A a) { return a; } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Method_TypeArguments(A a, C c) - { - Contract.Ensures(Contract.Result() == (this.c(a) == c)); - return this.c(a) == c; - } + private bool Method_TypeArguments(A a, C c) + { + Contract.Ensures(Contract.Result() == (this.c(a) == c)); + return this.c(a) == c; + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Method_Static(A a, C c) - { - Contract.Ensures(Contract.Result() == (sc(a) == c)); - return sc(a) == c; - } + private bool Method_Static(A a, C c) + { + Contract.Ensures(Contract.Result() == (sc(a) == c)); + return sc(a) == c; + } - [Pure] - U f(bool b, U x) { return b ? x : default(U); } + [Pure] + private U f(bool b, U x) { return b ? x : default(U); } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - A Method_Specialized(bool b, A a) - { - Contract.Ensures(Contract.Result() == this.f(b, a)); - return this.f(b, a); - } + private A Method_Specialized(bool b, A a) + { + Contract.Ensures(Contract.Result() == this.f(b, a)); + return this.f(b, a); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - U Method_Generic(bool b, U u) - where U : class - { - Contract.Ensures(Contract.Result() == this.f(b, u)); - return this.f(b, u); - } + private U Method_Generic(bool b, U u) + where U : class + { + Contract.Ensures(Contract.Result() == this.f(b, u)); + return this.f(b, u); + } } diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SerializationInferred.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SerializationInferred.cs index da9cf08e..d55ff31c 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SerializationInferred.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/SerializationInferred.cs @@ -1,16 +1,5 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Collections.Generic; @@ -19,155 +8,154 @@ public class Test { - [ClousotRegressionTest] -[RegressionOutcome("Contract.Ensures(Contract.Result() == true);")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == true);")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Type_Primitive() - { - // Contract.Ensures(Contract.Result() == true); - return true; - } + private bool Type_Primitive() + { + // Contract.Ensures(Contract.Result() == true); + return true; + } - [ClousotRegressionTest] -[RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - object Type_Object() - { - // Contract.Ensures(Contract.Result() != null); - return new Object(); - } + private object Type_Object() + { + // Contract.Ensures(Contract.Result() != null); + return new Object(); + } - [ClousotRegressionTest] -// No inference from Clousot - TODO + [ClousotRegressionTest] + // No inference from Clousot - TODO #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - T Type_FormalMethodParamter() - where T : new() - { - // Contract.Ensures(Contract.Result() != null); - return new T(); - } + private T Type_FormalMethodParamter() + where T : new() + { + // Contract.Ensures(Contract.Result() != null); + return new T(); + } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] - [RegressionOutcome("Contract.Ensures(Contract.Result().Length == 0);")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] + [RegressionOutcome("Contract.Ensures(Contract.Result().Length == 0);")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - int[] Type_Array() - { - // Contract.Ensures(Contract.Result() != null); - return new int[0]; - } + private int[] Type_Array() + { + // Contract.Ensures(Contract.Result() != null); + return new int[0]; + } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - int[,,] Type_Array3() - { - // Contract.Ensures(Contract.Result() != null); - return new int[0,0,0]; - } + private int[,,] Type_Array3() + { + // Contract.Ensures(Contract.Result() != null); + return new int[0, 0, 0]; + } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result>() != null);")] - [RegressionOutcome("Contract.Ensures(Contract.Result>().Count == 0);")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result>() != null);")] + [RegressionOutcome("Contract.Ensures(Contract.Result>().Count == 0);")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - List Type_Specialized() - { - // Contract.Ensures(Contract.Result>() != null); - return new List(); - } + private List Type_Specialized() + { + // Contract.Ensures(Contract.Result>() != null); + return new List(); + } - public class DummyClass - { - public class NestedClass + public class DummyClass { - public object DummyField; + public class NestedClass + { + public object DummyField; + } } - } - [ClousotRegressionTest] -#if !CLOUSOT2 -[RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] + [ClousotRegressionTest] +#if !CLOUSOT2 + [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] #else [RegressionOutcome("Contract.Ensures(Contract.Result() != null);")] #endif #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - DummyClass.NestedClass Type_NestedType() - { - // Contract.Ensures(Contract.Result() != null); - return new DummyClass.NestedClass(); - } + private DummyClass.NestedClass Type_NestedType() + { + // Contract.Ensures(Contract.Result() != null); + return new DummyClass.NestedClass(); + } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Requires(x != null);")] - [RegressionOutcome("Contract.Ensures(Contract.Result() == x.DummyField);")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Requires(x != null);")] + [RegressionOutcome("Contract.Ensures(Contract.Result() == x.DummyField);")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - public object Type_NestedType(DummyClass.NestedClass x) - { - // Contract.Requires(x != null); - // Contract.Ensures(Contract.Result() == x.DummyField); - return x.DummyField; - } + public object Type_NestedType(DummyClass.NestedClass x) + { + // Contract.Requires(x != null); + // Contract.Ensures(Contract.Result() == x.DummyField); + return x.DummyField; + } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == (((Test)(x)) == this));")] - // [RegressionOutcome("Contract.Ensures(Contract.Result() == (x == this));")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == (((Test)(x)) == this));")] + // [RegressionOutcome("Contract.Ensures(Contract.Result() == (x == this));")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Parameters1(object x, object y) - { - // Contract.Ensures(Contract.Result() == ((x == this))); - return x == this; - } + private bool Parameters1(object x, object y) + { + // Contract.Ensures(Contract.Result() == ((x == this))); + return x == this; + } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == (x == y));")] + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == (x == y));")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Parameters2(object x, object y) - { - // Contract.Ensures(Contract.Result() == ((x == y) )); - return x == y; - } - + private bool Parameters2(object x, object y) + { + // Contract.Ensures(Contract.Result() == ((x == y) )); + return x == y; + } } public class GenericClass @@ -175,94 +163,94 @@ public class GenericClass where C : class where T : class { - // nothing (default) - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == null);")] + // nothing (default) + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == null);")] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - T Type_FormalTypeParameter() - { - // Contract.Ensures(Contract.Result() == default(T)); - return default(T); - } + private T Type_FormalTypeParameter() + { + // Contract.Ensures(Contract.Result() == default(T)); + return default(T); + } - // nothing (default) - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == null);")] + // nothing (default) + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == null);")] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - T Type_FormalTypeParameterResultNull() - { - // Contract.Ensures(Contract.Result() == null); - return null; - } + private T Type_FormalTypeParameterResultNull() + { + // Contract.Ensures(Contract.Result() == null); + return null; + } - [Pure] - C c(A a) { return a; } + [Pure] + private C c(A a) { return a; } - [Pure] - static C sc(A a) { return a; } + [Pure] + private static C sc(A a) { return a; } - [ClousotRegressionTest] - // method call + [ClousotRegressionTest] + // method call #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Method_TypeArguments(A a, C c) - { - // Contract.Ensures(Contract.Result() == (this.c(a) == c)); - return this.c(a) == c; - } + private bool Method_TypeArguments(A a, C c) + { + // Contract.Ensures(Contract.Result() == (this.c(a) == c)); + return this.c(a) == c; + } - [ClousotRegressionTest] -// TODO: fix the Output of the postcondition, because GenericClass takes 4 arguments -//[RegressionOutcome("Contract.Ensures(Contract.Result() == (GenericClass.sc(a) == c));")] - [RegressionOutcome("Contract.Ensures(Contract.Result() == (GenericClass.sc(a).Equals(c)));")] + [ClousotRegressionTest] + // TODO: fix the Output of the postcondition, because GenericClass takes 4 arguments + //[RegressionOutcome("Contract.Ensures(Contract.Result() == (GenericClass.sc(a) == c));")] + [RegressionOutcome("Contract.Ensures(Contract.Result() == (GenericClass.sc(a).Equals(c)));")] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - bool Method_Static(A a, C c) - { - // Contract.Ensures(Contract.Result() == (sc(a) == c)); - return sc(a) == c; - } + private bool Method_Static(A a, C c) + { + // Contract.Ensures(Contract.Result() == (sc(a) == c)); + return sc(a) == c; + } - [Pure] - U f(bool b, U x) { return b ? x : default(U); } + [Pure] + private U f(bool b, U x) { return b ? x : default(U); } - [ClousotRegressionTest] - // generics + [ClousotRegressionTest] + // generics #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - A Method_Specialized(bool b, A a) - { - // Contract.Ensures(Contract.Result() == this.f(b, a)); - return this.f(b, a); - } + private A Method_Specialized(bool b, A a) + { + // Contract.Ensures(Contract.Result() == this.f(b, a)); + return this.f(b, a); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - U Method_Generic(bool b, U u) - where U : class - { - // Contract.Ensures(Contract.Result() == this.f(b, u)); - return this.f(b, u); - } + private U Method_Generic(bool b, U u) + where U : class + { + // Contract.Ensures(Contract.Result() == this.f(b, u)); + return this.f(b, u); + } } diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test.cs index cc7604c3..ed463176 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test.cs @@ -1,130 +1,100 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -class Test +internal class Test { - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - void F() - { - Console.WriteLine("Hello"); - } + private void F() + { + Console.WriteLine("Hello"); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 13, MethodILOffset = 0)] - void Fx(int x) // With outcome - { - F(); - Contract.Assert(x != 0); - Console.WriteLine("{0}", x); - } - - [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 13, MethodILOffset = 0)] + private void Fx(int x) // With outcome + { + F(); + Contract.Assert(x != 0); + Console.WriteLine("{0}", x); + } + + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"ensures unproven: Contract.Result() != null", PrimaryILOffset = 11, MethodILOffset = 17)] - object Fo(object o) // With suggestion - { - Contract.Ensures(Contract.Result() != null); + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"ensures unproven: Contract.Result() != null", PrimaryILOffset = 11, MethodILOffset = 17)] + private object Fo(object o) // With suggestion + { + Contract.Ensures(Contract.Result() != null); - return o; - } + return o; + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - void UseFo() // We try to use the non-null post condition inference - { - object o = Fo(1); - Contract.Assert(o != null); - } + private void UseFo() // We try to use the non-null post condition inference + { + object o = Fo(1); + Contract.Assert(o != null); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - object G0(object o) - { - Contract.Requires(o != null); + private object G0(object o) + { + Contract.Requires(o != null); - return o; - } + return o; + } - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] -#else - [RegressionOutcome("An entry has been found in the cache")] -#endif - void G() // With requires imported from another method, and an imported infered ensure - { - object o = G0(0); - Contract.Assert(o != null); - } - - // We now know how to cache pre/prost-conditions inferences - int P - { [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else [RegressionOutcome("An entry has been found in the cache")] #endif - get { return 1; } - } + private void G() // With requires imported from another method, and an imported infered ensure + { + object o = G0(0); + Contract.Assert(o != null); + } - [ClousotRegressionTest] + // We now know how to cache pre/prost-conditions inferences + private int P + { + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly unboxing a null reference", PrimaryILOffset = 28, MethodILOffset = 0)] - public static T GetService(IServiceProvider serviceProvider) - { - Contract.Requires(serviceProvider != null); - return (T)serviceProvider.GetService(typeof(T)); - } -} - -namespace CacheBugs -{ - public class ExampleWithPure - { - public object field; + get + { return 1; } + } [ClousotRegressionTest] #if FIRST @@ -132,154 +102,174 @@ public class ExampleWithPure #else [RegressionOutcome("An entry has been found in the cache")] #endif - [RegressionOutcome(Outcome=ProofOutcome.Top,Message=@"assert unproven",PrimaryILOffset=35,MethodILOffset=0)] - public void Use() + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"Possibly unboxing a null reference", PrimaryILOffset = 28, MethodILOffset = 0)] + public static T GetService(IServiceProvider serviceProvider) { - Contract.Assume(field != null); - - IAmPure(); - - Contract.Assert(field != null); + Contract.Requires(serviceProvider != null); + return (T)serviceProvider.GetService(typeof(T)); } - - public void IAmPure() +} + +namespace CacheBugs +{ + public class ExampleWithPure { - } - } + public object field; - public class ExamplesWithPure - { - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - public string PureMethod(object x) - { - Contract.Requires(x != null); - return x.ToString(); + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 35, MethodILOffset = 0)] + public void Use() + { + Contract.Assume(field != null); + + IAmPure(); + + Contract.Assert(field != null); + } + + public void IAmPure() + { + } } - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] + public class ExamplesWithPure + { + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - public string PureParameter(object[] x) - { - Contract.Requires(x != null); - return x.ToString(); - } - - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] + public string PureMethod(object x) + { + Contract.Requires(x != null); + return x.ToString(); + } + + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - public void CallPureParameter(object[] x) - { - Contract.Requires(x != null); - PureParameter(x); + public string PureParameter(object[] x) + { + Contract.Requires(x != null); + return x.ToString(); + } + + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] +#else + [RegressionOutcome("An entry has been found in the cache")] +#endif + public void CallPureParameter(object[] x) + { + Contract.Requires(x != null); + PureParameter(x); + } } - } } // For the tests below, Clousot2 was seeing the three occurrences of M as the same method, so it analyzed the first one, and read the other two from the cache. // The reason is that the generics were not in the Full name namespace CacheBugsWithClousot2 { - class C - { - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven",PrimaryILOffset=4,MethodILOffset=0)] -#if FIRST - [RegressionOutcome("No entry found in the cache")] + internal class C + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven", PrimaryILOffset = 4, MethodILOffset = 0)] +#if FIRST + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - void M(int x) - { - Contract.Assert(x > 0); + private void M(int x) + { + Contract.Assert(x > 0); + } } - } - - class C - { - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven",PrimaryILOffset=4,MethodILOffset=0)] -#if FIRST - [RegressionOutcome("No entry found in the cache")] + + internal class C + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven", PrimaryILOffset = 4, MethodILOffset = 0)] +#if FIRST + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - void M(int x) - { - Contract.Assert(x > 0); - } - } - class C - { - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven",PrimaryILOffset=4,MethodILOffset=0)] -#if FIRST - [RegressionOutcome("No entry found in the cache")] + private void M(int x) + { + Contract.Assert(x > 0); + } + } + internal class C + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven", PrimaryILOffset = 4, MethodILOffset = 0)] +#if FIRST + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - void M(int x) - { - Contract.Assert(x > 0); - } - } - + private void M(int x) + { + Contract.Assert(x > 0); + } + } + public class TryLambda - { - delegate TResult MyFunc(T arg); - - [ClousotRegressionTest] + { + private delegate TResult MyFunc(T arg); + + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif - public int SomeLambda(string mystr) - { - MyFunc lengthPlusTwo = (string s) => (s.Length + 2); + [RegressionOutcome("An entry has been found in the cache")] +#endif + public int SomeLambda(string mystr) + { + MyFunc lengthPlusTwo = (string s) => (s.Length + 2); - return lengthPlusTwo(mystr); + return lengthPlusTwo(mystr); + } } - } } namespace WithReadonly { - public class ReadonlyTest - { - string field; // not readonly - + public class ReadonlyTest + { + private string field; // not readonly + #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif - public ReadonlyTest(string s) - { - this.field = s; - } - + [RegressionOutcome("An entry has been found in the cache")] +#endif + public ReadonlyTest(string s) + { + this.field = s; + } + #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif - public string DoSomething() - { - return this.field; - } - } + [RegressionOutcome("An entry has been found in the cache")] +#endif + public string DoSomething() + { + return this.field; + } + } } namespace EnumValues @@ -295,12 +285,12 @@ static public Exception FailedAssertion() } public class Foo { - public enum MyEnum { One, Two, Three, Quattro}; + public enum MyEnum { One, Two, Three, Quattro }; #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif public int Test(MyEnum e) { @@ -326,6 +316,5 @@ public int Test(MyEnum e) return i; } - - } + } } \ No newline at end of file diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test2.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test2.cs index ec7c8eba..0eed5ad5 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test2.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/Test2.cs @@ -1,100 +1,32 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -class Test +internal class Test { - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] -#else - [RegressionOutcome("An entry has been found in the cache")] -#endif - void F() // We want to reanalyse - { - Console.WriteLine("Hello2"); - } - - [ClousotRegressionTest] - [RegressionOutcome("An entry has been found in the cache")] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 13, MethodILOffset = 0)] - void Fx(int x) // We do not want to reanalyse, even if F has changed. We find Fx in the cache from analyzing the prior test Test.cs - { - F(); - Contract.Assert(x != 0); - Console.WriteLine("{0}", x); - } - - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] -#else - [RegressionOutcome("An entry has been found in the cache")] -#endif - object Fo(object o) // We change the ensure to a requires (so we test the post condition suggestion) - { - Contract.Requires(o != null); - - return o; - } - - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] -#else - [RegressionOutcome("An entry has been found in the cache")] -#endif - object G0(object o) - { - return o; - } - - [ClousotRegressionTest] -#if FIRST - [RegressionOutcome("No entry found in the cache")] -#else - [RegressionOutcome("An entry has been found in the cache")] -#endif - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven",PrimaryILOffset=20,MethodILOffset=0)] - void G() // We want to reanalyse as contracts for G0 have changed - { - object o = G0(0); - Contract.Assert(o != null); - } - - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - public static T GetService(IServiceProvider serviceProvider) - where T : class - { - Contract.Requires(serviceProvider != null); - return (T)serviceProvider.GetService(typeof(T)); - } -} + private void F() // We want to reanalyse + { + Console.WriteLine("Hello2"); + } -namespace CacheBugs -{ - public class ExampleWithPure - { - public object field; + [ClousotRegressionTest] + [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 13, MethodILOffset = 0)] + private void Fx(int x) // We do not want to reanalyse, even if F has changed. We find Fx in the cache from analyzing the prior test Test.cs + { + F(); + Contract.Assert(x != 0); + Console.WriteLine("{0}", x); + } [ClousotRegressionTest] #if FIRST @@ -102,125 +34,180 @@ public class ExampleWithPure #else [RegressionOutcome("An entry has been found in the cache")] #endif - // no warning - public void Use() + private object Fo(object o) // We change the ensure to a requires (so we test the post condition suggestion) { - Contract.Assume(field != null); - - IAmPure(); + Contract.Requires(o != null); - Contract.Assert(field != null); - } - - [Pure] - public void IAmPure() - { + return o; } - } - public class ExamplesWithPure - { [ClousotRegressionTest] #if FIRST [RegressionOutcome("No entry found in the cache")] #else [RegressionOutcome("An entry has been found in the cache")] #endif - [Pure] // This time it is pure, so we should not find the one defined in Test1 - public string PureMethod(object x) + private object G0(object o) { - Contract.Requires(x != null); - return x.ToString(); + return o; } [ClousotRegressionTest] -#if FIRST +#if FIRST [RegressionOutcome("No entry found in the cache")] #else [RegressionOutcome("An entry has been found in the cache")] #endif - // this time the parameter is pure, so we should hash again - public string PureParameter([Pure] object[] x) + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven", PrimaryILOffset = 20, MethodILOffset = 0)] + private void G() // We want to reanalyse as contracts for G0 have changed { - Contract.Requires(x != null); - return x.ToString(); + object o = G0(0); + Contract.Assert(o != null); } [ClousotRegressionTest] -#if FIRST +#if FIRST [RegressionOutcome("No entry found in the cache")] #else [RegressionOutcome("An entry has been found in the cache")] #endif - public void CallPureParameter(object[] x) + public static T GetService(IServiceProvider serviceProvider) + where T : class { - Contract.Requires(x != null); - PureParameter(x); + Contract.Requires(serviceProvider != null); + return (T)serviceProvider.GetService(typeof(T)); } - } - - public class TryLambda - { - - delegate TResult MyFunc(T arg); - - [ClousotRegressionTest] +} + +namespace CacheBugs +{ + public class ExampleWithPure + { + public object field; + + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif + [RegressionOutcome("An entry has been found in the cache")] +#endif + // no warning + public void Use() + { + Contract.Assume(field != null); - public int SomeLambda2(string mystr) - { - MyFunc lengthPlusTwoSecond = (string s) => (s.Length + 2); + IAmPure(); - return lengthPlusTwoSecond(mystr); + Contract.Assert(field != null); + } + + [Pure] + public void IAmPure() + { + } } - - // We should find it in the cache - [ClousotRegressionTest] + + public class ExamplesWithPure + { + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif - public int SomeLambda(string mystr) - { - MyFunc lengthPlusTwo = (string s) => (s.Length + 2); + [RegressionOutcome("An entry has been found in the cache")] +#endif + [Pure] // This time it is pure, so we should not find the one defined in Test1 + public string PureMethod(object x) + { + Contract.Requires(x != null); + return x.ToString(); + } + + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] +#else + [RegressionOutcome("An entry has been found in the cache")] +#endif + // this time the parameter is pure, so we should hash again + public string PureParameter([Pure] object[] x) + { + Contract.Requires(x != null); + return x.ToString(); + } - return lengthPlusTwo(mystr); + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] +#else + [RegressionOutcome("An entry has been found in the cache")] +#endif + public void CallPureParameter(object[] x) + { + Contract.Requires(x != null); + PureParameter(x); + } } - } + public class TryLambda + { + private delegate TResult MyFunc(T arg); + + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] +#else + [RegressionOutcome("An entry has been found in the cache")] +#endif + + public int SomeLambda2(string mystr) + { + MyFunc lengthPlusTwoSecond = (string s) => (s.Length + 2); + + return lengthPlusTwoSecond(mystr); + } + + // We should find it in the cache + [ClousotRegressionTest] +#if FIRST + [RegressionOutcome("No entry found in the cache")] +#else + [RegressionOutcome("An entry has been found in the cache")] +#endif + public int SomeLambda(string mystr) + { + MyFunc lengthPlusTwo = (string s) => (s.Length + 2); + + return lengthPlusTwo(mystr); + } + } } namespace WithReadonly { - public class ReadonlyTest - { - readonly string field; // now we marked it readonly! - + public class ReadonlyTest + { + private readonly string field; // now we marked it readonly! + #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif - public ReadonlyTest(string s) - { - this.field = s; - } - + [RegressionOutcome("An entry has been found in the cache")] +#endif + public ReadonlyTest(string s) + { + this.field = s; + } + #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] -#endif - public string DoSomething() - { - return this.field; - } - } + [RegressionOutcome("An entry has been found in the cache")] +#endif + public string DoSomething() + { + return this.field; + } + } } namespace EnumValues @@ -237,16 +224,15 @@ static public Exception FailedAssertion() public class Foo { - public enum MyEnum { One, Two, Three, Quattro}; // Added one case!!! + public enum MyEnum { One, Two, Three, Quattro }; // Added one case!!! #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif public int Test(MyEnum e) { - var i = 0; switch (e) @@ -269,6 +255,5 @@ public int Test(MyEnum e) return i; } - - } + } } \ No newline at end of file diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/TestQuantifiers.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/TestQuantifiers.cs index 03853b83..aa46e64c 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/TestQuantifiers.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Sources/TestQuantifiers.cs @@ -1,60 +1,49 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace Quantifiers { - public class ExampleWithForAll - { - [ClousotRegressionTest] +namespace Quantifiers +{ + public class ExampleWithForAll + { + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("No entry found in the cache")] // it should not be found - [RegressionOutcome(Outcome=ProofOutcome.False,Message=@"assert is false",PrimaryILOffset=91,MethodILOffset=0)] + [RegressionOutcome("No entry found in the cache")] // it should not be found + [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"assert is false", PrimaryILOffset = 91, MethodILOffset = 0)] #endif - // no warning - public void UseIncorrect(string[] array) - { - Contract.Requires(array != null); - Contract.Requires(array.Length > 0); + // no warning + public void UseIncorrect(string[] array) + { + Contract.Requires(array != null); + Contract.Requires(array.Length > 0); #if FIRST - Contract.Requires(Contract.ForAll(0, array.Length, i => array[i] != null)); + Contract.Requires(Contract.ForAll(0, array.Length, i => array[i] != null)); #else - Contract.Requires(Contract.ForAll(0, array.Length, i => array[i] == null)); + Contract.Requires(Contract.ForAll(0, array.Length, i => array[i] == null)); #endif - Contract.Assert(array[0] != null); - } + Contract.Assert(array[0] != null); + } - [ClousotRegressionTest] + [ClousotRegressionTest] #if FIRST - [RegressionOutcome("No entry found in the cache")] + [RegressionOutcome("No entry found in the cache")] #else - [RegressionOutcome("An entry has been found in the cache")] + [RegressionOutcome("An entry has been found in the cache")] #endif - // no warning - public void UseCorrect(string[] array) - { - Contract.Requires(array != null); - Contract.Requires(array.Length > 0); - Contract.Requires(Contract.ForAll(0, array.Length, i => array[i] != null)); + // no warning + public void UseCorrect(string[] array) + { + Contract.Requires(array != null); + Contract.Requires(array.Length > 0); + Contract.Requires(Contract.ForAll(0, array.Length, i => array[i] != null)); - Contract.Assert(array[0] != null); + Contract.Assert(array[0] != null); + } } - - } } diff --git a/Microsoft.Research/RegressionTest/ClousotCacheTests/Tests.cs b/Microsoft.Research/RegressionTest/ClousotCacheTests/Tests.cs index 55a1b590..1d69cfee 100644 --- a/Microsoft.Research/RegressionTest/ClousotCacheTests/Tests.cs +++ b/Microsoft.Research/RegressionTest/ClousotCacheTests/Tests.cs @@ -1,16 +1,5 @@ -// CodeContracts -// -// Copyright (c) Microsoft Corporation -// -// All rights reserved. -// -// MIT License -// -// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: -// -// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// Copyright (c) Microsoft. All rights reserved. +// Licensed under the MIT license. See LICENSE file in the project root for full license information. using System; using ClousotTests; @@ -18,153 +7,151 @@ namespace Tests { - /// - /// Summary description for RewriterTests - /// - [TestClass] - public class ClousotCacheTests - { - public ClousotCacheTests() - { - // - // TODO: Add constructor logic here - // - } - - private TestContext testContextInstance; - /// - ///Gets or sets the test context which provides - ///information about and functionality for the current test run. - /// - public TestContext TestContext - { - get - { - return testContextInstance; - } - set - { - testContextInstance = value; - } - } - - #region Additional test attributes - // - // You can use the following additional attributes as you write your tests: - // - // Use ClassInitialize to run code before running the first test in the class - // [ClassInitialize()] - // public static void MyClassInitialize(TestContext testContext) { } - // - // Use ClassCleanup to run code after all tests in a class have run - // [ClassCleanup()] - // public static void MyClassCleanup() { } - // - // Use TestInitialize to run code before running each test - // [TestInitialize()] - // public void MyTestInitialize() { } - // - //Use TestCleanup to run code after each test has run - [TestCleanup()] - public void MyTestCleanup() - { - if (TestContext.CurrentTestOutcome != UnitTestOutcome.Passed && CurrentGroupInfo != null && !System.Diagnostics.Debugger.IsAttached) - { - // record failing case - CurrentGroupInfo.WriteFailure(); - } - } - #endregion - - [TestCategory("StaticChecker"), TestCategory("Clousot1")] - [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] - [TestMethod] - public void Analyze1FromSourcesV35Cache() - { - var options = GrabTestOptions("Analyze1FromSourcesV35Cache"); - options.BuildFramework = @"v3.5"; - options.ContractFramework = @"v3.5"; - if (!options.Skip) - TestDriver.BuildAndAnalyze(options); - } - - [TestCategory("StaticChecker"), TestCategory("Clousot2"), TestCategory("Cache")] - [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] - [TestMethod] - public void Analyze2FromSourcesV35Cache() - { - var options = GrabTestOptions("Analyze2FromSourcesV35Cache"); - options.BuildFramework = @"v3.5"; - options.ContractFramework = @"v3.5"; - if (!options.Skip) - TestDriver.BuildAndAnalyze2(options); - } - - [TestCategory("StaticChecker"), TestCategory("Clousot1"), TestCategory("Cache")] - [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] - [TestMethod] - public void Analyze1FromSourcesV40Cache() - { - var options = GrabTestOptions("Analyze1FromSourcesV40Cache"); - options.BuildFramework = @".NETFramework\v4.0"; - options.ContractFramework = @".NETFramework\v4.0"; - if (!options.Skip) - TestDriver.BuildAndAnalyze(options); - } - - [TestCategory("StaticChecker"), TestCategory("Clousot1"), TestCategory("Cache")] - [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] - [TestMethod] - public void Analyze1FromSourcesV40AgainstV35ContractsCache() - { - var options = GrabTestOptions("Analyze1FromSourcesV40AgainstV35ContractsCache"); - options.BuildFramework = @".NETFramework\v4.0"; - options.ContractFramework = @"v3.5"; - if (!options.Skip) - TestDriver.BuildAndAnalyze(options); - } - - [TestCategory("StaticChecker"), TestCategory("Clousot2"), TestCategory("Service"), TestCategory("Cache")] - [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] - [TestMethod] - public void Analyze2ServiceSequentialFromSourcesV40Cache() + /// Summary description for RewriterTests + /// + [TestClass] + public class ClousotCacheTests { - var options = GrabTestOptions("Analyze2ServiceSequentialFromSourcesV40Cache"); - options.BuildFramework = @".NETFramework\v4.0"; - options.ContractFramework = @".NETFramework\v4.0"; - if (!options.Skip) - TestDriver.BuildAndAnalyze2S(options); + public ClousotCacheTests() + { + // + // TODO: Add constructor logic here + // + } + + private TestContext testContextInstance; + + /// + ///Gets or sets the test context which provides + ///information about and functionality for the current test run. + /// + public TestContext TestContext + { + get + { + return testContextInstance; + } + set + { + testContextInstance = value; + } + } + + #region Additional test attributes + // + // You can use the following additional attributes as you write your tests: + // + // Use ClassInitialize to run code before running the first test in the class + // [ClassInitialize()] + // public static void MyClassInitialize(TestContext testContext) { } + // + // Use ClassCleanup to run code after all tests in a class have run + // [ClassCleanup()] + // public static void MyClassCleanup() { } + // + // Use TestInitialize to run code before running each test + // [TestInitialize()] + // public void MyTestInitialize() { } + // + //Use TestCleanup to run code after each test has run + [TestCleanup()] + public void MyTestCleanup() + { + if (TestContext.CurrentTestOutcome != UnitTestOutcome.Passed && CurrentGroupInfo != null && !System.Diagnostics.Debugger.IsAttached) + { + // record failing case + CurrentGroupInfo.WriteFailure(); + } + } + #endregion + + [TestCategory("StaticChecker"), TestCategory("Clousot1")] + [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] + [TestMethod] + public void Analyze1FromSourcesV35Cache() + { + var options = GrabTestOptions("Analyze1FromSourcesV35Cache"); + options.BuildFramework = @"v3.5"; + options.ContractFramework = @"v3.5"; + if (!options.Skip) + TestDriver.BuildAndAnalyze(options); + } + + [TestCategory("StaticChecker"), TestCategory("Clousot2"), TestCategory("Cache")] + [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] + [TestMethod] + public void Analyze2FromSourcesV35Cache() + { + var options = GrabTestOptions("Analyze2FromSourcesV35Cache"); + options.BuildFramework = @"v3.5"; + options.ContractFramework = @"v3.5"; + if (!options.Skip) + TestDriver.BuildAndAnalyze2(options); + } + + [TestCategory("StaticChecker"), TestCategory("Clousot1"), TestCategory("Cache")] + [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] + [TestMethod] + public void Analyze1FromSourcesV40Cache() + { + var options = GrabTestOptions("Analyze1FromSourcesV40Cache"); + options.BuildFramework = @".NETFramework\v4.0"; + options.ContractFramework = @".NETFramework\v4.0"; + if (!options.Skip) + TestDriver.BuildAndAnalyze(options); + } + + [TestCategory("StaticChecker"), TestCategory("Clousot1"), TestCategory("Cache")] + [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] + [TestMethod] + public void Analyze1FromSourcesV40AgainstV35ContractsCache() + { + var options = GrabTestOptions("Analyze1FromSourcesV40AgainstV35ContractsCache"); + options.BuildFramework = @".NETFramework\v4.0"; + options.ContractFramework = @"v3.5"; + if (!options.Skip) + TestDriver.BuildAndAnalyze(options); + } + + [TestCategory("StaticChecker"), TestCategory("Clousot2"), TestCategory("Service"), TestCategory("Cache")] + [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] + [TestMethod] + public void Analyze2ServiceSequentialFromSourcesV40Cache() + { + var options = GrabTestOptions("Analyze2ServiceSequentialFromSourcesV40Cache"); + options.BuildFramework = @".NETFramework\v4.0"; + options.ContractFramework = @".NETFramework\v4.0"; + if (!options.Skip) + TestDriver.BuildAndAnalyze2S(options); + } + + [TestCategory("StaticChecker"), TestCategory("Clousot2"), TestCategory("Service"), TestCategory("Cache"), TestCategory("Short")] + [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] + [TestMethod] + public void Analyze2FastSequentialFromSourcesV40Cache() + { + var options = GrabTestOptions("Analyze2FastSequentialFromSourcesV40Cache"); + options.BuildFramework = @".NETFramework\v4.0"; + options.ContractFramework = @".NETFramework\v4.0"; + options.Fast = true; + if (!options.Skip) + TestDriver.BuildAndAnalyze2(options); + } + + [AssemblyCleanup] // Automatically called at the end of ClousotCacheTests + public static void AssemblyCleanup() + { + TestDriver.Cleanup(); + } + + private Options GrabTestOptions(string testGroupName) + { + var options = new Options(testGroupName, TestContext); + CurrentGroupInfo = options.Group; + return options; + } + + private static GroupInfo CurrentGroupInfo; } - - [TestCategory("StaticChecker"), TestCategory("Clousot2"), TestCategory("Service"), TestCategory("Cache"), TestCategory("Short")] - [DeploymentItem(@"Microsoft.Research\RegressionTest\ClousotCacheTests\ClousotCacheTestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\ClousotCacheTestInputs.xml", "TestRun", DataAccessMethod.Sequential)] - [TestMethod] - public void Analyze2FastSequentialFromSourcesV40Cache() - { - var options = GrabTestOptions("Analyze2FastSequentialFromSourcesV40Cache"); - options.BuildFramework = @".NETFramework\v4.0"; - options.ContractFramework = @".NETFramework\v4.0"; - options.Fast = true; - if (!options.Skip) - TestDriver.BuildAndAnalyze2(options); - } - - [AssemblyCleanup] // Automatically called at the end of ClousotCacheTests - public static void AssemblyCleanup() - { - TestDriver.Cleanup(); - } - - private Options GrabTestOptions(string testGroupName) - { - var options = new Options(testGroupName, TestContext); - CurrentGroupInfo = options.Group; - return options; - } - - static GroupInfo CurrentGroupInfo; - - } - }