2008-02-15 Sebastien Pouliot <sebastien@ximian.com>

	* AvoidConstructorsInStaticTypesRule.cs
	* BadRecursiveInvocationRule.cs
	* CallingEqualsWithNullArgRule.cs
	* DontCompareWithNaNRule.cs
	* FloatComparisonRule.cs
	* MethodCanBeMadeStaticRule.cs
	* NullDerefAnalysis.cs
	* NullDerefFrame.cs
	* NullDerefRule.cs
	* Nullity.cs
	* UseValueInPropertySetterRule.cs:
		Update rules wrt framework changes.


svn path=/trunk/mono-tools/; revision=95783

12 files changed, 1012 insertions, 1065 deletions

diff --git a/gendarme/rules/Gendarme.Rules.Correctness/AvoidConstructorsInStaticTypesRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/AvoidConstructorsInStaticTypesRule.cs
index a157e7ed..28cbc091 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/AvoidConstructorsInStaticTypesRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/AvoidConstructorsInStaticTypesRule.cs
@@ -6,7 +6,7 @@
 //	Sebastien Pouliot <sebastien@ximian.com>
 //
 // Copyright (C) 2007 Lukasz Knop
-// Copyright (C) 2007 Novell, Inc (http://www.novell.com)
+// Copyright (C) 2007-2008 Novell, Inc (http://www.novell.com)
 //
 // Permission is hereby granted, free of charge, to any person obtaining
 // a copy of this software and associated documentation files (the
