creusot
creusot copied to clipboard
Unsafe checker
Creusot can't actually verify unsafe code. For the moment, when you attempt to perform an 'unsafe operation' (raw pointer stuff, etc), an error is printed about how this operation is unsupported. Instead, we should check if a function contains unsafe code at all and just abort compilation, reporting a helpful message about unsafety.
This is a bool field on basic blocks so it shouldn't be hard to check