#
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.
|