Skip to content

Commit

Permalink
Remove workaround in reachable_items
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Dec 8, 2023
1 parent f673e2c commit 5415041
Showing 1 changed file with 1 addition and 5 deletions.
6 changes: 1 addition & 5 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,11 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
/// instruction looking for the items that should be included in the compilation.
fn reachable_items(&mut self) {
while let Some(to_visit) = self.queue.pop() {
// TODO: This should only check is_foreign_item() or even `has_body()`.
// We need https://github.com/rust-lang/rust/pull/118681 to land first.
if !self.collected.contains(&to_visit)
&& !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id())
{
if !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) {
self.collected.insert(to_visit.clone());
let next_items = match &to_visit {
MonoItem::Fn(instance) => self.visit_fn(*instance),
Expand Down

0 comments on commit 5415041

Please sign in to comment.