Added more tests for Drop

[YoshikiTakashima]

Description of changes:

Kani's behavior does not change. 4 tests are added to test Kani's behavior on the Drop trait. These test enums, channels, Rc<Refcell<T>> and ownership-moving closures.

Resolved issues:

Issue #1284

Call-outs:

1. The channel test case (tests/kani/Drop/fixme_drop_after_moving_across_channel.rs) fails when kani::unwind(1) is set, and does not finish in under 10m when kani::unwind(2) is set. This will get a separate issue once merged.
2. I've placed the tests in places that I think will fit, but please object if you think the tests should be somewhere else.

Testing

• How is this change tested? All new test cases run with scripts/kani-regression.sh, also manually check that assertions are valid.

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
  • Similar level as other test cases.
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[danielsn]

LGTM, modulo comments.

Does this resolve all the open drop testing issues?

@adpaco-aws thoughts on the file name/locations for these tests?

[adpaco-aws]

I'd rather have all drop-related tests in the Drop folder so we have them all in one place. As long as their names refer to the types for which it's being tested (which they do), they're fine.

[YoshikiTakashima]

@adpaco-aws @danielsn:

• Drop related tests are placed under tests/kani/Drop.
• I'm not too familiar with the custom drop behaviors that are built in, but the existing set (including previous test cases) should cover the areas identified at the start of this week.

[adpaco-aws]

Thanks!