diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/state.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/state.ml b/src/state.ml index 40ec80ad..59fb9995 100644 --- a/src/state.ml +++ b/src/state.ml @@ -242,6 +242,9 @@ let register_refs_lem mwords registers = in separate hardline [generic_convs; refs; getters_setters] +(* TODO Generate well-typedness predicate for register states (and events), + asserting that all lists representing non-bit-vectors have the right length. *) + let generate_isa_lemmas mwords (Defs defs : tannot defs) = let rec drop_while f = function | x :: xs when f x -> drop_while f xs |