Closed icosahedron closed 4 years ago
thanks for the questions
there are several ways to handle runtime errors.
the first is the standard C one you mentioned, for example fopen() which may return NULL.
fn fopen() -> int * {
}
fn main() {
let f = fopen();
let access = *f;
}
this will error in the last line, because f may be a null pointer. instead this will pass:
fn fopen() -> int * {
}
fn main() {
let f = fopen();
if f == 0 {
return;
}
static_attest(safe(f)); // this will go away when the some() theory is implemented
let access = *f;
}
you can define custom type state to indicate a return value may be several things, and then the usage of that value is only valid on one thing
theory isopen(int) -> bool;
fn fopen() -> int
model isopen(return) || return == 0
{
}
fn useme(int a)
where isopen(a)
{
}
fn main() {
let f = fopen();
if f == 0 {
return;
}
useme(f);
}
there's an err module which uses typestate to force the user to check errors on return
fn something(err::Err mut *e ) -> int
where err::checked(*e)
{
}
fn bob(err::Err mut *e )
where err::checked(*e)
{
something(e);
something(e);
}
the last line will error because the call requires err::checked, but err::check was not called in between like it should have
fn bob(err::Err mut *e )
where err::checked(*e)
{
something(e);
if err::check(e) { return }
something(e);
if err::check(e) { return }
}
err also gives you a backtrace without the need for unwind info
Thanks for the explanation. I really like option 2 with the type states. It’s like a built-in Maybe monad.
Learning how to use this and what it all means. How does ZZ handle file opens that fail?
Obviously the example using
where is_open
isn't supposed to catch that case, since that is not runtime code, so does that mean that read is still supposed to do:or similar?