Rebase

model-checking · Nov 21, 2023 · dd0e36b · dd0e36b
1 parent b90a0eb
commit dd0e36b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 12 deletions.
diff --git a/kani-compiler/src/codegen_boogie/compiler_interface.rs b/kani-compiler/src/codegen_boogie/compiler_interface.rs
@@ -32,8 +32,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::MonoItem;
-use rustc_middle::query::{ExternProviders, Providers};
 use rustc_middle::ty::TyCtxt;
+use rustc_middle::util::Providers;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
@@ -189,10 +189,6 @@ impl CodegenBackend for BoogieCodegenBackend {
  provide::provide(providers, &self.queries.lock().unwrap());
  }
 
- fn provide_extern(&self, providers: &mut ExternProviders) {
- provide::provide_extern(providers, &self.queries.lock().unwrap());
- }
-
  fn print_version(&self) {
  println!("Kani-boogie version: {}", env!("CARGO_PKG_VERSION"));
  }
@@ -265,7 +261,7 @@ impl CodegenBackend for BoogieCodegenBackend {
  if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
  let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
  let test_model_path = &metadata.goto_file.as_ref().unwrap();
- std::fs::copy(&model_path, &test_model_path).expect(&format!(
+ std::fs::copy(&model_path, test_model_path).expect(&format!(
  "Failed to copy {} to {}",
  model_path.display(),
  test_model_path.display()

diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
@@ -5,11 +5,12 @@ use std::io::Write;
 
 use crate::kani_queries::QueryDb;
 use boogie_ast::boogie_program::{BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type};
-use rustc_middle::mir::interpret::{ConstValue, Scalar};
+use rustc_middle::mir::interpret::Scalar;
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{
- BasicBlock, BasicBlockData, BinOp, Constant, ConstantKind, HasLocalDecls, Local, LocalDecls,
- Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+ BasicBlock, BasicBlockData, BinOp, Const as mirConst, ConstOperand, ConstValue, HasLocalDecls,
+ Local, LocalDecls, Operand, Place, Rvalue, Statement, StatementKind, Terminator,
+ TerminatorKind,
 };
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
@@ -279,11 +280,11 @@ impl<'tcx> BoogieCtx<'tcx> {
  Expr::Symbol { name: format!("{local:?}") }
  }
 
- fn codegen_constant(&self, c: &Constant<'tcx>) -> Expr {
+ fn codegen_constant(&self, c: &ConstOperand<'tcx>) -> Expr {
  trace!(constant=?c, "codegen_constant");
  // TODO: monomorphize
- match c.literal {
- ConstantKind::Val(val, ty) => self.codegen_constant_value(val, ty),
+ match c.const_ {
+ mirConst::Val(val, ty) => self.codegen_constant_value(val, ty),
  _ => todo!(),
  }
  }