I'm reading the code in check.ml
for my own understanding (I haven't done any tests), so this could be incorrect, but I noticed something odd:
The definition v_libraryobjs
is used to validate the library_objects
type in check.ml, but these types are significantly different. The one in check.ml
uses Dyn
while v_libraryobjs
has a more precise type, but even before that it seems that check.ml
thinks the list elements have type Id.t * obj
while values.ml says the elements have type v_libobjt
which is a sum type and would presumably not match the structure of a tuple in most situations.
another bug: v_level
says it has 3 constant constructors (SProp
, Prop
, Set
) but the actual type only has one (Set
) and the other two are missing for some reason
v_retro_action
has 3 constructors but Retroknowledge.action
has 2
v_libraryobjs is correct and Check.library_objects is incorrect, but this doesn't lead to an observable bug because the checker doesn't actually use it (we could and probably should make Check.library_objects an abstract type)
the other 2 probably can lead to segfaults on crafted .vo files
we should probably figure out some way to generate values.ml
from the types we check but no work has been done on this
found another one, v_library_info
has 2 variants but LibraryInfo.t
has 1 (and the Deprecation
variant has the wrong tag)
v_libsum has 4 fields but Check.summary_disk only has 3 (the last one is where libraryinfo should be) x_x
also v_library_info changed recently, it looks correct now
Last updated: Oct 13 2024 at 01:02 UTC