Skip to content

Commit 31acdb2

Browse files
danielsntedinski
authored andcommitted
Decouple RMC from llvm crate (rust-lang#510)
1 parent 527970c commit 31acdb2

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

63 files changed

+147
-73
lines changed

Cargo.lock

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3734,6 +3734,36 @@ dependencies = [
37343734
[[package]]
37353735
name = "rustc_codegen_llvm"
37363736
version = "0.0.0"
3737+
dependencies = [
3738+
"bitflags",
3739+
"cstr",
3740+
"libc",
3741+
"measureme",
3742+
"rustc-demangle",
3743+
"rustc_arena",
3744+
"rustc_ast",
3745+
"rustc_attr",
3746+
"rustc_codegen_ssa",
3747+
"rustc_data_structures",
3748+
"rustc_errors",
3749+
"rustc_fs_util",
3750+
"rustc_hir",
3751+
"rustc_index",
3752+
"rustc_llvm",
3753+
"rustc_metadata",
3754+
"rustc_middle",
3755+
"rustc_serialize",
3756+
"rustc_session",
3757+
"rustc_span",
3758+
"rustc_target",
3759+
"smallvec",
3760+
"snap",
3761+
"tracing",
3762+
]
3763+
3764+
[[package]]
3765+
name = "rustc_codegen_rmc"
3766+
version = "0.0.0"
37373767
dependencies = [
37383768
"bitflags",
37393769
"cstr",
@@ -4030,6 +4060,7 @@ dependencies = [
40304060
"rustc_borrowck",
40314061
"rustc_builtin_macros",
40324062
"rustc_codegen_llvm",
4063+
"rustc_codegen_rmc",
40334064
"rustc_codegen_ssa",
40344065
"rustc_const_eval",
40354066
"rustc_data_structures",

compiler/rustc_codegen_llvm/Cargo.toml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,14 @@ version = "0.0.0"
44
edition = "2018"
55

66
[lib]
7-
test = true
7+
test = false
88
doctest = false
99

1010
[dependencies]
1111
bitflags = "1.0"
1212
cstr = "0.2"
1313
libc = "0.2"
1414
measureme = "9.1.0"
15-
num = "0.4.0"
1615
snap = "1"
1716
tracing = "0.1"
1817
rustc_middle = { path = "../rustc_middle" }

compiler/rustc_codegen_llvm/src/gotoc/mod.rs

Lines changed: 0 additions & 6 deletions
This file was deleted.

compiler/rustc_codegen_llvm/src/lib.rs

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,6 @@
1313
#![feature(iter_zip)]
1414
#![feature(nll)]
1515
#![recursion_limit = "256"]
16-
#![feature(destructuring_assignment)]
17-
#![feature(box_patterns)]
18-
#![feature(once_cell)]
1916

2017
use back::write::{create_informational_target_machine, create_target_machine};
2118

@@ -76,8 +73,6 @@ mod type_of;
7673
mod va_arg;
7774
mod value;
7875

79-
pub mod gotoc;
80-
8176
#[derive(Clone)]
8277
pub struct LlvmCodegenBackend(());
8378

compiler/rustc_codegen_rmc/Cargo.toml

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
[package]
5+
name = "rustc_codegen_rmc"
6+
version = "0.0.0"
7+
edition = "2018"
8+
9+
[lib]
10+
test = true
11+
doctest = false
12+
13+
[dependencies]
14+
bitflags = "1.0"
15+
cstr = "0.2"
16+
libc = "0.2"
17+
measureme = "9.1.0"
18+
num = "0.4.0"
19+
snap = "1"
20+
tracing = "0.1"
21+
rustc_middle = { path = "../rustc_middle" }
22+
rustc-demangle = "0.1.21"
23+
rustc_arena = { path = "../rustc_arena" }
24+
rustc_attr = { path = "../rustc_attr" }
25+
rustc_codegen_ssa = { path = "../rustc_codegen_ssa" }
26+
rustc_data_structures = { path = "../rustc_data_structures" }
27+
rustc_errors = { path = "../rustc_errors" }
28+
rustc_fs_util = { path = "../rustc_fs_util" }
29+
rustc_hir = { path = "../rustc_hir" }
30+
rustc_index = { path = "../rustc_index" }
31+
rustc_llvm = { path = "../rustc_llvm" }
32+
rustc_metadata = { path = "../rustc_metadata" }
33+
rustc_session = { path = "../rustc_session" }
34+
rustc_serialize = { path = "../rustc_serialize" }
35+
rustc_target = { path = "../rustc_target" }
36+
smallvec = { version = "1.6.1", features = ["union", "may_dangle"] }
37+
rustc_ast = { path = "../rustc_ast" }
38+
rustc_span = { path = "../rustc_span" }
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
use std::ops::{BitAnd, Shl, Shr};
55

66
use super::super::Transformer;
7-
use crate::gotoc::cbmc::goto_program::{
7+
use crate::cbmc::goto_program::{
88
BinaryOperand, CIntType, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, SymbolValues,
99
Type,
1010
};
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
use super::super::Transformer;
5-
use crate::gotoc::cbmc::goto_program::{
5+
use crate::cbmc::goto_program::{
66
DatatypeComponent, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, Type,
77
};
88
use rustc_data_structures::fx::{FxHashMap, FxHashSet};
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
use super::super::Transformer;
5-
use crate::gotoc::cbmc::goto_program::{Expr, Location, Stmt, Symbol, SymbolTable, Type};
5+
use crate::cbmc::goto_program::{Expr, Location, Stmt, Symbol, SymbolTable, Type};
66
use rustc_data_structures::fx::FxHashMap;
77

88
/// Struct for handling the nondet transformations for --gen-c-runnable.
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
use super::Transformer;
5-
use crate::gotoc::cbmc::goto_program::SymbolTable;
5+
use crate::cbmc::goto_program::SymbolTable;
66

77
/// Struct for performing the identity transformation on a symbol table.
88
/// Mainly used as a demo/for testing.

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/passes.rs renamed to compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/passes.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
use super::gen_c_transformer::{ExprTransformer, NameTransformer, NondetTransformer};
55
use super::identity_transformer::IdentityTransformer;
6-
use crate::gotoc::cbmc::goto_program::SymbolTable;
6+
use crate::cbmc::goto_program::SymbolTable;
77

88
/// Performs each pass provided on the given symbol table.
99
pub fn do_passes(mut symtab: SymbolTable, pass_names: &[String]) -> SymbolTable {

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs renamed to compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/transformer.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
use crate::gotoc::cbmc::goto_program::{
4+
use crate::cbmc::goto_program::{
55
BinaryOperand, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter, SelfOperand,
66
Stmt, StmtBody, SwitchCase, Symbol, SymbolTable, SymbolValues, Type, UnaryOperand,
77
};

compiler/rustc_codegen_rmc/src/lib.rs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
#![feature(bool_to_option)]
5+
#![feature(const_cstr_unchecked)]
6+
#![feature(crate_visibility_modifier)]
7+
#![feature(extern_types)]
8+
#![feature(in_band_lifetimes)]
9+
#![feature(iter_zip)]
10+
#![feature(nll)]
11+
#![recursion_limit = "256"]
12+
#![feature(destructuring_assignment)]
13+
#![feature(box_patterns)]
14+
#![feature(once_cell)]
15+
16+
pub mod cbmc;
17+
mod mir_to_goto;
18+
pub use mir_to_goto::GotocCodegenBackend;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/assumptions.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/assumptions.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
//! this module defines functions which impose data invariant on generated data types.
44
5-
use crate::gotoc::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
6-
use crate::gotoc::mir_to_goto::GotocCtx;
5+
use crate::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
6+
use crate::mir_to_goto::GotocCtx;
77
use rustc_middle::mir::interpret::{ConstValue, Scalar};
88
use rustc_middle::ty;
99
use rustc_middle::ty::layout::LayoutOf;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/block.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/block.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
//! This file contains functions related to codegenning MIR blocks into gotoc
55
6-
use crate::gotoc::mir_to_goto::GotocCtx;
6+
use crate::mir_to_goto::GotocCtx;
77
use rustc_middle::mir::{BasicBlock, BasicBlockData};
88

99
impl<'tcx> GotocCtx<'tcx> {

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/function.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/function.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33

44
//! This file contains functions related to codegenning MIR functions into gotoc
55
6-
use crate::gotoc::cbmc::goto_program::{Expr, Stmt, Symbol};
7-
use crate::gotoc::mir_to_goto::GotocCtx;
6+
use crate::cbmc::goto_program::{Expr, Stmt, Symbol};
7+
use crate::mir_to_goto::GotocCtx;
88
use rustc_middle::mir::{HasLocalDecls, Local};
99
use rustc_middle::ty::{self, Instance, TyS};
1010
use tracing::{debug, warn};

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/intrinsic.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/intrinsic.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33
//! this module handles intrinsics
44
use tracing::{debug, warn};
55

6-
use crate::gotoc::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
7-
use crate::gotoc::mir_to_goto::GotocCtx;
6+
use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
7+
use crate::mir_to_goto::GotocCtx;
88
use rustc_middle::mir::Place;
99
use rustc_middle::ty::layout::LayoutOf;
1010
use rustc_middle::ty::Instance;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/operand.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/operand.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
use crate::gotoc::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
4-
use crate::gotoc::mir_to_goto::utils::slice_fat_ptr;
5-
use crate::gotoc::mir_to_goto::GotocCtx;
3+
use crate::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
4+
use crate::mir_to_goto::utils::slice_fat_ptr;
5+
use crate::mir_to_goto::GotocCtx;
66
use rustc_ast::ast::Mutability;
77
use rustc_middle::mir::interpret::{
88
read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar,

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/place.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@
55
//! a place is an expression of specifying a location in memory, like a left value. check the cases
66
//! in [codegen_place] below.
77
8-
use crate::gotoc::cbmc::goto_program::{Expr, Type};
9-
use crate::gotoc::mir_to_goto::utils::slice_fat_ptr;
10-
use crate::gotoc::mir_to_goto::GotocCtx;
8+
use crate::cbmc::goto_program::{Expr, Type};
9+
use crate::mir_to_goto::utils::slice_fat_ptr;
10+
use crate::mir_to_goto::GotocCtx;
1111
use rustc_hir::Mutability;
1212
use rustc_middle::ty::layout::LayoutOf;
1313
use rustc_middle::{

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/rvalue.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/rvalue.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,11 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use super::typ::{is_pointer, pointee_type};
44
use crate::btree_string_map;
5-
use crate::gotoc::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
6-
use crate::gotoc::cbmc::utils::{aggr_name, BUG_REPORT_URL};
7-
use crate::gotoc::cbmc::MachineModel;
8-
use crate::gotoc::mir_to_goto::utils::{dynamic_fat_ptr, slice_fat_ptr};
9-
use crate::gotoc::mir_to_goto::GotocCtx;
5+
use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
6+
use crate::cbmc::utils::{aggr_name, BUG_REPORT_URL};
7+
use crate::cbmc::MachineModel;
8+
use crate::mir_to_goto::utils::{dynamic_fat_ptr, slice_fat_ptr};
9+
use crate::mir_to_goto::GotocCtx;
1010
use num::bigint::BigInt;
1111
use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
1212
use rustc_middle::ty::adjustment::PointerCast;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/span.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/span.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33

44
//! MIR Span related functions
55
6-
use crate::gotoc::cbmc::goto_program::Location;
7-
use crate::gotoc::mir_to_goto::GotocCtx;
6+
use crate::cbmc::goto_program::Location;
7+
use crate::mir_to_goto::GotocCtx;
88
use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
99
use rustc_span::Span;
1010

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/statement.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use super::typ::FN_RETURN_VOID_VAR_NAME;
4-
use crate::gotoc::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
5-
use crate::gotoc::mir_to_goto::GotocCtx;
4+
use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
5+
use crate::mir_to_goto::GotocCtx;
66
use rustc_hir::def_id::DefId;
77
use rustc_middle::mir;
88
use rustc_middle::mir::{

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/static_var.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/static_var.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33

44
//! This file contains functions related to codegenning MIR static variables into gotoc
55
6-
use crate::gotoc::cbmc::goto_program::Symbol;
7-
use crate::gotoc::mir_to_goto::GotocCtx;
6+
use crate::cbmc::goto_program::Symbol;
7+
use crate::mir_to_goto::GotocCtx;
88
use rustc_hir::def_id::DefId;
99
use rustc_middle::mir::mono::MonoItem;
1010
use tracing::debug;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/codegen/typ.rs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use crate::btree_map;
4-
use crate::gotoc::cbmc::goto_program::{
5-
DatatypeComponent, Expr, Parameter, Symbol, SymbolTable, Type,
6-
};
7-
use crate::gotoc::cbmc::utils::aggr_name;
8-
use crate::gotoc::mir_to_goto::GotocCtx;
4+
use crate::cbmc::goto_program::{DatatypeComponent, Expr, Parameter, Symbol, SymbolTable, Type};
5+
use crate::cbmc::utils::aggr_name;
6+
use crate::mir_to_goto::GotocCtx;
97
use rustc_ast::ast::Mutability;
108
use rustc_index::vec::IndexVec;
119
use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue};

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/compiler_interface.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/compiler_interface.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@
33

44
//! This file contains the code necessary to interface with the compiler backend
55
6-
use crate::gotoc::cbmc::goto_program::symtab_transformer;
7-
use crate::gotoc::cbmc::goto_program::SymbolTable;
8-
use crate::gotoc::mir_to_goto::overrides::skip_monomorphize;
9-
use crate::gotoc::mir_to_goto::GotocCtx;
6+
use crate::cbmc::goto_program::symtab_transformer;
7+
use crate::cbmc::goto_program::SymbolTable;
8+
use crate::mir_to_goto::overrides::skip_monomorphize;
9+
use crate::mir_to_goto::GotocCtx;
1010
use bitflags::_core::any::Any;
1111
use rustc_codegen_ssa::traits::CodegenBackend;
1212
use rustc_data_structures::fx::FxHashMap;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/current_fn.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/context/current_fn.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
use crate::gotoc::cbmc::goto_program::Stmt;
5-
use crate::gotoc::mir_to_goto::GotocCtx;
4+
use crate::cbmc::goto_program::Stmt;
5+
use crate::mir_to_goto::GotocCtx;
66
use rustc_middle::mir::BasicBlock;
77
use rustc_middle::mir::Body;
88
use rustc_middle::ty::Instance;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/goto_ctx.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/context/goto_ctx.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,13 @@
1515
//! this structure as input.
1616
1717
use super::current_fn::CurrentFnCtx;
18-
use crate::gotoc::cbmc::goto_program::{
18+
use crate::cbmc::goto_program::{
1919
DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type,
2020
};
21-
use crate::gotoc::cbmc::utils::aggr_name;
22-
use crate::gotoc::cbmc::{MachineModel, RoundingMode};
23-
use crate::gotoc::mir_to_goto::overrides::{type_and_fn_hooks, GotocHooks, GotocTypeHooks};
24-
use crate::gotoc::mir_to_goto::utils::full_crate_name;
21+
use crate::cbmc::utils::aggr_name;
22+
use crate::cbmc::{MachineModel, RoundingMode};
23+
use crate::mir_to_goto::overrides::{type_and_fn_hooks, GotocHooks, GotocTypeHooks};
24+
use crate::mir_to_goto::utils::full_crate_name;
2525
use rustc_data_structures::owning_ref::OwningRef;
2626
use rustc_data_structures::rustc_erase_owner;
2727
use rustc_data_structures::stable_map::FxHashMap;

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/overrides/hooks.rs renamed to compiler/rustc_codegen_rmc/src/mir_to_goto/overrides/hooks.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,9 @@
99
//! this module addresses this issue.
1010
1111
use super::stubs::{HashMapStub, VecStub};
12-
use crate::gotoc::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
13-
use crate::gotoc::mir_to_goto::utils::{instance_name_is, instance_name_starts_with};
14-
use crate::gotoc::mir_to_goto::GotocCtx;
12+
use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
13+
use crate::mir_to_goto::utils::{instance_name_is, instance_name_starts_with};
14+
use crate::mir_to_goto::GotocCtx;
1515
use rustc_hir::definitions::DefPathDataName;
1616
use rustc_middle::mir::{BasicBlock, Place};
1717
use rustc_middle::ty::layout::LayoutOf;

0 commit comments

Comments
 (0)