diff options
| author | Kathy Gray | 2014-02-18 17:13:27 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-18 17:13:42 +0000 |
| commit | 23a1cfb3f957f45d26138d4436169723beebc573 (patch) | |
| tree | 03a5263181b8c1bb0291d394e432a5341ca9f3d9 | |
| parent | 02b78a552d92582b54c78560c791bad4f1532fc1 (diff) | |
Put a plaster on bug for finding memory reading/writing operations
| -rw-r--r-- | src/lem_interp/interp.lem | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 122fd928..45396a5a 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -154,6 +154,10 @@ let rec to_memory_ops (Defs defs) = match valsp with | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id -> if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs)) + | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id _ -> + if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs)) + | VS_extern_no_rename (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id -> + if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs)) | _ -> to_memory_ops (Defs defs) end | _ -> to_memory_ops (Defs defs) end end |