|
|
|---|
|
|
|
|---|
Unambiguity of the C abstract syntax for tools.
Our abstract syntax includes ambiguous constructs, i.e. constructs that capture syntactically ambiguous constructs; see the documentation of the abstract syntax for details. The disambiguator, if successful, removes those constructs, leaving only the unambiguous ones.
Here we define predicates over the abstract syntax that say whether the constructs are unambiguous, i.e. whether there are no ambiguous constructs.
For now we do not make any checks on GCC extensions, even though they may contain expressions. This mirrors the treatment in the disambiguator: the reason for this (temporary) limitation is explained there.
Besides defining the unambiguity predicates, we also provide rules to automate guard and return proofs that involve the unambiguity predicates. The rules about the fixtype deconstructors automate the guard proofs; the rules about the fixtype constructors automate the return proofs.