acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Modifiable lvalue #13

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

In the definition of modifiable lvalue, there should be an example for the distinction between lvalue and modifiable lvalue.

In particular, can \result be considered as a modifiable lvalue, i.e. is it possible to write something like assigns \result.a from i = i;?