@requires semantics for VM flags

[David Holmes]

Ping!

Thanks,
David

On 7/11/2018 7:01 PM, David Holmes wrote:
> Hi,
> 
> Can you clarify the intended semantics for @requires when referencing a 
> VM flag. It seems the current behaviour is:
> 
> @requires foo -> foo must exist and == true
> @requires !foo -> foo must exist and == false
> @requires foo == true -> IF foo exists then it == true
> @requires foo == false -> IF foo exists then it == false
> 
> I would have naively expected:
> 
> @requires foo
> 
> and
> 
> @requires foo == true
> 
> to be semantically identical?
> 
> Follow up question: if there are multiple @requires are they evaluated 
> using short-circuit logic ie:
> 
> @requires vm.bits == 64
> @requires VMFlagOnlyFor64Bits
> 
> will not look for the flag if running on a 32-bit system?
> 
> Thanks,
> David