A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/model-checking/kani/issues/448 below:

Handle `Variant` check in projection assertion · Issue #448 · model-checking/kani · GitHub

    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.


RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4