Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Handle Variant check in projection assertion #448

Open
avanhatt opened this issue Aug 23, 2021 · 2 comments
Open

Handle Variant check in projection assertion #448

avanhatt opened this issue Aug 23, 2021 · 2 comments
Assignees
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@avanhatt
Copy link
Contributor

In checking a projections type, we have this comment:

    fn check_expr_typ_mismatch(
        expr: &Expr,
        typ: &TypeOrVariant<'tcx>,
        ctx: &mut GotocCtx<'tcx>,
    ) -> Option<(Type, Type)> {
        match typ {
            TypeOrVariant::Type(t) => {
                let expr_ty = expr.typ().clone();
                let type_from_mir = ctx.codegen_ty(t);
                if expr_ty != type_from_mir { Some((expr_ty, type_from_mir)) } else { None }
            }
            // TODO: handle Variant
            TypeOrVariant::Variant(_) => None,
        }
    }

Creating a tracking issue for the variant case.

@avanhatt avanhatt added the [C] Bug This is a bug. Something isn't working. label Aug 23, 2021
celinval pushed a commit to celinval/kani-dev that referenced this issue Nov 10, 2021
ARMv6K Horizon OS panic change

After a small change to `backtrace-rs` ([model-checking#448](rust-lang/backtrace-rs#448)), `PanicStrategy::Unwind` is now fully supported.
@celinval
Copy link
Contributor

Note to self: refactor the logic here a bit and handle Variant separate from Type. In order to check the Variant, we need more information than provided here.

@fzaiser
Copy link
Contributor

fzaiser commented Jul 20, 2022

As of #1378, there is now a generator variant: TypeOrVariant::GeneratorVariant that needs to be handled too.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Development

No branches or pull requests

4 participants