Clarify binding levels in BodyTransCtx

AeneasVerif · Dec 13, 2024 · 3b50570 · 3b50570
1 parent 879e38f
commit 3b50570
Show file tree

Hide file tree

Showing 6 changed files with 273 additions and 272 deletions.
diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs
@@ -149,21 +149,19 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 let arg = self.translate_constant_expr_to_constant_expr(span, arg)?;
                 RawConstantExpr::MutPtr(Box::new(arg))
             }
-            ConstantExprKind::ConstRef { id } => {
-                let var_id = self.const_generic_vars_map.get(&id.index);
-                if let Some(var_id) = var_id {
-                    RawConstantExpr::Var(ConstGenericDbVar::free(*var_id))
-                } else {
+            ConstantExprKind::ConstRef { id } => match self.lookup_const_generic_var(id) {
+                Some(var) => RawConstantExpr::Var(var),
+                None => {
                     error_or_panic!(
                         self,
                         span,
                         &format!(
-                            "Unexpected error: could not find the const var generic of index {}",
-                            id.index
+                            "Unexpected error: could not find the const generic variable {}",
+                            id.name
                         )
                     )
                 }
-            }
+            },
             ConstantExprKind::FnPtr {
                 def_id: fn_id,
                 generics: substs,