Contract.ForAll and multithreaded

hello,

i have encountered problem seems multithreading related when using contract.forall in postcondition of static method (at runtime).

here repo:

  namespace contractforallmultithreading  {    class program    {      static random rand = new random();        static string[] dosomething()      {        contract.ensures(contract.result<string[]>() != null);        contract.ensures(contract.forall(0, contract.result<string[]>().length, => contract.result<string[]>()[i] != null)); // crashes index out of range          int count;        lock (rand)        {          count = rand.next(0, 10);        }          string[] result = new string[count];        for (int = 0; < result.length; i++)          result[i] = string.empty;        return result;      }        static void threadpoc()      {        while (true)        {          string[] data = dosomething();          thread.sleep(0);        }      }        static void main(string[] args)      {        for (int = 0; < 4; i++)        {          thread thread = new thread(threadpoc);          thread.isbackground = true;          thread.start();        }          console.readline();      }    }  }    

here generated code:

  private static string[] dosomething()  {    int count;    lock (rand)    {      count = rand.next(0, 10);    }    string[] result = new string[count];    for (int = 0; < result.length; i++)    {      result[i] = string.empty;    }    string[] cs$1$0000 = result;    string[] contract.result = cs$1$0000;    _result173961 = contract.result; // _result173961 static field generated rewriter    if (__contractsruntime.insidecontractevaluation <= 4)    {      try      {        __contractsruntime.insidecontractevaluation++;        __contractsruntime.ensures(contract.result != null, null, "contract.result<string[]>() != null");        __contractsruntime.ensures(contract.forall(0, contract.result.length, delegate (int i) {          return _result173961[i] != null; // line not threadsafe because each returned array may have different length!        }), null, "contract.forall(0, contract.result<string[]>().length, => contract.result<string[]>()[i] != null)");      }      finally      {        __contractsruntime.insidecontractevaluation--;      }    }    return contract.result;  }         

the rewriter generates field holds return value of method.
when working multiple threads field not threadsafe , causes indexoutofrangeexception (in example).

jean-ph.

hi,

maybe rewriter marks field [threadstatic]?

DevLabs  >  Code Contracts