diff options
| -rw-r--r-- | src/ast_util.ml | 7 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 29 |
3 files changed, 28 insertions, 9 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 61bc9ba3..f0b6508b 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -888,6 +888,13 @@ let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux let id_of_val_spec (VS_aux (VS_val_spec (_, id, _, _), _)) = id +let id_of_dec_spec (DEC_aux (ds_aux, _)) = + match ds_aux with + | DEC_reg (_, id) -> id + | DEC_config (id, _, _) -> id + | DEC_alias (id, _) -> id + | DEC_typ_alias (_, id, _) -> id + let ids_of_def = function | DEF_kind (KD_aux (KD_nabbrev (_, id, _, _), _)) -> IdSet.singleton id | DEF_type td -> IdSet.singleton (id_of_type_def td) diff --git a/src/ast_util.mli b/src/ast_util.mli index f55cdf16..2a303475 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -232,6 +232,7 @@ val string_of_index_range : index_range -> string val id_of_fundef : 'a fundef -> id val id_of_type_def : 'a type_def -> id val id_of_val_spec : 'a val_spec -> id +val id_of_dec_spec : 'a dec_spec -> id val id_of_kid : kid -> id val kid_of_id : id -> kid diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 75f55c9c..c858754e 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -447,15 +447,26 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd else init_env name in init_env (name ^ "/end"), uses -let fv_of_rd consider_var (DEC_aux (d,_)) = match d with - | DEC_reg(t,id) -> - init_env (string_of_id id), fv_of_typ consider_var mt mt t - | DEC_config(id,t,exp) -> - init_env (string_of_id id), fv_of_typ consider_var mt mt t - | DEC_alias(id,alias) -> - init_env (string_of_id id),mt - | DEC_typ_alias(t,id,alias) -> - init_env (string_of_id id), mt +let fv_of_rd consider_var (DEC_aux (d, annot)) = + (* When we get the free variables of a register, we have to ensure + that we expand all synonyms so we can pick up dependencies with + undefined_type function, even when type is indirected through a + synonym. *) + let open Type_check in + let env = env_of_annot annot in + match d with + | DEC_reg(t, id) -> + let t' = Env.expand_synonyms env t in + init_env (string_of_id id), + Nameset.union (fv_of_typ consider_var mt mt t) (fv_of_typ consider_var mt mt t') + | DEC_config(id, t, exp) -> + let t' = Env.expand_synonyms env t in + init_env (string_of_id id), + Nameset.union (fv_of_typ consider_var mt mt t) (fv_of_typ consider_var mt mt t') + | DEC_alias(id, alias) -> + init_env (string_of_id id), mt + | DEC_typ_alias(t, id, alias) -> + init_env (string_of_id id), mt let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_kind kdef -> fv_of_kind_def consider_var kdef |