model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.04k stars 85 forks source link

Handle `Variant` check in projection assertion #448

Open avanhatt opened 2 years ago

avanhatt commented 2 years ago

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.

celinval commented 2 years ago

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 commented 1 year ago

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