You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I don't think we have thoroughly tested the cast logic and we should probably revisit some assertions as well as the code structure in general. Issues I noticed while working on #1522:
Incorrect code path. E.g.: casting std::boxed::Box<dyn Byte + std::marker::Sync> to std::boxed::Box<dyn Byte> was invoking cast_sized_expr_to_unsized_expr.
Incorrect assumptions / misleading names: E.g.:
Functions like cast_sized_pointer_to_fat_pointer and cast_sized_expr_to_unsized_expr operates under the assumption that we are casting sized to unsized, but at the same time they start checking if the type of source is the same type as destination.
Function cast_sized_expr_to_unsized_expr is not necessarily casting a sized expression to an unsized expression. A big part of it does thin pointer to fat pointer conversion. Both generate pointers which are sized expressions.
Trivially true assertions and (hopefully) unreachable code paths. E.g.:
Activity
Create kani_middle module to host backend agnostic code (#1833)
Refactor coercion logic for future usage inside codegen
Refactor coercion logic for future usage inside codegen (#1837)
Fix unsized coercion of a struct element
Fix unsized coercion of a struct element (#1880)