Add support to stack unwind panic strategy

[celinval]

Requested feature: We would like to be able to verify the logic that is triggered while unwinding a panic statement.
Use case: Programs sometimes rely on the unwind logic to ensure that there is not resource leak or persistent data inconsistency. Thus, it is important to users to be able to verify that the program will correctly handle its resource if a panic occurs.
Link to relevant documentation (Rust reference, Nomicon, RFC): N/A
Is this a breaking change?

Test case:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// We currently do not support stack unwinding panic strategy. Once we do, this testcase should
// fail during the verification with both the panic and the assertion failing.
// To run manually, execute:
// ```
// RUSTFLAGS="--C panic=unwind --crate-type lib" rmc unwind_fixme.rs  --function create
// ```
//
// compile-flags: --C panic=unwind --crate-type lib
// rmc-flags: --function create
// rmc-verify-fail

pub struct DummyResource {
    pub data: Option<String>,
}

impl Drop for DummyResource {
    fn drop(&mut self) {
        assert!(self.data.is_some(), "This should fail");
    }
}

#[no_mangle]
pub fn create(empty: bool) -> DummyResource {
    let mut dummy = DummyResource { data: None };
    if empty {
        unimplemented!("This is not supported yet");
    }
    dummy.data = Some(String::from("data"));
    dummy
}

With stack unwinding, the assertion inside the DummyResource::drop() should fail. However, with the abort strategy, the same assertion should hold.

[tedinski]

• Related: Unimplemented: catch_unwind intrinsic #267