| #
8e7c55c1 |
|
11-Jul-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Handling of AsmStmt in c-parser, more tests.
The C-parser contains a full parser for __asm__ syntax but
up until now hasn't done anything with it. Instead we export
some semantics. It's unspecified exactly what these semantics
are but they are parametrised with the __asm__ semantics that
went in to them, so the translation validation has something
to reason about.
Tweak modifies proofs as a result, and add some more test files.
|