print · source · login

Léon Gondelman

Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions---so called sequence point violations''. Undefined behavior may cause a program to crash or to have arbitrary results, so it is essential to make sure that C programs are free of undefined behavior for _any_ expression evaluation order.