summaryrefslogtreecommitdiff
path: root/src/process_file.mli
diff options
context:
space:
mode:
authorThomas Bauereiss2017-08-08 13:21:42 +0100
committerThomas Bauereiss2017-08-08 13:55:25 +0100
commit14e0846502714ee310f4a8dad7f96e3a0d8ed8bf (patch)
treeee5a4312c63938f0bd41855196273d9f3892ebf9 /src/process_file.mli
parent20f5a64aec6db745f5418ee74b98d16c7c3e6f34 (diff)
Various fixes and improvements for the Lem pretty-printing
- Add some missing "wreg" effect annotations in the type checker - Improve pretty-printing of register type definitions: In addition to a "build" function, output an actual type definition, and some getter/setter functions for register fields - Fix a bug in sizeof rewriting that caused it to fail when rewriting nested calls of functions that contained sizeof expressions - Fix pretty-printing of user-defined union types with type variables (cf. test case option_either.sail) - Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to output more type annotations with bitvector lengths - Add (back) some support for specifying Lem bindings in val specs using "val extern ... foo = bar" - Misc bug fixes
Diffstat (limited to 'src/process_file.mli')
0 files changed, 0 insertions, 0 deletions