diff options
| author | Thomas Bauereiss | 2017-08-08 13:21:42 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-08-08 13:55:25 +0100 |
| commit | 14e0846502714ee310f4a8dad7f96e3a0d8ed8bf (patch) | |
| tree | ee5a4312c63938f0bd41855196273d9f3892ebf9 /src/ast_util.mli | |
| parent | 20f5a64aec6db745f5418ee74b98d16c7c3e6f34 (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/ast_util.mli')
| -rw-r--r-- | src/ast_util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli index 8a07b83f..ae340839 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -120,6 +120,7 @@ end val nexp_frees : nexp -> KidSet.t val nexp_identical : nexp -> nexp -> bool val is_nexp_constant : nexp -> bool +val simplify_nexp : nexp -> nexp val is_number : typ -> bool val is_vector_typ : typ -> bool |