summaryrefslogtreecommitdiff
path: root/src/anf.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-02-20 14:18:49 +0000
committerAlasdair Armstrong2019-02-20 14:21:23 +0000
commita45ce2aecdd27de565dd32d42c8c79d10e2edd0a (patch)
tree379ef84eae44cb28ce8b6730f94a2f82f780bd04 /src/anf.ml
parentfc7d360e9442ab2e945e0d2da97faaf0eefec66f (diff)
Remove dead branches when compiling to C
Specifically remove branches where flow-typing implies false, as this allows the optimizer to prove anything, which can result in nonsense code. This does incur something of a performance hit.
Diffstat (limited to 'src/anf.ml')
-rw-r--r--src/anf.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/anf.ml b/src/anf.ml
index 38c77e0b..5db836e9 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -436,6 +436,8 @@ and pp_aval = function
let ae_lit lit typ = AE_val (AV_lit (lit, typ))
+let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false
+
(** GLOBAL: gensym_counter is used to generate fresh identifiers where
needed. It should be safe to reset between top level
definitions. **)