generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 130
Open
Labels
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct
Description
Only remaining issue from #158
https://doc.rust-lang.org/std/intrinsics/fn.try.html
https://doc.rust-lang.org/src/core/intrinsics.rs.html#1717
https://doc.rust-lang.org/std/panic/fn.catch_unwind.html
try
makes a best-effort attempt to recover from panics - if the code in the first function pointer crashes with a panic, rust will try to run the cleanup code in the second function pointer.
It is not clear to me what the right semantics are here. For now, handling this as a unimplemented
allows us to soundly move forward, but it might be more accurate to actually call the first function pointer. I don't know of a nice way to do the unwinding on panic - maybe CBMC has a mechanism?
Metadata
Metadata
Assignees
Labels
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct