I suggest we ...

Code Contracts support

This has been discussed but I believe it should be F# that can fix it.

F# compiler does a lot of magic. Especially if we put Contract.Requires to the beginning of a method or a constructor, F# can (if it is a constructor it will) put additional code.

There is nothing code contract team can do anything about this because this is about how F# compiler works. It basically adds code to the prologue methods and ctors. What compiler can do is to respect System.Diagnostics.Contract class and don't put any code above it.

Example:

Suppose you have this code:

type RationalEx =
val numerator : int

new(num : int) as this =
{ numerator = num }
then
Contract.Requires(this.numerator>0)
this.Check(this.numerator)

member this.Check(num:int)=
Contract.Requires(num > 0 )
()

When it is compiled and checked from reflector what you will see is

For the constructor:

public RationalEx(int num)
{
FSharpRef<Program.RationalEx> this = new FSharpRef<Program.RationalEx>(null);
base();
this.numerator@ = num;
this.contents = this;
this.init@5 = 1;
Contract.Requires(LanguagePrimitives.IntrinsicFunctions.CheckThis<Program.RationalEx>(this.contents).numerator@ > 0);
LanguagePrimitives.IntrinsicFunctions.CheckThis<Program.RationalEx>(this.contents).Check(LanguagePrimitives.IntrinsicFunctions.CheckThis<Program.RationalEx>(this.contents).numerator@);
}

and for the method

public void Check(int num)
{
if (this.init@5 < 1)
{
LanguagePrimitives.IntrinsicFunctions.FailInit();
}
Contract.Requires(num > 0);
}

as you see it adds some magic code on top of the contract code by magic. And this causes contract checker and rewriter to fail

24 votes
Vote
Sign in
Check!
(thinking…)
Reset
or sign in with
  • facebook
  • google
    Password icon
    I agree to the terms of service
    Signed in as (Sign out)
    You have left! (?) (thinking…)
    Onur shared this idea  ·   ·  Admin →

    1 comment

    Sign in
    Check!
    (thinking…)
    Reset
    or sign in with
    • facebook
    • google
      Password icon
      I agree to the terms of service
      Signed in as (Sign out)
      Submitting...
      • Don Syme commented  · 

        Why doe this require a fix in F# rather than in the Code Contracts tool?

      F# Language

      Feedback and Knowledge Base