From 18767e96381dc5fdd5a88fc18a355b5f67433021 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 16 Feb 2018 20:01:51 +0000 Subject: Don't generate undefined functions for generated register types --- src/state.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index 1bde448f..67eda5b8 100644 --- a/src/state.ml +++ b/src/state.ml @@ -243,6 +243,12 @@ let register_refs_lem prefix_recordtype mwords registers = separate hardline [generic_convs; refs; getters_setters] let generate_regstate_defs mwords defs = + (* FIXME We currently don't want to generate undefined_type functions + for register state and values. For the Lem backend, this would require + taking the dependencies of those functions into account when partitioning + definitions into the different lem files, which we currently don't do. *) + let gen_undef = !Initial_check.opt_undefined_gen in + Initial_check.opt_undefined_gen := false; let registers = find_registers defs in let def_ids = ids_of_defs (Defs defs) in let has_def name = IdSet.mem (mk_id name) def_ids in @@ -253,12 +259,6 @@ let generate_regstate_defs mwords defs = in let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in - (* FIXME We currently don't want to generate undefined_type functions - for register state and values. For the Lem backend, this would require - taking the dependencies of those functions into account when partitioning - definitions into the different lem files, which we currently don't do. *) - let gen_undef = !Initial_check.opt_undefined_gen in - Initial_check.opt_undefined_gen := false; let defs = option_typ @ regval_typ @ regstate_typ |> List.map defs_of_string -- cgit v1.2.3