locked
Support for enum flags RRS feed

  • Question

  • What is the level of support as of now for flags enumerations, and is that expected to improve in the future? I'm asking because some postcontitions that I wrote don't seem to be verified correctly, such as below.

    (Note that both enums (ValidationOptions and ConstraintFlags) are standard flags enums, with None being set to 0 and everything else being set to powers of 2.

     

    	// The following XOR is false. The two conditions being they wanting a result, and we giving a result.
    	Contract.Ensures(!((options & ValidationOptions.ReportResult) == 0 
    		^ ((Contract.Result<ConstraintFlags>() & ConstraintFlags.Passed) != 0
    		|| (Contract.Result<ConstraintFlags>() & ConstraintFlags.Failed) != 0)));
    
    	if ((options & ValidationOptions.ReportResult) != 0)
    		return ConstraintFlags.Failed;
    
    	return ConstraintFlags.None;
    

     

    The static checker complains about both of the return statements. It would seem that for the first return statement, from the if statement the checker would know that the first xor part is true, and then that the second xor is also true by looking at the return value, making the xor result false, which is then negated by the not. Similarly, for the second return, both parts of the xor can be shown false.

     

    Wednesday, March 24, 2010 10:14 AM

Answers

  • Hi Jamie,

      We do not have a great support for enumerations and in general for bitwise reasoning now. We are thinking to ways to improve it.

    Sorry about that,

    f

    • Proposed as answer by Francesco Logozzo Friday, April 23, 2010 11:46 PM
    • Marked as answer by Jamie550 Wednesday, April 28, 2010 3:19 PM
    Friday, April 23, 2010 11:46 PM