@@ -37,46 +37,41 @@ using Gendarme.Framework.Rocks;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class AvoidConstructorsInStaticTypesRule : ITypeRule {
+	[Problem ("This type contains only static fields and methods and have a non static constructor.")]
+	[Solution ("You should use an static constructor or make the fields and methods non-static.")]
+	public class AvoidConstructorsInStaticTypesRule : Rule, ITypeRule {
 
-		private const string MessageString = "Types with no instance fields or methods should not have public instance constructors";
-
-		public MessageCollection CheckType (TypeDefinition type, Runner runner)
+		public RuleResult CheckType (TypeDefinition type)
 		{
 			// rule applies only if the type as method or fields
 			if (type.Methods.Count == 0 && type.Fields.Count == 0)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// rule applies only if all methods are static
 			foreach (MethodDefinition method in type.Methods) {
 				if (!method.IsStatic)
-					return runner.RuleSuccess;
+					return RuleResult.DoesNotApply;
 			}
 
 			// rule applies only if all fields are static
 			foreach (FieldDefinition field in type.Fields) {
 				if (!field.IsStatic)
-					return runner.RuleSuccess;
+					return RuleResult.DoesNotApply;
 			}
 
 			// rule applies only if the type isn't compiler generated
 			if (type.IsGeneratedCode ())
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// rule applies!
-			MessageCollection mc = null;
+
 			foreach (MethodDefinition ctor in type.Constructors) {
 				if (!ctor.IsStatic && ctor.IsPublic) {
-					Location location = new Location (ctor);
-					Message message = new Message(MessageString, location, MessageType.Error);
-					if (mc == null)
-						mc = new MessageCollection (message);
-					else
-						mc.Add (message);
+					Runner.Report (ctor, Severity.Low, Confidence.High, String.Empty);
 				}
 			}
 
-			return mc;
+			return Runner.CurrentRuleResult;
 		}
 	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/BadRecursiveInvocationRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/BadRecursiveInvocationRule.cs
index 409db073..d9b76795 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/BadRecursiveInvocationRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/BadRecursiveInvocationRule.cs
@@ -38,7 +38,9 @@ using Gendarme.Framework;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class BadRecursiveInvocationRule : IMethodRule {
+	[Problem ("This method, or property, invokes itself recursively in a suspcious way.")]
+	[Solution ("Ensure that an exit condition exists to terminate recursion.")]
+	public class BadRecursiveInvocationRule : Rule, IMethodRule {
 
 		// note: parameter names do not have to match because we can be calling a base class virtual method
 		private static bool CheckParameters (MethodReference caller, MethodReference callee)
@@ -130,11 +132,11 @@ namespace Gendarme.Rules.Correctness {
 			return false;
 		}
 
-		public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
+		public RuleResult CheckMethod (MethodDefinition method)
 		{
 			// rule applies only if the method has a body
 			if (!method.HasBody)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			foreach (Instruction ins in method.Body.Instructions) {
 				switch (ins.OpCode.FlowControl) {
@@ -148,20 +150,19 @@ namespace Gendarme.Rules.Correctness {
 
 					// recursion detected! check if there a way out of it
 					if (CheckForEndlessRecursion (method, method.Body.Instructions.IndexOf (ins))) {
-						Location loc = new Location (method, ins.Offset);
-						Message msg = new Message ("Suspicious recursive call found.", loc, MessageType.Warning);
-						return new MessageCollection (msg);
+						Runner.Report (method, ins, Severity.Critical, Confidence.High, String.Empty);
+						return RuleResult.Failure;
 					}
 					break;
 				case FlowControl.Cond_Branch:
 				case FlowControl.Return:
 				case FlowControl.Throw:
 					// if there's a way to break free before a recursive call then we let it go
-					return runner.RuleSuccess;
+					return RuleResult.Success;
 				}
 			}
 
-			return runner.RuleSuccess;
+			return RuleResult.Success;
 		}
 	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/CallingEqualsWithNullArgRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/CallingEqualsWithNullArgRule.cs
index 1716fe89..9a001c9f 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/CallingEqualsWithNullArgRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/CallingEqualsWithNullArgRule.cs
@@ -6,7 +6,7 @@
 //	Sebastien Pouliot  <sebastien@ximian.com>
 //
 // Copyright (c) <2007> Nidhi Rawal
-// Copyright (C) 2007 Novell, Inc (http://www.novell.com)
+// Copyright (C) 2007-2008 Novell, Inc (http://www.novell.com)
 //
 // Permission is hereby granted, free of charge, to any person obtaining a copy
 // of this software and associated documentation files (the "Software"), to deal
@@ -27,29 +27,22 @@
 // THE SOFTWARE.
 
 using System;
-using System.Collections;
 
 using Mono.Cecil;
 using Mono.Cecil.Cil;
+
 using Gendarme.Framework;
+using Gendarme.Framework.Helpers;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class CallingEqualsWithNullArgRule: IMethodRule {
-
-		private static bool IsEquals (MethodReference md)
-		{
-			if ((md == null) || (md.Name != "Equals"))
-				return false;
-
-			return (md.ReturnType.ReturnType.FullName == "System.Boolean");
-		}
+	[Problem ("This method calls Equals(object) with a null argument.")]
+	[Solution ("Pass some other appropriate argument than null, as passing null parameter should always return false.")]
+	public class CallingEqualsWithNullArgRule: Rule, IMethodRule {
 
-		private static bool IsCall (Instruction ins)
-		{
-			OpCode oc = ins.OpCode;
-			return ((oc == OpCodes.Call) || (oc == OpCodes.Calli) || (oc == OpCodes.Callvirt));
-		}
+		// MethodSignatures.Equals check for a System.Object parameter while this rule is more general
+		// and will work as long as there is a single parameter, whatever the type
+		private static readonly new MethodSignature Equals = new MethodSignature ("Equals", "System.Boolean", new string [1], MethodAttributes.Public);
 
 		private static bool IsPreviousLdnull (Instruction ins)
 		{
@@ -66,29 +59,28 @@ namespace Gendarme.Rules.Correctness {
 			return false;
 		}
 
-		public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
+		public RuleResult CheckMethod (MethodDefinition method)
 		{
 			if (!method.HasBody)
-				return null;
+				return RuleResult.DoesNotApply;
 
-			MessageCollection mc = null;
 			foreach (Instruction ins in method.Body.Instructions) {
 				// if we're calling bool type.Equals()
-				if (IsCall (ins) && IsEquals (ins.Operand as MethodReference)) {
-					// and that the previous, real, instruction is loading a null value
-					if (IsPreviousLdnull (ins)) {
-						Location location = new Location (method, ins.Offset);
-						Message message = new Message ("You should not call Equals (null), i.e., argument should not be null", location, MessageType.Error);
-
-						if (mc == null)
-							mc = new MessageCollection (message);
-						else
-							mc.Add (message);
+				switch (ins.OpCode.Code) {
+				case Code.Call:
+				case Code.Calli:
+				case Code.Callvirt:
+					if (Equals.Matches (ins.Operand as MethodReference)) {
+						// and that the previous, real, instruction is loading a null value
+						if (IsPreviousLdnull (ins)) {
+							Runner.Report (method, ins, Severity.Low, Confidence.High, String.Empty);
+						}
 					}
+					break;
 				}
 			}
 
-			return mc;
+			return Runner.CurrentRuleResult;
 		}
 	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/ChangeLog b/gendarme/rules/Gendarme.Rules.Correctness/ChangeLog
index b7f034f9..50e516bf 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/ChangeLog
+++ b/gendarme/rules/Gendarme.Rules.Correctness/ChangeLog
@@ -1,3 +1,18 @@
+2008-02-15  Sebastien Pouliot  <sebastien@ximian.com>
+
+	* AvoidConstructorsInStaticTypesRule.cs
+	* BadRecursiveInvocationRule.cs
+	* CallingEqualsWithNullArgRule.cs
+	* DontCompareWithNaNRule.cs
+	* FloatComparisonRule.cs
+	* MethodCanBeMadeStaticRule.cs
+	* NullDerefAnalysis.cs
+	* NullDerefFrame.cs
+	* NullDerefRule.cs
+	* Nullity.cs
+	* UseValueInPropertySetterRule.cs:
+		Update rules wrt framework changes.
+
 2008-01-29  Sebastien Pouliot  <sebastien@ximian.com>
 
 	* FloatComparisonRule.cs: Handle "this" and don't report defects on
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/DontCompareWithNaNRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/DontCompareWithNaNRule.cs
index 78e8b40f..6a5ed888 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/DontCompareWithNaNRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/DontCompareWithNaNRule.cs
@@ -1,5 +1,5 @@
 //
-// Gendarme.Rules.Correctness.DontCompareWithNaNRule
+// Gendarme.Rules.Correctness.DoNotCompareWithNaNRule
 //
 // Authors:
 //	Sebastien Pouliot <sebastien@ximian.com>
@@ -36,7 +36,9 @@ using Gendarme.Framework.Rocks;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class DontCompareWithNaNRule : IMethodRule {
+	[Problem ("This method compares a floating point value with NaN (Not a Number) which always return false, even for (NaN == NaN).")]
+	[Solution ("Replace the code with a call to the appropriate Single.IsNaN(value) or Double.IsNaN(value).")]
+	public class DoNotCompareWithNaNRule : Rule, IMethodRule {
 
 		private const string EqualityMessage = "A floating point value is compared (== or !=) with [Single|Double].NaN.";
 		private const string EqualsMessage = "[Single|Double].Equals is called using NaN.";
@@ -69,13 +71,11 @@ namespace Gendarme.Rules.Correctness {
 			return true;
 		}
 
-		public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
+		public RuleResult CheckMethod (MethodDefinition method)
 		{
-			MessageCollection messageCollection = null;
 			if (!method.HasBody)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
-			MessageCollection mc = null;
 			InstructionCollection il = method.Body.Instructions;
 			for (int i = 0; i < method.Body.Instructions.Count; i++) {
 				Instruction ins = il [i];
@@ -83,11 +83,7 @@ namespace Gendarme.Rules.Correctness {
 				// handle == and !=
 				case Code.Ceq:
 					if (!CheckPrevious (il, i - 1)) {
-						Message msg = new Message (EqualityMessage, new Location (method, ins.Offset), MessageType.Error);
-						if (mc == null)
-							mc = new MessageCollection (msg);
-						else
-							mc.Add (msg);
+						Runner.Report (method, ins, Severity.Critical, Confidence.Total, EqualityMessage);
 					}
 					break;
 				// handle calls to [Single|Double].Equals
@@ -97,17 +93,13 @@ namespace Gendarme.Rules.Correctness {
 					MemberReference callee = ins.Operand as MemberReference;
 					if (callee.Name.Equals ("Equals") && callee.DeclaringType.IsFloatingPoint ()) {
 						if (!CheckPrevious (il, i - 1)) {
-							Message msg = new Message (EqualsMessage, new Location (method, ins.Offset), MessageType.Error);
-							if (mc == null)
-								mc = new MessageCollection (msg);
-							else
-								mc.Add (msg);
+							Runner.Report (method, ins, Severity.Critical, Confidence.Total, EqualsMessage);
 						}
 					}
 					break;
 				}
 			}
-			return mc;
+			return Runner.CurrentRuleResult;
 		}
 	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/FloatComparisonRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/FloatComparisonRule.cs
index ea6291c2..1d26022f 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/FloatComparisonRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/FloatComparisonRule.cs
@@ -38,7 +38,9 @@ using Gendarme.Framework.Rocks;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class FloatComparisonRule : IMethodRule {
+	[Problem ("This method contais some code that performs equality operation between floating points.")]
+	[Solution ("Try comparing the absolute difference between the two floating point values and a small constant value.")]
+	public class FloatComparisonRule : Rule, IMethodRule {
 
 		private const string EqualityMessage = "Floating point values should not be directly compared for equality (e.g. == or !=).";
 		private const string EqualsMessage = "Floating point values should not be directly compared for equality using [Single|Double].Equals.";
@@ -94,28 +96,22 @@ namespace Gendarme.Rules.Correctness {
 			return problem;
 		}
 
-		public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
+		public RuleResult CheckMethod (MethodDefinition method)
 		{
 			// we only check methods with a body
 			if (!method.HasBody)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// we don't check System.Single and System.Double
 			// special case for handling mscorlib.dll
 			if (method.DeclaringType.IsFloatingPoint ())
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
-			MessageCollection mc = null;
 			foreach (Instruction instruction in method.Body.Instructions) {
 				switch (instruction.OpCode.Code) {
 				case Code.Ceq:
 					if (CheckCeqInstruction (SkipArithmeticOperations (instruction), method)) {
-						Location location = new Location (method, instruction.Offset);
-						Message message = new Message (EqualityMessage, location, MessageType.Error);
-						if (mc == null)
-							mc = new MessageCollection (message);
-						else
-							mc.Add (message);
+						Runner.Report (method, instruction, Severity.High, Confidence.Total, EqualityMessage);
 					}
 					break;
 				case Code.Call:
@@ -123,18 +119,13 @@ namespace Gendarme.Rules.Correctness {
 				case Code.Callvirt:
 					MemberReference member = instruction.Operand as MemberReference;
 					if (member.Name.Equals ("Equals") && member.DeclaringType.IsFloatingPoint ()) {
-						Location location = new Location (method, instruction.Offset);
-						Message message = new Message (EqualsMessage, location, MessageType.Error);
-						if (mc == null)
-							mc = new MessageCollection (message);
-						else
-							mc.Add (message);
+						Runner.Report (method, instruction, Severity.High, Confidence.Total, EqualsMessage);
 					}
 					break;
 				}
 			}
 
-			return mc;
+			return Runner.CurrentRuleResult;
 		}
 
 		static OpCode [] arithOpCodes = new OpCode [] {
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/MethodCanBeMadeStaticRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/MethodCanBeMadeStaticRule.cs
index 0f9dfa0b..f976f9ba 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/MethodCanBeMadeStaticRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/MethodCanBeMadeStaticRule.cs
@@ -36,33 +36,34 @@ using Gendarme.Framework.Rocks;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class MethodCanBeMadeStaticRule : IMethodRule {
+	[Problem ("This method does not use any instance fields, properties or methods and can be made static.")]
+	[Solution ("Make this method static.")]
+	public class MethodCanBeMadeStaticRule : Rule, IMethodRule {
 
-		public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
+		public RuleResult CheckMethod (MethodDefinition method)
 		{
 			// we only check non static, non virtual methods and not constructors
 			if (method.IsStatic || method.IsVirtual || method.IsConstructor)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// we only check methods with a body
 			if (!method.HasBody)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// that aren't compiler generated (e.g. anonymous methods) or generated by a tool (e.g. web services)
 			if (method.IsGeneratedCode ())
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// rule applies
 
 			// if we find a use of the "this" reference, it's ok
-			foreach (Instruction instr in method.Body.Instructions)
-				if (instr.OpCode == OpCodes.Ldarg_0 ||
-					(instr.OpCode == OpCodes.Ldarg && (int) instr.Operand == 0))
-					return runner.RuleSuccess;
+			foreach (Instruction instr in method.Body.Instructions) {
+				if (instr.OpCode == OpCodes.Ldarg_0 || (instr.OpCode == OpCodes.Ldarg && (int) instr.Operand == 0))
+					return RuleResult.Success;
+			}
 
-			Location loc = new Location (method);
-			Message msg = new Message ("This method could be static.", loc, MessageType.Warning);
-			return new MessageCollection (msg);
+			Runner.Report (method, Severity.Low, Confidence.Total, string.Empty);
+			return RuleResult.Failure;
 		}
 	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/NullDerefAnalysis.cs b/gendarme/rules/Gendarme.Rules.Correctness/NullDerefAnalysis.cs
index f23464fc..dcaa0f74 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/NullDerefAnalysis.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/NullDerefAnalysis.cs
@@ -20,706 +20,671 @@ using Gendarme.Framework;
 
 namespace Gendarme.Rules.Correctness {
 
-public class NullDerefAnalysis : IDataflowAnalysis {
-
-    int stackDepth;
-    int locals;
-    int args;
-    [NonNull] private MethodDefinition method;
-    [NonNull] private NonNullAttributeCollector nnaCollector;
-    [NonNull] private MessageCollection messages;
-    [NonNull] private Runner runner;
-
-    public NullDerefAnalysis([NonNull] MethodDefinition method,
-            [NonNull] MessageCollection messages,
-            [NonNull] NonNullAttributeCollector nnaCollector,
-            [NonNull] Runner runner)
-    {
-        this.stackDepth = method.Body.MaxStack;
-        this.locals = method.Body.Variables.Count;
-        if(method.HasThis)
-            this.args = method.Parameters.Count + 1;
-        else
-            this.args = method.Parameters.Count;
-        this.method = method;
-        this.messages = messages;
-        this.nnaCollector = nnaCollector;
-        this.runner = runner;
-    }
-
-    [NonNull]
-    public object NewTop()
-    {
-        return new NullDerefFrame(stackDepth, locals, args, false, runner);
-    }
-
-    [NonNull]
-    public object NewEntry()
-    {
-        NullDerefFrame result =
-            new NullDerefFrame(stackDepth, locals, args, true, runner);
-        if(method.HasThis)
-            result.SetArgNullity(0, Nullity.NonNull);
-        foreach(ParameterDefinition param in method.Parameters)
-            if(nnaCollector.HasNonNullAttribute(method, param))
-                result.SetArgNullity(param.Sequence - 1, Nullity.NonNull);
-        return result;
-    }
-
-    [NonNull]
-    public object NewCatch()
-    {
-        NullDerefFrame result =
-            new NullDerefFrame(stackDepth, locals, args, true, runner);
-        if(method.HasThis)
-            result.SetArgNullity(0, Nullity.NonNull);
-        foreach(ParameterDefinition param in method.Parameters)
-            if(nnaCollector.HasNonNullAttribute(method, param))
-                result.SetArgNullity(param.Sequence - 1, Nullity.NonNull);
-        /* The exception being caught is pushed onto the stack. */
-        result.PushStack(Nullity.NonNull);
-        return result;
-    }
-
-    /* Changes originalFact. */
-    public void MeetInto([NonNull] object originalFact,
-            [NonNull] object newFact, bool warn)
-    {
-        NullDerefFrame original = (NullDerefFrame)originalFact;
-        NullDerefFrame incoming = (NullDerefFrame)newFact;
-        original.MergeWith(incoming);
-    }
-
-    private static bool IsVoid([NonNull] TypeReference type)
-    {
-        if(type.FullName.Equals("System.Void"))
-            return true;
-        return false;
-    }
-
-    public void Transfer([NonNull] Node node, [NonNull] object inFact,
-            [NonNull] object outFact, bool warn)
-    {
-        BasicBlock bb = (BasicBlock)node;
-
-        /* Exit and exception nodes don't cover any real instructions. */
-        if(bb.isExit || bb.isException)
-            return;
-
-        //NullDerefFrame inFrame = (NullDerefFrame)inFact;
-        NullDerefFrame outFrame = (NullDerefFrame)outFact;
-        VariableDefinitionCollection vars = method.Body.Variables;
-
-        if(runner.Debug) {
-            Console.WriteLine("Basic block {0}", bb.ToString());
-            Console.WriteLine("Input frame:");
-            Console.Write(outFrame.ToString());
-        }
-
-        for(int i = bb.first; i <= bb.last; i++) {
-            Instruction insn = bb.Instructions[i];
-            OpCode opcode = insn.OpCode;
-
-            if(runner.Debug) {
-                Console.Write("{0}", opcode.Name);
-                if(insn.Operand != null && !(insn.Operand is Instruction)) {
-                    Console.WriteLine(" {0}", insn.Operand.ToString());
-                } else if(insn.Operand is Instruction) {
-                    Console.WriteLine(" {0}",
-                            ((Instruction)insn.Operand).Offset.ToString("X4"));
-                } else {
-                    Console.WriteLine();
-                }
-            }
-
-            switch (opcode.Code) {
-                /* Load argument */
-                /* Stored nullities are set to declared values on method
-                 * entry. Starg and kin can change this over time. */
-                case Code.Ldarg_0:
-                    outFrame.PushStack(outFrame.GetArgNullity(0));
-                    break;
-		case Code.Ldarg_1:
-                    outFrame.PushStack(outFrame.GetArgNullity(1));
-                    break;
-		case Code.Ldarg_2:
-                    outFrame.PushStack(outFrame.GetArgNullity(2));
-                    break;
-		case Code.Ldarg_3:
-                    outFrame.PushStack(outFrame.GetArgNullity(3));
-                    break;
-		case Code.Ldarg:
-		    if (insn.Operand is int) {
-			outFrame.PushStack (outFrame.GetArgNullity ((int) insn.Operand));
-		    } else if (insn.Operand is ParameterDefinition) {
-			ParameterDefinition pd = (insn.Operand as ParameterDefinition);
-			outFrame.PushStack ((pd.HasConstant && pd.Constant == null) ? 
-				Nullity.Null : Nullity.NonNull);
-		    } else {
-			outFrame.PushStack(Nullity.NonNull);
-		    }
-                    break;
-		case Code.Ldarg_S: {
-                    ParameterDefinition param =
-                        (ParameterDefinition)insn.Operand;
-                    outFrame.PushStack(
-                            outFrame.GetArgNullity(param.Sequence - 1));
-                    break;
-                }
-		case Code.Ldarga:
-		case Code.Ldarga_S:
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-                /* Store argument */
-		case Code.Starg:
-                    outFrame.SetArgNullity((int)insn.Operand,
-                            outFrame.PopStack());
-                    break;
-		case Code.Starg_S: {
-                    ParameterDefinition param =
-                        (ParameterDefinition)insn.Operand;
-                    outFrame.SetArgNullity(param.Sequence - 1,
-                            outFrame.PopStack());
-                    break;
-                }
-
-                /* Load local */
-		case Code.Ldloc_0:
-                    outFrame.PushStack(outFrame.GetLocNullity(0));
-                    break;
-		case Code.Ldloc_1:
-                    outFrame.PushStack(outFrame.GetLocNullity(1));
-                    break;
-		case Code.Ldloc_2:
-                    outFrame.PushStack(outFrame.GetLocNullity(2));
-                    break;
-		case Code.Ldloc_3:
-                    outFrame.PushStack(outFrame.GetLocNullity(3));
-                    break;
-		case Code.Ldloc:
-		case Code.Ldloc_S:
-                    outFrame.PushStack(outFrame.GetLocNullity(
-                        vars.IndexOf((VariableDefinition)insn.Operand)));
-                    break;
-		case Code.Ldloca:
-		case Code.Ldloca_S:
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                /* Store local */
-		case Code.Stloc_0:
-                    outFrame.SetLocNullity(0, outFrame.PopStack());
-                    break;
-		case Code.Stloc_1:
-                    outFrame.SetLocNullity(1, outFrame.PopStack());
-                    break;
-		case Code.Stloc_2:
-                    outFrame.SetLocNullity(2, outFrame.PopStack());
-                    break;
-		case Code.Stloc_3:
-                    outFrame.SetLocNullity(3, outFrame.PopStack());
-                    break;
-		case Code.Stloc:
-		case Code.Stloc_S:
-                    outFrame.SetLocNullity(
-                        vars.IndexOf((VariableDefinition)insn.Operand),
-                        outFrame.PopStack());
-                    break;
-
-                /* Load other things */
-		case Code.Ldftn:
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Ldvirtftn:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Ldstr:
-		case Code.Ldnull:
-                    outFrame.PushStack(Nullity.Null);
-                    break;
-		case Code.Ldlen:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Ldtoken:
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                 /* Object operations */
-		case Code.Cpobj:
-		    outFrame.PopStack (2);
-		    break;
-		case Code.Newobj:
-                    outFrame.PopStack(
-                        ((MethodReference)insn.Operand).Parameters.Count);
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Ldobj:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Stobj:
-		    outFrame.PopStack (2);
-		    break;
-		case Code.Initobj:
-		    outFrame.PopStack ();
-		    break;
-
-                 /* Load field */
-		case Code.Ldfld: {
-                    Check(insn, warn, outFrame.PopStack(), "field");
-                    FieldReference field = (FieldReference)insn.Operand;
-                    if(nnaCollector.HasNonNullAttribute(field))
-                        outFrame.PushStack(Nullity.NonNull);
-                    else
-                        outFrame.PushStack(Nullity.Unknown);
-                    break;
-                }
-		case Code.Ldflda:
-                    Check(insn, warn, outFrame.PopStack(), "field");
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Ldsfld: {
-                    FieldReference field = (FieldReference)insn.Operand;
-                    if(nnaCollector.HasNonNullAttribute(field))
-                        outFrame.PushStack(Nullity.NonNull);
-                    else
-                        outFrame.PushStack(Nullity.Unknown);
-                    break;
-                }
-		case Code.Ldsflda:
-			outFrame.PushStack (Nullity.NonNull);
-			break;
-
-                /* Store field */
-		case Code.Stfld: {
-                    /* FIXME: warn if writing null to non-null field */
-                    Nullity n = outFrame.PopStack();
-                    Check(insn, warn, outFrame.PopStack(), "field");
-                    FieldReference field = (FieldReference)insn.Operand;
-                    if(warn && nnaCollector.HasNonNullAttribute(field)) {
-                        Location loc = new Location(method, insn.Offset);
-                        if(n == Nullity.Unknown)
-                            messages.Add(new Message(
-                                        "storing possibly null value in " +
-                                        "field declared non-null",
-                                        loc, MessageType.Warning));
-                        else if(n == Nullity.Null)
-                            messages.Add(new Message(
-                                        "storing null value in " +
-                                        "field declared non-null",
-                                        loc, MessageType.Warning));
-                    }
-                    break;
-                }
-		case Code.Stsfld: {
-                    Nullity n = outFrame.PopStack();
-                    FieldReference field = (FieldReference)insn.Operand;
-                    if(warn && nnaCollector.HasNonNullAttribute(field)) {
-                        Location loc = new Location(method, insn.Offset);
-                        if(n == Nullity.Unknown)
-                            messages.Add(new Message(
-                                        "storing possibly null value in " +
-                                        "field declared non-null",
-                                        loc, MessageType.Warning));
-                        else if(n == Nullity.Null)
-                            messages.Add(new Message(
-                                        "storing null value in " +
-                                        "field declared non-null",
-                                        loc, MessageType.Warning));
-                    }
-                    break;
-                }
-
-                /* Stack operations */
-		case Code.Dup:
-			outFrame.PushStack (outFrame.PeekStack ());
-			break;
-		case Code.Pop:
-			outFrame.PopStack ();
-			break;
-
-                 /* Method call and return */
-		case Code.Calli:
-                    ProcessCall(insn, warn, true, outFrame);
-                    break;
-		case Code.Call:
-		case Code.Callvirt:
-                    ProcessCall(insn, warn, false, outFrame);
-                    break;
-		case Code.Ret:
-                    if(!IsVoid(method.ReturnType.ReturnType)) {
-                        Nullity n = outFrame.PopStack();
-                        if(nnaCollector.HasNonNullAttribute(method) && warn) {
-                            Location loc = new Location (method, insn.Offset);
-                            if(n == Nullity.Null)
-                                messages.Add(new Message(
-                                            "returning null value from " +
-                                            "method declared non-null",
-                                            loc, MessageType.Warning));
-                            else if(n == Nullity.Unknown)
-                                messages.Add(new Message(
-                                            "returning possibly null value " +
-                                            "from method declared non-null",
-                                            loc, MessageType.Warning));
-                        }
-                    }
-                    break;
-
-                /* Indirect load */
-		case Code.Ldind_I1:
-		case Code.Ldind_U1:
-		case Code.Ldind_I2:
-		case Code.Ldind_U2:
-		case Code.Ldind_I4:
-		case Code.Ldind_U4:
-		case Code.Ldind_I8:
-		case Code.Ldind_I:
-		case Code.Ldind_R4:
-		case Code.Ldind_R8:
-		case Code.Ldind_Ref:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.Unknown);
-                    break;
-
-                /* Indirect store */
-		case Code.Stind_Ref:
-		case Code.Stind_I:
-		case Code.Stind_I1:
-		case Code.Stind_I2:
-		case Code.Stind_I4:
-		case Code.Stind_I8:
-		case Code.Stind_R4:
-		case Code.Stind_R8:
-		    outFrame.PopStack (2);
-		    break;
-
-                /* Class-related operations */
-		case Code.Box:
-		case Code.Unbox:
-		case Code.Unbox_Any:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Castclass:
-		case Code.Isinst:
-		    break;
-
-                /* Exception handling */
-		case Code.Rethrow:
-		    break;
-		case Code.Throw:
-		case Code.Leave:
-		case Code.Leave_S:
-		case Code.Endfinally:
-		case Code.Endfilter:
-		    outFrame.PopStack ();
-		    break;
-
-                /* Array operations */
-		case Code.Newarr:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-                /* Load element */
-		case Code.Ldelema:
-		case Code.Ldelem_I1:
-		case Code.Ldelem_U1:
-		case Code.Ldelem_I2:
-		case Code.Ldelem_U2:
-		case Code.Ldelem_I4:
-		case Code.Ldelem_U4:
-		case Code.Ldelem_I8:
-		case Code.Ldelem_I:
-		case Code.Ldelem_R4:
-		case Code.Ldelem_R8:
-                    outFrame.PopStack(2);
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Ldelem_Ref:
-		case Code.Ldelem_Any: /* This may or may not be a reference. */
-                    outFrame.PopStack(2);
-                    outFrame.PushStack(Nullity.Unknown);
-                    break;
-                /* Store element */
-                /* Pop 3 */
-		case Code.Stelem_I:
-		case Code.Stelem_I1:
-		case Code.Stelem_I2:
-		case Code.Stelem_I4:
-		case Code.Stelem_I8:
-		case Code.Stelem_R4:
-		case Code.Stelem_R8:
-		case Code.Stelem_Ref:
-		case Code.Stelem_Any:
-		    outFrame.PopStack (3);
-		    break;
-
-		case Code.Arglist:
-		case Code.Sizeof:
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-		case Code.Mkrefany:
-		case Code.Refanyval:
-		case Code.Refanytype:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                /* Prefixes */
-		case Code.Unaligned:
-		case Code.Volatile:
-		case Code.Tail:
-		    break;
-
-                /* Effect-free instructions */
-		case Code.Nop:
-		case Code.Break:
-		    break;
-
-                /* Load constant */
-                /* Push non-ref. */
-		case Code.Ldc_I4_M1:
-		case Code.Ldc_I4_0:
-		case Code.Ldc_I4_1:
-		case Code.Ldc_I4_2:
-		case Code.Ldc_I4_3:
-		case Code.Ldc_I4_4:
-		case Code.Ldc_I4_5:
-		case Code.Ldc_I4_6:
-		case Code.Ldc_I4_7:
-		case Code.Ldc_I4_8:
-		case Code.Ldc_I4_S:
-		case Code.Ldc_I4:
-		case Code.Ldc_I8:
-		case Code.Ldc_R4:
-		case Code.Ldc_R8:
-		    outFrame.PushStack (Nullity.NonNull);
-		    break;
-
-                /* Unconditional control flow */
-                /* Do nothing */
-		case Code.Br:
-		case Code.Br_S:
-		    break;
-
-                /* Conditional branches */
-                /* Pop 1 */
-		case Code.Brfalse:
-		case Code.Brtrue:
-		case Code.Brfalse_S:
-		case Code.Brtrue_S:
-		    outFrame.PopStack ();
-		    break;
-
-                /* Comparison branches */
-                /* Pop 2. */
-		case Code.Beq:
-		case Code.Bge:
-		case Code.Bgt:
-		case Code.Ble:
-		case Code.Blt:
-		case Code.Bne_Un:
-		case Code.Bge_Un:
-		case Code.Bgt_Un:
-		case Code.Ble_Un:
-		case Code.Blt_Un:
-		case Code.Beq_S:
-		case Code.Bge_S:
-		case Code.Bgt_S:
-		case Code.Ble_S:
-		case Code.Blt_S:
-		case Code.Bne_Un_S:
-		case Code.Bge_Un_S:
-		case Code.Bgt_Un_S:
-		case Code.Ble_Un_S:
-		case Code.Blt_Un_S:
-			outFrame.PopStack (2);
-			break;
-
-                case Code.Switch:
-			outFrame.PopStack(); break;
-
-                /* Comparisons */
-                /* Pop 2, push non-ref */
-		case Code.Ceq:
-		case Code.Cgt:
-		case Code.Cgt_Un:
-		case Code.Clt:
-		case Code.Clt_Un:
-                    outFrame.PopStack(2);
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                /* Arithmetic and logical binary operators */
-                /* Pop 2, push non-ref */
-		case Code.Add:
-		case Code.Sub:
-		case Code.Mul:
-		case Code.Div:
-		case Code.Div_Un:
-		case Code.Rem:
-		case Code.Rem_Un:
-		case Code.And:
-		case Code.Or:
-		case Code.Xor:
-		case Code.Shl:
-		case Code.Shr:
-		case Code.Shr_Un:
-		case Code.Add_Ovf:
-		case Code.Add_Ovf_Un:
-		case Code.Mul_Ovf:
-		case Code.Mul_Ovf_Un:
-		case Code.Sub_Ovf:
-		case Code.Sub_Ovf_Un:
-                    outFrame.PopStack(2);
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                /* Arithmetic and logical unary operators */
-                /* Pop 1, push non-ref */
-                case Code.Neg:
-                case Code.Not:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                /* Conversions. */
-                /* Do nothing. */
-		case Code.Conv_I1:
-		case Code.Conv_I2:
-		case Code.Conv_I4:
-		case Code.Conv_I8:
-		case Code.Conv_R4:
-		case Code.Conv_R8:
-		case Code.Conv_U4:
-		case Code.Conv_U8:
-		case Code.Conv_U:
-		case Code.Conv_R_Un:
-		case Code.Conv_Ovf_I1_Un:
-		case Code.Conv_Ovf_I2_Un:
-		case Code.Conv_Ovf_I4_Un:
-		case Code.Conv_Ovf_I8_Un:
-		case Code.Conv_Ovf_U1_Un:
-		case Code.Conv_Ovf_U2_Un:
-		case Code.Conv_Ovf_U4_Un:
-		case Code.Conv_Ovf_U8_Un:
-		case Code.Conv_Ovf_I_Un:
-		case Code.Conv_Ovf_U_Un:
-		case Code.Conv_Ovf_I1:
-		case Code.Conv_Ovf_U1:
-		case Code.Conv_Ovf_I2:
-		case Code.Conv_Ovf_U2:
-		case Code.Conv_Ovf_I4:
-		case Code.Conv_Ovf_U4:
-		case Code.Conv_Ovf_I8:
-		case Code.Conv_Ovf_U8:
-		case Code.Conv_U2:
-		case Code.Conv_U1:
-		case Code.Conv_I:
-		case Code.Conv_Ovf_I:
-		case Code.Conv_Ovf_U:
-		case Code.Ckfinite:
-			break;
-
-                /* Unverifiable instructions. */
-                case Code.Jmp:
-			break;
-		case Code.Cpblk:
-			outFrame.PopStack (3);
-			break;
-		case Code.Initblk:
-			outFrame.PopStack (3);
-			break;
-		case Code.Localloc:
-                    outFrame.PopStack();
-                    outFrame.PushStack(Nullity.NonNull);
-                    break;
-
-                default:
-                    Console.WriteLine("Unknown instruction: {0} {1}",
-                            opcode.Name, opcode.Value.ToString("X4"));
-                    break;
-            } /* switch */
-        } /* for */
-
-        if(runner.Debug) {
-            Console.WriteLine("Output frame:");
-            Console.Write(outFrame.ToString());
-        }
-    } /* Transfer */
-
-    private void Check([NonNull]Instruction insn, bool warn, Nullity n,
-            [NonNull] string type)
-    {
-        if(!warn) return;
-
-        Location loc = new Location (method, insn.Offset);
-        string name = insn.Operand.ToString();
-        int nameOffset = name.LastIndexOf("::");
-        if(nameOffset != -1)
-            name = name.Substring(nameOffset + 2);
-        if(type.Equals("method")) {
-            string prefix = name.Substring(0, 4);
-            if(prefix.Equals("get_") || prefix.Equals("set_")) {
-                name = name.Substring(4);
-                type = "property";
-            }
-        }
-        if(n == Nullity.Unknown) {
-            messages.Add(new Message(
-                        "accessing " + type + " " + name +
-                        " from potentially null object",
-                        loc, MessageType.Warning));
-        } else if(n == Nullity.Null) {
-            messages.Add(new Message(
-                        "accessing " + type + " " + name +
-                        " from null object",
-                        loc, MessageType.Warning));
-        }
-    }
-
-    private void ProcessCall([NonNull] Instruction insn, bool warn,
-            bool indirect, [NonNull] NullDerefFrame frame)
-    {
-        Location loc = new Location (method, insn.Offset);
-        IMethodSignature csig = (IMethodSignature)insn.Operand;
-        if(indirect)
-            frame.PopStack(); /* Function pointer */
-        foreach(ParameterDefinition param in csig.Parameters) {
-            Nullity n = frame.PopStack();
-            if(warn && nnaCollector.HasNonNullAttribute(method, param)) {
-                if(n == Nullity.Null)
-                    messages.Add(new Message(
-                                "passing null value as argument " +
-                                "declared non-null",
-                                loc, MessageType.Warning));
-                else if(n == Nullity.Unknown)
-                    messages.Add(new Message(
-                                "passing possibly null value as argument " +
-                                "declared non-null",
-                                loc, MessageType.Warning));
-            }
-        }
-        if(csig.HasThis && !Ignoring(csig)) /* Add 'this' parameter. */
-            Check(insn, warn, frame.PopStack(), "method");
-        if(!IsVoid(csig.ReturnType.ReturnType)) {
-            if(csig.ReturnType.ReturnType.IsValueType)
-                frame.PushStack(Nullity.NonNull);
-            else if(nnaCollector.HasNonNullAttribute(csig))
-                frame.PushStack(Nullity.NonNull);
-            else
-                frame.PushStack(Nullity.Unknown);
-        }
-    }
-
-    private static bool Ignoring([NonNull] IMethodSignature msig)
-    {
-        /* FIXME: Ignoring is a temporary hack! */
-        /* Right now, it always returns false, as it should. */
-        return false;
-    }
-}
-
+	public class NullDerefAnalysis : IDataflowAnalysis {
+
+		int stackDepth;
+		int locals;
+		int args;
+		[NonNull] private MethodDefinition method;
+		[NonNull] private NonNullAttributeCollector nnaCollector;
+		[NonNull] private IRunner runner;
+
+		public NullDerefAnalysis([NonNull] MethodDefinition method,
+				[NonNull] NonNullAttributeCollector nnaCollector,
+				[NonNull] IRunner runner)
+		{
+			this.stackDepth = method.Body.MaxStack;
+			this.locals = method.Body.Variables.Count;
+			if(method.HasThis)
+				this.args = method.Parameters.Count + 1;
+			else
+				this.args = method.Parameters.Count;
+			this.method = method;
+			this.nnaCollector = nnaCollector;
+			this.runner = runner;
+		}
+
+		[NonNull]
+		public object NewTop()
+		{
+			return new NullDerefFrame(stackDepth, locals, args, false, runner);
+		}
+
+		[NonNull]
+		public object NewEntry()
+		{
+			NullDerefFrame result =
+				new NullDerefFrame(stackDepth, locals, args, true, runner);
+			if(method.HasThis)
+				result.SetArgNullity(0, Nullity.NonNull);
+			foreach(ParameterDefinition param in method.Parameters)
+				if(nnaCollector.HasNonNullAttribute(method, param))
+					result.SetArgNullity(param.Sequence - 1, Nullity.NonNull);
+			return result;
+		}
+
+		[NonNull]
+		public object NewCatch()
+		{
+			NullDerefFrame result =
+				new NullDerefFrame(stackDepth, locals, args, true, runner);
+			if(method.HasThis)
+				result.SetArgNullity(0, Nullity.NonNull);
+			foreach(ParameterDefinition param in method.Parameters)
+				if(nnaCollector.HasNonNullAttribute(method, param))
+					result.SetArgNullity(param.Sequence - 1, Nullity.NonNull);
+			/* The exception being caught is pushed onto the stack. */
+			result.PushStack(Nullity.NonNull);
+			return result;
+		}
+
+		/* Changes originalFact. */
+		public void MeetInto([NonNull] object originalFact,
+				[NonNull] object newFact, bool warn)
+		{
+			NullDerefFrame original = (NullDerefFrame)originalFact;
+			NullDerefFrame incoming = (NullDerefFrame)newFact;
+			original.MergeWith(incoming);
+		}
+
+		private static bool IsVoid([NonNull] TypeReference type)
+		{
+			if(type.FullName.Equals("System.Void"))
+				return true;
+			return false;
+		}
+
+		public void Transfer([NonNull] Node node, [NonNull] object inFact,
+				[NonNull] object outFact, bool warn)
+		{
+			BasicBlock bb = (BasicBlock)node;
+
+			/* Exit and exception nodes don't cover any real instructions. */
+			if(bb.isExit || bb.isException)
+				return;
+
+			//NullDerefFrame inFrame = (NullDerefFrame)inFact;
+			NullDerefFrame outFrame = (NullDerefFrame)outFact;
+			VariableDefinitionCollection vars = method.Body.Variables;
+
+			if(runner.VerbosityLevel > 1) {
+				Console.WriteLine("Basic block {0}", bb.ToString());
+				Console.WriteLine("Input frame:");
+				Console.Write(outFrame.ToString());
+			}
+
+			for(int i = bb.first; i <= bb.last; i++) {
+				Instruction insn = bb.Instructions[i];
+				OpCode opcode = insn.OpCode;
+
+			if (runner.VerbosityLevel > 1) {
+				Console.Write ("{0}", opcode.Name);
+					if(insn.Operand != null && !(insn.Operand is Instruction)) {
+						Console.WriteLine(" {0}", insn.Operand.ToString());
+					} else if(insn.Operand is Instruction) {
+						Console.WriteLine(" {0}",
+								((Instruction)insn.Operand).Offset.ToString("X4"));
+					} else {
+						Console.WriteLine();
+					}
+				}
+
+				switch (opcode.Code) {
+					/* Load argument */
+					/* Stored nullities are set to declared values on method
+					 * entry. Starg and kin can change this over time. */
+					case Code.Ldarg_0:
+						outFrame.PushStack(outFrame.GetArgNullity(0));
+						break;
+			case Code.Ldarg_1:
+						outFrame.PushStack(outFrame.GetArgNullity(1));
+						break;
+			case Code.Ldarg_2:
+						outFrame.PushStack(outFrame.GetArgNullity(2));
+						break;
+			case Code.Ldarg_3:
+						outFrame.PushStack(outFrame.GetArgNullity(3));
+						break;
+			case Code.Ldarg:
+				if (insn.Operand is int) {
+				outFrame.PushStack (outFrame.GetArgNullity ((int) insn.Operand));
+				} else if (insn.Operand is ParameterDefinition) {
+				ParameterDefinition pd = (insn.Operand as ParameterDefinition);
+				outFrame.PushStack ((pd.HasConstant && pd.Constant == null) ? 
+					Nullity.Null : Nullity.NonNull);
+				} else {
+				outFrame.PushStack(Nullity.NonNull);
+				}
+						break;
+			case Code.Ldarg_S: {
+						ParameterDefinition param =
+							(ParameterDefinition)insn.Operand;
+						outFrame.PushStack(
+								outFrame.GetArgNullity(param.Sequence - 1));
+						break;
+					}
+			case Code.Ldarga:
+			case Code.Ldarga_S:
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+					/* Store argument */
+			case Code.Starg:
+						outFrame.SetArgNullity((int)insn.Operand,
+								outFrame.PopStack());
+						break;
+			case Code.Starg_S: {
+						ParameterDefinition param =
+							(ParameterDefinition)insn.Operand;
+						outFrame.SetArgNullity(param.Sequence - 1,
+								outFrame.PopStack());
+						break;
+					}
+
+					/* Load local */
+			case Code.Ldloc_0:
+						outFrame.PushStack(outFrame.GetLocNullity(0));
+						break;
+			case Code.Ldloc_1:
+						outFrame.PushStack(outFrame.GetLocNullity(1));
+						break;
+			case Code.Ldloc_2:
+						outFrame.PushStack(outFrame.GetLocNullity(2));
+						break;
+			case Code.Ldloc_3:
+						outFrame.PushStack(outFrame.GetLocNullity(3));
+						break;
+			case Code.Ldloc:
+			case Code.Ldloc_S:
+						outFrame.PushStack(outFrame.GetLocNullity(
+							vars.IndexOf((VariableDefinition)insn.Operand)));
+						break;
+			case Code.Ldloca:
+			case Code.Ldloca_S:
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+
+					/* Store local */
+			case Code.Stloc_0:
+						outFrame.SetLocNullity(0, outFrame.PopStack());
+						break;
+			case Code.Stloc_1:
+						outFrame.SetLocNullity(1, outFrame.PopStack());
+						break;
+			case Code.Stloc_2:
+						outFrame.SetLocNullity(2, outFrame.PopStack());
+						break;
+			case Code.Stloc_3:
+						outFrame.SetLocNullity(3, outFrame.PopStack());
+						break;
+			case Code.Stloc:
+			case Code.Stloc_S:
+						outFrame.SetLocNullity(
+							vars.IndexOf((VariableDefinition)insn.Operand),
+							outFrame.PopStack());
+						break;
+
+					/* Load other things */
+			case Code.Ldftn:
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+			case Code.Ldvirtftn:
+						outFrame.PopStack();
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+			case Code.Ldstr:
+			case Code.Ldnull:
+						outFrame.PushStack(Nullity.Null);
+						break;
+			case Code.Ldlen:
+						outFrame.PopStack();
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+			case Code.Ldtoken:
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+
+					 /* Object operations */
+			case Code.Cpobj:
+				outFrame.PopStack (2);
+				break;
+			case Code.Newobj:
+						outFrame.PopStack(
+							((MethodReference)insn.Operand).Parameters.Count);
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+			case Code.Ldobj:
+						outFrame.PopStack();
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+			case Code.Stobj:
+				outFrame.PopStack (2);
+				break;
+			case Code.Initobj:
+				outFrame.PopStack ();
+				break;
+
+					 /* Load field */
+			case Code.Ldfld: {
+						Check(insn, warn, outFrame.PopStack(), "field");
+						FieldReference field = (FieldReference)insn.Operand;
+						if(nnaCollector.HasNonNullAttribute(field))
+							outFrame.PushStack(Nullity.NonNull);
+						else
+							outFrame.PushStack(Nullity.Unknown);
+						break;
+					}
+			case Code.Ldflda:
+						Check(insn, warn, outFrame.PopStack(), "field");
+						outFrame.PushStack(Nullity.NonNull);
+						break;
+			case Code.Ldsfld: {
+						FieldReference field = (FieldReference)insn.Operand;
+						if(nnaCollector.HasNonNullAttribute(field))
+							outFrame.PushStack(Nullity.NonNull);
+						else
+							outFrame.PushStack(Nullity.Unknown);
+						break;
+					}
+			case Code.Ldsflda:
+				outFrame.PushStack (Nullity.NonNull);
+				break;
+
+					/* Store field */
+			case Code.Stfld: {
+				/* FIXME: warn if writing null to non-null field */
+				Nullity n = outFrame.PopStack ();
+				Check (insn, warn, outFrame.PopStack(), "field");
+				FieldReference field = (FieldReference)insn.Operand;
+				if (warn && nnaCollector.HasNonNullAttribute (field)) {
+					if (n == Nullity.Unknown)
+						runner.Report (method, insn, Severity.High, Confidence.Low, "storing possibly null value in field declared non-null");
+					else if (n == Nullity.Null)
+						runner.Report (method, insn, Severity.High, Confidence.Low, "storing null value in field declared non-null");
+				}
+				break;
+			}
+			case Code.Stsfld: {
+				Nullity n = outFrame.PopStack ();
+				FieldReference field = (FieldReference)insn.Operand;
+				if (warn && nnaCollector.HasNonNullAttribute (field)) {
+					if (n == Nullity.Unknown)
+						runner.Report (method, insn, Severity.High, Confidence.Low, "storing possibly null value in field declared non-null");
+					else if (n == Nullity.Null)
+						runner.Report (method, insn, Severity.High, Confidence.Low, "storing null value in field declared non-null");
+				}
+				break;
+			}
+
+			/* Stack operations */
+			case Code.Dup:
+				outFrame.PushStack (outFrame.PeekStack ());
+				break;
+			case Code.Pop:
+				outFrame.PopStack ();
+				break;
+
+			/* Method call and return */
+			case Code.Calli:
+				ProcessCall (insn, warn, true, outFrame);
+				break;
+			case Code.Call:
+			case Code.Callvirt:
+				ProcessCall (insn, warn, false, outFrame);
+				break;
+			case Code.Ret:
+				if(!IsVoid(method.ReturnType.ReturnType)) {
+					Nullity n = outFrame.PopStack();
+					if(nnaCollector.HasNonNullAttribute(method) && warn) {
+						if(n == Nullity.Null)
+							runner.Report (method, insn, Severity.High, Confidence.Low, "returning null value from method declared non-null");
+						else
+							runner.Report (method, insn, Severity.High, Confidence.Low, "returning possibly null value from method declared non-null");
+					}
+				}
+				break;
+
+			/* Indirect load */
+			case Code.Ldind_I1:
+			case Code.Ldind_U1:
+			case Code.Ldind_I2:
+			case Code.Ldind_U2:
+			case Code.Ldind_I4:
+			case Code.Ldind_U4:
+			case Code.Ldind_I8:
+			case Code.Ldind_I:
+			case Code.Ldind_R4:
+			case Code.Ldind_R8:
+			case Code.Ldind_Ref:
+				outFrame.PopStack();
+				outFrame.PushStack(Nullity.Unknown);
+				break;
+
+			/* Indirect store */
+			case Code.Stind_Ref:
+			case Code.Stind_I:
+			case Code.Stind_I1:
+			case Code.Stind_I2:
+			case Code.Stind_I4:
+			case Code.Stind_I8:
+			case Code.Stind_R4:
+			case Code.Stind_R8:
+				outFrame.PopStack (2);
+				break;
+
+			/* Class-related operations */
+			case Code.Box:
+			case Code.Unbox:
+			case Code.Unbox_Any:
+				outFrame.PopStack();
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+			case Code.Castclass:
+			case Code.Isinst:
+				break;
+
+			/* Exception handling */
+			case Code.Rethrow:
+				break;
+			case Code.Throw:
+			case Code.Leave:
+			case Code.Leave_S:
+			case Code.Endfinally:
+			case Code.Endfilter:
+				outFrame.PopStack ();
+				break;
+
+			/* Array operations */
+			case Code.Newarr:
+				outFrame.PopStack();
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+
+			/* Load element */
+			case Code.Ldelema:
+			case Code.Ldelem_I1:
+			case Code.Ldelem_U1:
+			case Code.Ldelem_I2:
+			case Code.Ldelem_U2:
+			case Code.Ldelem_I4:
+			case Code.Ldelem_U4:
+			case Code.Ldelem_I8:
+			case Code.Ldelem_I:
+			case Code.Ldelem_R4:
+			case Code.Ldelem_R8:
+				outFrame.PopStack(2);
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+			case Code.Ldelem_Ref:
+			case Code.Ldelem_Any: /* This may or may not be a reference. */
+				outFrame.PopStack(2);
+				outFrame.PushStack(Nullity.Unknown);
+				break;
+			/* Store element */
+			/* Pop 3 */
+			case Code.Stelem_I:
+			case Code.Stelem_I1:
+			case Code.Stelem_I2:
+			case Code.Stelem_I4:
+			case Code.Stelem_I8:
+			case Code.Stelem_R4:
+			case Code.Stelem_R8:
+			case Code.Stelem_Ref:
+			case Code.Stelem_Any:
+				outFrame.PopStack (3);
+				break;
+
+			case Code.Arglist:
+			case Code.Sizeof:
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+			case Code.Mkrefany:
+			case Code.Refanyval:
+			case Code.Refanytype:
+				outFrame.PopStack();
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+
+			/* Prefixes */
+			case Code.Unaligned:
+			case Code.Volatile:
+			case Code.Tail:
+				break;
+
+			/* Effect-free instructions */
+			case Code.Nop:
+			case Code.Break:
+				break;
+
+			/* Load constant */
+			/* Push non-ref. */
+			case Code.Ldc_I4_M1:
+			case Code.Ldc_I4_0:
+			case Code.Ldc_I4_1:
+			case Code.Ldc_I4_2:
+			case Code.Ldc_I4_3:
+			case Code.Ldc_I4_4:
+			case Code.Ldc_I4_5:
+			case Code.Ldc_I4_6:
+			case Code.Ldc_I4_7:
+			case Code.Ldc_I4_8:
+			case Code.Ldc_I4_S:
+			case Code.Ldc_I4:
+			case Code.Ldc_I8:
+			case Code.Ldc_R4:
+			case Code.Ldc_R8:
+				outFrame.PushStack (Nullity.NonNull);
+				break;
+
+			/* Unconditional control flow */
+			/* Do nothing */
+			case Code.Br:
+			case Code.Br_S:
+				break;
+
+			/* Conditional branches */
+			/* Pop 1 */
+			case Code.Brfalse:
+			case Code.Brtrue:
+			case Code.Brfalse_S:
+			case Code.Brtrue_S:
+				outFrame.PopStack ();
+				break;
+
+			/* Comparison branches */
+			/* Pop 2. */
+			case Code.Beq:
+			case Code.Bge:
+			case Code.Bgt:
+			case Code.Ble:
+			case Code.Blt:
+			case Code.Bne_Un:
+			case Code.Bge_Un:
+			case Code.Bgt_Un:
+			case Code.Ble_Un:
+			case Code.Blt_Un:
+			case Code.Beq_S:
+			case Code.Bge_S:
+			case Code.Bgt_S:
+			case Code.Ble_S:
+			case Code.Blt_S:
+			case Code.Bne_Un_S:
+			case Code.Bge_Un_S:
+			case Code.Bgt_Un_S:
+			case Code.Ble_Un_S:
+			case Code.Blt_Un_S:
+				outFrame.PopStack (2);
+				break;
+
+			case Code.Switch:
+				outFrame.PopStack();
+				break;
+
+			/* Comparisons */
+			/* Pop 2, push non-ref */
+			case Code.Ceq:
+			case Code.Cgt:
+			case Code.Cgt_Un:
+			case Code.Clt:
+			case Code.Clt_Un:
+				outFrame.PopStack(2);
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+
+			/* Arithmetic and logical binary operators */
+			/* Pop 2, push non-ref */
+			case Code.Add:
+			case Code.Sub:
+			case Code.Mul:
+			case Code.Div:
+			case Code.Div_Un:
+			case Code.Rem:
+			case Code.Rem_Un:
+			case Code.And:
+			case Code.Or:
+			case Code.Xor:
+			case Code.Shl:
+			case Code.Shr:
+			case Code.Shr_Un:
+			case Code.Add_Ovf:
+			case Code.Add_Ovf_Un:
+			case Code.Mul_Ovf:
+			case Code.Mul_Ovf_Un:
+			case Code.Sub_Ovf:
+			case Code.Sub_Ovf_Un:
+				outFrame.PopStack(2);
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+
+			/* Arithmetic and logical unary operators */
+			/* Pop 1, push non-ref */
+			case Code.Neg:
+			case Code.Not:
+				outFrame.PopStack();
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+
+			/* Conversions. */
+			/* Do nothing. */
+			case Code.Conv_I1:
+			case Code.Conv_I2:
+			case Code.Conv_I4:
+			case Code.Conv_I8:
+			case Code.Conv_R4:
+			case Code.Conv_R8:
+			case Code.Conv_U4:
+			case Code.Conv_U8:
+			case Code.Conv_U:
+			case Code.Conv_R_Un:
+			case Code.Conv_Ovf_I1_Un:
+			case Code.Conv_Ovf_I2_Un:
+			case Code.Conv_Ovf_I4_Un:
+			case Code.Conv_Ovf_I8_Un:
+			case Code.Conv_Ovf_U1_Un:
+			case Code.Conv_Ovf_U2_Un:
+			case Code.Conv_Ovf_U4_Un:
+			case Code.Conv_Ovf_U8_Un:
+			case Code.Conv_Ovf_I_Un:
+			case Code.Conv_Ovf_U_Un:
+			case Code.Conv_Ovf_I1:
+			case Code.Conv_Ovf_U1:
+			case Code.Conv_Ovf_I2:
+			case Code.Conv_Ovf_U2:
+			case Code.Conv_Ovf_I4:
+			case Code.Conv_Ovf_U4:
+			case Code.Conv_Ovf_I8:
+			case Code.Conv_Ovf_U8:
+			case Code.Conv_U2:
+			case Code.Conv_U1:
+			case Code.Conv_I:
+			case Code.Conv_Ovf_I:
+			case Code.Conv_Ovf_U:
+			case Code.Ckfinite:
+				break;
+
+			/* Unverifiable instructions. */
+			case Code.Jmp:
+				break;
+			case Code.Cpblk:
+				outFrame.PopStack (3);
+				break;
+			case Code.Initblk:
+				outFrame.PopStack (3);
+				break;
+			case Code.Localloc:
+				outFrame.PopStack();
+				outFrame.PushStack(Nullity.NonNull);
+				break;
+
+			default:
+				Console.WriteLine("Unknown instruction: {0} {1}",
+						opcode.Name, opcode.Value.ToString("X4"));
+				break;
+				} /* switch */
+			} /* for */
+
+			if (runner.VerbosityLevel > 1) {
+				Console.WriteLine ("Output frame:");
+				Console.Write (outFrame.ToString ());
+			}
+		} /* Transfer */
+
+		private void Check([NonNull]Instruction insn, bool warn, Nullity n,
+				[NonNull] string type)
+		{
+			if (!warn)
+				return;
+
+			string name = insn.Operand.ToString();
+			int nameOffset = name.LastIndexOf("::");
+			if(nameOffset != -1)
+				name = name.Substring(nameOffset + 2);
+			if(type.Equals("method")) {
+				string prefix = name.Substring(0, 4);
+				if(prefix.Equals("get_") || prefix.Equals("set_")) {
+					name = name.Substring(4);
+					type = "property";
+				}
+			}
+			if(n == Nullity.Unknown) {
+				string s = String.Format ("accessing {0} {1} from potentially null object", type, name);
+				runner.Report (method, insn, Severity.High, Confidence.Low, s);
+			} else if(n == Nullity.Null) {
+				string s = String.Format ("accessing {0} {1} from null object", type, name);
+				runner.Report (method, insn, Severity.High, Confidence.Low, s);
+			}
+		}
+
+		private void ProcessCall ([NonNull] Instruction insn, bool warn, bool indirect, [NonNull] NullDerefFrame frame)
+		{
+			IMethodSignature csig = (IMethodSignature)insn.Operand;
+			if(indirect)
+				frame.PopStack(); /* Function pointer */
+			foreach(ParameterDefinition param in csig.Parameters) {
+				Nullity n = frame.PopStack();
+				if(warn && nnaCollector.HasNonNullAttribute(method, param)) {
+					if(n == Nullity.Null) 
+						runner.Report (method, insn, Severity.High, Confidence.Low, "passing null value as argument declared non-null");
+					else if(n == Nullity.Unknown)
+						runner.Report (method, insn, Severity.High, Confidence.Low, "passing possibly null value as argument declared non-null");
+				}
+			}
+			if(csig.HasThis && !Ignoring(csig)) /* Add 'this' parameter. */
+				Check(insn, warn, frame.PopStack(), "method");
+			if(!IsVoid(csig.ReturnType.ReturnType)) {
+				if(csig.ReturnType.ReturnType.IsValueType)
+					frame.PushStack(Nullity.NonNull);
+				else if(nnaCollector.HasNonNullAttribute(csig))
+					frame.PushStack(Nullity.NonNull);
+				else
+					frame.PushStack(Nullity.Unknown);
+			}
+		}
+
+		private static bool Ignoring([NonNull] IMethodSignature msig)
+		{
+			/* FIXME: Ignoring is a temporary hack! */
+			/* Right now, it always returns false, as it should. */
+			return false;
+		}
+	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/NullDerefFrame.cs b/gendarme/rules/Gendarme.Rules.Correctness/NullDerefFrame.cs
index 3c56e3ed..8effa62d 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/NullDerefFrame.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/NullDerefFrame.cs
@@ -19,240 +19,238 @@ using Gendarme.Framework;
 
 namespace Gendarme.Rules.Correctness {
 
-public class NullDerefFrame : ICloneable {
-    [NonNull] private Nullity[] stack;
-    [NonNull] private Nullity[] locals;
-    [NonNull] private Nullity[] args;
-    [NonNull] private Runner runner;
-    int stackDepth;
+	public class NullDerefFrame : ICloneable {
+		[NonNull] private Nullity[] stack;
+		[NonNull] private Nullity[] locals;
+		[NonNull] private Nullity[] args;
+		[NonNull] private IRunner runner;
+		int stackDepth;
 
-    /* Unused   Null     NonNull  Unknown            */
-    /* -------------------------------------         */
-    /* Unused   Null     NonNull  Unknown  | Unused  */
-    /* Null     Null     Unknown  Unknown  | Null    */
-    /* NonNull  Unknown  NonNull  Unknown  | NonNull */
-    /* Unknown  Unknown  Unknown  Unknown  | Uknown  */
-    [NonNull] private static Nullity[][] lub = {
-        new Nullity[] { Nullity.Unused, Nullity.Null,
-            Nullity.NonNull, Nullity.Unknown },
-        new Nullity[] { Nullity.Null, Nullity.Null,
-            Nullity.Unknown, Nullity.Unknown },
-        new Nullity[] { Nullity.NonNull, Nullity.Unknown,
-            Nullity.NonNull, Nullity.Unknown },
-        new Nullity[] { Nullity.Unknown, Nullity.Unknown,
-            Nullity.Unknown, Nullity.Unknown },
-    };
+		/* Unused   Null	 NonNull  Unknown			*/
+		/* -------------------------------------		 */
+		/* Unused   Null	 NonNull  Unknown  | Unused  */
+		/* Null	 Null	 Unknown  Unknown  | Null	*/
+		/* NonNull  Unknown  NonNull  Unknown  | NonNull */
+		/* Unknown  Unknown  Unknown  Unknown  | Uknown  */
+		[NonNull] private static Nullity[][] lub = {
+			new Nullity[] { Nullity.Unused, Nullity.Null,
+				Nullity.NonNull, Nullity.Unknown },
+			new Nullity[] { Nullity.Null, Nullity.Null,
+				Nullity.Unknown, Nullity.Unknown },
+			new Nullity[] { Nullity.NonNull, Nullity.Unknown,
+				Nullity.NonNull, Nullity.Unknown },
+			new Nullity[] { Nullity.Unknown, Nullity.Unknown,
+				Nullity.Unknown, Nullity.Unknown },
+		};
 
-    public NullDerefFrame(int maxStackDepth, int numLocals, int numArgs,
-            bool entry, [NonNull] Runner runner)
-    {
-        int i;
+		public NullDerefFrame(int maxStackDepth, int numLocals, int numArgs, bool entry, [NonNull] IRunner runner)
+		{
+			int i;
 
-        stackDepth = 0;
-        stack = new Nullity[maxStackDepth];
-        locals = new Nullity[numLocals];
-        args = new Nullity[numArgs];
-        for(i = 0; i < maxStackDepth; i++)
-            stack[i] = Nullity.Unused;
+			stackDepth = 0;
+			stack = new Nullity[maxStackDepth];
+			locals = new Nullity[numLocals];
+			args = new Nullity[numArgs];
+			for(i = 0; i < maxStackDepth; i++)
+				stack[i] = Nullity.Unused;
 
-        if(entry) {
-            for(i = 0; i < numLocals; i++)
-                locals[i] = Nullity.Null;
-            for(i = 0; i < numArgs; i++)
-                args[i] = Nullity.Unknown;
-        } else {
-            for(i = 0; i < numLocals; i++)
-                locals[i] = Nullity.Unused;
-            for(i = 0; i < numArgs; i++)
-                args[i] = Nullity.Unused;
-        }
-        this.runner = runner;
-    }
+			if (entry) {
+				for(i = 0; i < numLocals; i++)
+					locals[i] = Nullity.Null;
+				for(i = 0; i < numArgs; i++)
+					args[i] = Nullity.Unknown;
+			} else {
+				for(i = 0; i < numLocals; i++)
+					locals[i] = Nullity.Unused;
+				for(i = 0; i < numArgs; i++)
+					args[i] = Nullity.Unused;
+			}
+			this.runner = runner;
+		}
 
-    public void PushStack(Nullity n)
-    {
-        if(stackDepth == stack.Length) {
-            throw new Exception("Nullity stack overflow");
-        }
-        /*
-        if(runner.Debug)
-            Console.WriteLine("Push: {0} {1} {2}", stackDepth,
-                    stack.Length, n);
-                    */
-        stack[stackDepth] = n;
-        stackDepth++;
-    }
+		public void PushStack (Nullity n)
+		{
+			if(stackDepth == stack.Length) {
+				throw new Exception("Nullity stack overflow");
+			}
+			/*
+			if(runner.Debug)
+				Console.WriteLine("Push: {0} {1} {2}", stackDepth,
+						stack.Length, n);
+						*/
+			stack[stackDepth] = n;
+			stackDepth++;
+		}
 
-    [NonNull]
-    public Nullity PopStack()
-    {
-        if(stackDepth == 0) {
-            throw new Exception("Nullity stack underflow");
-        }
-        /*
-        if(runner.Debug)
-            Console.WriteLine("Pop: {0} {1} {2}", stackDepth,
-                    stack.Length, stack[stackDepth - 1]);
-                    */
-        stackDepth--;
-        Nullity result = stack[stackDepth];
-        stack[stackDepth] = Nullity.Unused;
-        return result;
-    }
+		[NonNull]
+		public Nullity PopStack ()
+		{
+			if (stackDepth == 0) {
+				throw new Exception("Nullity stack underflow");
+			}
+			/*
+			if(runner.Debug)
+				Console.WriteLine("Pop: {0} {1} {2}", stackDepth,
+						stack.Length, stack[stackDepth - 1]);
+						*/
+			stackDepth--;
+			Nullity result = stack[stackDepth];
+			stack[stackDepth] = Nullity.Unused;
+			return result;
+		}
 
-    public void PopStack(int count)
-    {
-        for(int i = 0; i < count; i++)
-            PopStack();
-    }
+		public void PopStack (int count)
+		{
+			for(int i = 0; i < count; i++)
+				PopStack ();
+		}
 
-    public void EmptyStack()
-    {
-        PopStack(stackDepth);
-    }
+		public void EmptyStack ()
+		{
+			PopStack (stackDepth);
+		}
 
-    [NonNull]
-    public Nullity PeekStack()
-    {
-        if(stackDepth == 0) {
-            throw new Exception("Nullity stack underflow");
-        }
-        return stack[stackDepth - 1];
-    }
+		[NonNull]
+		public Nullity PeekStack()
+		{
+			if(stackDepth == 0) {
+				throw new Exception("Nullity stack underflow");
+			}
+			return stack[stackDepth - 1];
+		}
 
-    public void SetLocNullity(int index, Nullity n)
-    {
-        if(runner.Debug)
-            Console.WriteLine("SetLoc {0} {1} {2}", index, locals.Length, n);
-        locals[index] = n;
-    }
+		public void SetLocNullity(int index, Nullity n)
+		{
+			if(runner.VerbosityLevel > 1)
+				Console.WriteLine("SetLoc {0} {1} {2}", index, locals.Length, n);
+			locals[index] = n;
+		}
 
-    [NonNull]
-    public Nullity GetLocNullity(int index)
-    {
-        if(runner.Debug)
-            Console.WriteLine("GetLoc {0} {1} {2}", index, locals.Length,
-                    locals[index]);
-        return locals[index];
-    }
+		[NonNull]
+		public Nullity GetLocNullity(int index)
+		{
+			if (runner.VerbosityLevel > 1)
+				Console.WriteLine ("GetLoc {0} {1} {2}", index, locals.Length,
+						locals[index]);
+			return locals[index];
+		}
 
-    public void SetArgNullity(int index, Nullity n)
-    {
-        if(runner.Debug) {
-            Console.WriteLine("SetArg {0} {1} {2}", index, args.Length, n);
-            Console.Out.Flush();
-        }
-        args[index] = n;
-    }
+		public void SetArgNullity(int index, Nullity n)
+		{
+			if (runner.VerbosityLevel > 1) {
+				Console.WriteLine("SetArg {0} {1} {2}", index, args.Length, n);
+				Console.Out.Flush();
+			}
+			args[index] = n;
+		}
 
-    [NonNull]
-    public Nullity GetArgNullity(int index)
-    {
-        if(runner.Debug) {
-            Console.WriteLine("GetArg {0} {1}", index, args.Length);
-            Console.Out.Flush();
-        }
-        return args[index];
-    }
+		[NonNull]
+		public Nullity GetArgNullity(int index)
+		{
+			if (runner.VerbosityLevel > 1) {
+				Console.WriteLine("GetArg {0} {1}", index, args.Length);
+				Console.Out.Flush();
+			}
+			return args[index];
+		}
 
-    public void MergeWith([NonNull] NullDerefFrame incoming)
-    {
-        int i;
-        if(locals.Length != incoming.locals.Length ||
-                args.Length != incoming.args.Length ||
-                stack.Length != incoming.stack.Length)
-            throw new Exception("Merging incompatible frames");
+		public void MergeWith([NonNull] NullDerefFrame incoming)
+		{
+			int i;
+			if(locals.Length != incoming.locals.Length ||
+					args.Length != incoming.args.Length ||
+					stack.Length != incoming.stack.Length)
+				throw new Exception("Merging incompatible frames");
 
-        for(i = 0; i < locals.Length; i++)
-            locals[i] = MergeNullity(locals[i], incoming.locals[i]);
-        for(i = 0; i < args.Length; i++)
-            args[i] = MergeNullity(args[i], incoming.args[i]);
-        for(i = 0; i < stack.Length; i++)
-            stack[i] = MergeNullity(stack[i], incoming.stack[i]);
-        if(incoming.stackDepth > stackDepth)
-            stackDepth = incoming.stackDepth;
-    }
+			for(i = 0; i < locals.Length; i++)
+				locals[i] = MergeNullity(locals[i], incoming.locals[i]);
+			for(i = 0; i < args.Length; i++)
+				args[i] = MergeNullity(args[i], incoming.args[i]);
+			for(i = 0; i < stack.Length; i++)
+				stack[i] = MergeNullity(stack[i], incoming.stack[i]);
+			if(incoming.stackDepth > stackDepth)
+				stackDepth = incoming.stackDepth;
+		}
 
-    [NonNull]
-    public static Nullity MergeNullity(Nullity n1, Nullity n2)
-    {
-        return lub[(int)n1][(int)n2];
-    }
+		[NonNull]
+		public static Nullity MergeNullity(Nullity n1, Nullity n2)
+		{
+			return lub[(int)n1][(int)n2];
+		}
 
-    public override bool Equals(object o)
-    {
-        if(o == null)
-            return false;
-        NullDerefFrame frame = (NullDerefFrame)o;
-        if(this.stackDepth != frame.stackDepth)
-            return false;
-        if(this.stack.Length != frame.stack.Length)
-            return false;
-        if(this.args.Length != frame.args.Length)
-            return false;
-        if(this.locals.Length != frame.locals.Length)
-            return false;
-        int i;
-        for(i = 0; i < this.stack.Length; i++)
-            if(this.stack[i] != frame.stack[i])
-                return false;
-        for(i = 0; i < this.args.Length; i++)
-            if(this.args[i] != frame.args[i])
-                return false;
-        for(i = 0; i < this.locals.Length; i++)
-            if(this.locals[i] != frame.locals[i])
-                return false;
-        return true;
-    }
+		public override bool Equals(object o)
+		{
+			if(o == null)
+				return false;
+			NullDerefFrame frame = (NullDerefFrame)o;
+			if(this.stackDepth != frame.stackDepth)
+				return false;
+			if(this.stack.Length != frame.stack.Length)
+				return false;
+			if(this.args.Length != frame.args.Length)
+				return false;
+			if(this.locals.Length != frame.locals.Length)
+				return false;
+			int i;
+			for(i = 0; i < this.stack.Length; i++)
+				if(this.stack[i] != frame.stack[i])
+					return false;
+			for(i = 0; i < this.args.Length; i++)
+				if(this.args[i] != frame.args[i])
+					return false;
+			for(i = 0; i < this.locals.Length; i++)
+				if(this.locals[i] != frame.locals[i])
+					return false;
+			return true;
+		}
 
-    public override int GetHashCode()
-    {
-        /* FIXME: we can do better than this, perhaps? */
-        return base.GetHashCode();
-    }
+		public override int GetHashCode()
+		{
+			/* FIXME: we can do better than this, perhaps? */
+			return base.GetHashCode();
+		}
 
-    [NonNull]
-    public object Clone()
-    {
-        NullDerefFrame result = new NullDerefFrame(stack.Length,
-                locals.Length, args.Length, false, runner);
-        int i;
+		[NonNull]
+		public object Clone()
+		{
+			NullDerefFrame result = new NullDerefFrame(stack.Length,
+					locals.Length, args.Length, false, runner);
+			int i;
 
-        for(i = 0; i < locals.Length; i++)
-            result.locals[i] = locals[i];
-        for(i = 0; i < args.Length; i++)
-            result.args[i] = args[i];
-        for(i = 0; i < stack.Length; i++)
-            result.stack[i] = stack[i];
-        result.stackDepth = stackDepth;
-        return result;
-    }
+			for(i = 0; i < locals.Length; i++)
+				result.locals[i] = locals[i];
+			for(i = 0; i < args.Length; i++)
+				result.args[i] = args[i];
+			for(i = 0; i < stack.Length; i++)
+				result.stack[i] = stack[i];
+			result.stackDepth = stackDepth;
+			return result;
+		}
 
-    public override string ToString ()
-    {
-        StringBuilder sb = new StringBuilder ("Locals {");
-	for (int i = 0; i < locals.Length; i++) {
-		sb.Append (" ");
-		sb.Append (locals [i].ToString ());
+		public override string ToString ()
+		{
+			StringBuilder sb = new StringBuilder ("Locals {");
+			for (int i = 0; i < locals.Length; i++) {
+				sb.Append (" ");
+				sb.Append (locals [i].ToString ());
+			}
+			sb.AppendLine (" }");
+			sb.Append ("Args { ");
+			for (int i = 0; i < args.Length; i++) {
+				sb.Append (" ");
+				sb.Append (args [i].ToString ());
+			}
+			sb.AppendLine (" }");
+			sb.Append ("Stack { ");
+			for (int i = 0; i < stack.Length; i++) {
+				sb.Append (" ");
+				sb.Append (stack [i].ToString ());
+			}
+			sb.AppendLine (" }");
+			sb.Append ("stackDepth = ");
+			sb.Append (stackDepth);
+			sb.AppendLine ();
+			return sb.ToString ();
+		}
 	}
-	sb.AppendLine (" }");
-	sb.Append ("Args { ");
-	for (int i = 0; i < args.Length; i++) {
-		sb.Append (" ");
-		sb.Append (args [i].ToString ());
-	}
-	sb.AppendLine (" }");
-	sb.Append ("Stack { ");
-	for (int i = 0; i < stack.Length; i++) {
-		sb.Append (" ");
-		sb.Append (stack [i].ToString ());
-	}
-	sb.AppendLine (" }");
-	sb.Append ("stackDepth = ");
-	sb.Append (stackDepth);
-	sb.AppendLine ();
-        return sb.ToString ();
-    }
-}
-
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/NullDerefRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/NullDerefRule.cs
index 1bedac88..97c58362 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/NullDerefRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/NullDerefRule.cs
@@ -19,31 +19,29 @@ using Gendarme.Framework;
 
 namespace Gendarme.Rules.Correctness {
 
-public class NullDerefRule : IMethodRule {
-
-    public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
-    {
-        if(method.Body == null)
-            return runner.RuleSuccess;
-
-        CFG cfg = new CFG(method);
-        if(runner.Debug) {
-            cfg.PrintBasicBlocks();
-            cfg.PrintDot();
-        }
-
-        MessageCollection messages = new MessageCollection();
-        NonNullAttributeCollector nnaCollector =
-            new NonNullAttributeCollector();
-        IDataflowAnalysis analysis = new NullDerefAnalysis(method, messages,
-                nnaCollector, runner);
-        Dataflow dataflow = new Dataflow(cfg, analysis);
-        dataflow.Compute();
-        if(messages.Count > 0)
-            return messages;
-        else
-            return runner.RuleSuccess;
-    }
-}
+	[Problem ("This method, or property, might dereference a null pointer, or cause other code to do so.")]
+	[Solution ("Examine the detailed listing of problem locations, and ensure that the variables in question cannot be null.")]
+	public class NullDerefRule : Rule, IMethodRule {
+
+		public RuleResult CheckMethod (MethodDefinition method)
+		{
+			if (method.Body == null)
+				return RuleResult.DoesNotApply;
+
+			CFG cfg = new CFG (method);
+			// requires -v -v
+			if (Runner.VerbosityLevel > 1) {
+				cfg.PrintBasicBlocks ();
+				cfg.PrintDot ();
+			}
+
+			NonNullAttributeCollector nnaCollector = new NonNullAttributeCollector();
+			IDataflowAnalysis analysis = new NullDerefAnalysis (method, nnaCollector, Runner);
+
+			Dataflow dataflow = new Dataflow (cfg, analysis);
+			dataflow.Compute ();
 
+			return Runner.CurrentRuleResult;
+		}
+	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/Nullity.cs b/gendarme/rules/Gendarme.Rules.Correctness/Nullity.cs
index 690feb34..0b34fde2 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/Nullity.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/Nullity.cs
@@ -14,11 +14,10 @@
 
 namespace Gendarme.Rules.Correctness {
 
-public enum Nullity : int {
-    Unused  = 0,
-    Null    = 1,
-    NonNull = 2,
-    Unknown = 3,
-}
-
+	public enum Nullity {
+	    Unused  = 0,
+	    Null    = 1,
+	    NonNull = 2,
+	    Unknown = 3,
+	}
 }
diff --git a/gendarme/rules/Gendarme.Rules.Correctness/UseValueInPropertySetterRule.cs b/gendarme/rules/Gendarme.Rules.Correctness/UseValueInPropertySetterRule.cs
index 07995f6b..8c66c3e9 100644
--- a/gendarme/rules/Gendarme.Rules.Correctness/UseValueInPropertySetterRule.cs
+++ b/gendarme/rules/Gendarme.Rules.Correctness/UseValueInPropertySetterRule.cs
@@ -38,20 +38,20 @@ using Gendarme.Framework.Rocks;
 
 namespace Gendarme.Rules.Correctness {
 
-	public class UseValueInPropertySetterRule : IMethodRule {
+	[Problem ("This property setter doesn't use 'value'.")]
+	[Solution ("The setter should use 'value' or, if unneeded, you should consider remove the setter to reduce possible confusion.")]
+	public class UseValueInPropertySetterRule : Rule, IMethodRule {
 
-		private const string MessageString = "Property setter should use the assigned value";
-
-		public MessageCollection CheckMethod (MethodDefinition method, Runner runner)
+		public RuleResult CheckMethod (MethodDefinition method)
 		{
 			//Skip the test, instead of flooding messages
 			//in stubs or empty setters.
 			if (!method.HasBody)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// rule applies to setters methods
 			if (!method.IsSetter)
-				return runner.RuleSuccess;
+				return RuleResult.DoesNotApply;
 
 			// rule applies
 			bool flow = false;
@@ -62,13 +62,13 @@ namespace Gendarme.Rules.Correctness {
 				case Code.Ldarg_0:
 					// first argument if property is static
 					if (method.IsStatic)
-						return runner.RuleSuccess;
+						return RuleResult.Success;
 					empty = false;
 					break;
 				case Code.Ldarg_1:
 					// second argument if property is not static (instance)
 					if (!method.IsStatic)
-						return runner.RuleSuccess;
+						return RuleResult.Success;
 					empty = false;
 					break;
 				case Code.Ldarg_2:
@@ -76,19 +76,19 @@ namespace Gendarme.Rules.Correctness {
 					// this[] properties have multiple parameters
 					int index = instruction.OpCode.Code - Code.Ldarg_1;
 					if (method.Parameters [index].Name == "value")
-						return runner.RuleSuccess;
+						return RuleResult.Success;
 					empty = false;
 					break;
 				case Code.Ldarga:
 				case Code.Ldarga_S:
 					if ((instruction.Operand as ParameterDefinition).Name == "value")
-						return runner.RuleSuccess;
+						return RuleResult.Success;
 					empty = false;
 					break;
 				// check if the IL simply throws an exception
 				case Code.Throw:
 					if (!flow)
-						return runner.RuleSuccess;
+						return RuleResult.Success;
 					empty = false;
 					break;
 				case Code.Nop:
@@ -110,10 +110,10 @@ namespace Gendarme.Rules.Correctness {
 			}
 
 			if (empty)
-				return runner.RuleSuccess;
+				return RuleResult.Success;
 
-			Message message = new Message (MessageString, new Location (method), MessageType.Error);
-			return new MessageCollection (message);
+			Runner.Report (method, Severity.High, Confidence.Total, String.Empty);
+			return RuleResult.Failure;
 		}
 	}
 }