diff options
| author | Alasdair Armstrong | 2018-11-19 16:00:26 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-11-19 16:08:51 +0000 |
| commit | e313c717efec50676fb101df1cd399b2c376dc2b (patch) | |
| tree | 29dea585a3b474b6afe6cab7d339182949452b16 /src | |
| parent | b891846bef840ecbe5673c3b22cbd0f2cfceef0f (diff) | |
Ensure sizeof re-writing occurs for configuration registers
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 591b86a7..53a20465 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -649,6 +649,9 @@ let rewrite_sizeof (Defs defs) = LB_val (pat, exp') in (params_map, defs @ [DEF_val (LB_aux (lb', annot))]) end + | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) -> + let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in + (params_map, defs @ [DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp'), annot))]) | def -> (params_map, defs @ [def]) in |