Verify that coq instance of `the_dead_constant` is not a bug

OCamlPro / flambda-task-force

13 stars 1 forks source link

Verify that coq instance of `the_dead_constant` is not a bug #131

Open chambart opened 8 years ago

chambart commented 8 years ago

Coq built with -O3 has an instance of a constant access to a field of a non block.

This can be

Some untyped (or GADT) dead code
Some bug in the compiler
Some Obj.magic related bug

I wish it to be the first case, but we need to ensure that this isn't any of the others

DemiMarie commented 3 years ago

Coq extracts to (essentially) the untyped lambda calculus, so this is not surprising. Coq would probably prefer ocamlopt to prune this branch as having undefined behavior.