Why inferring methodensures doesn't work here?


compiled option "-infer methodensures":

    class program
    {
        static void main(string[] args)
        {
            string s = test();
            contract.assert(s.length < 10); // assert unproven
        }

        static string test()
        {
            string s = new string('x', 7);
            contract.assume(s.length < 10);
            return s;
        }
    }

actually, question _inferring_ ensures. declare fact return value has length < 10. static checker doesn't automatically infers fact. think bug. if it's not bug, interesting know why fact not inferred.



DevLabs  >  Code Contracts



Comments

Popular posts from this blog

Azure DocumentDB Owner resource does not exist

job syspolicy_purge_history job fail in sqlserver 2008

Trying to register with public marketplace error with 'Get-AzureStackStampInformation'