Skip to content

Commit c14042a

Browse files
danielsntedinski
authored andcommitted
Handle ! as its own type, rather than incorrectly mapping it to void. (rust-lang#588)
1 parent 70a23a7 commit c14042a

File tree

3 files changed

+22
-7
lines changed
  • compiler
    • cbmc/src/goto_program
    • rustc_codegen_rmc/src/codegen
  • src/test/rmc/Never

3 files changed

+22
-7
lines changed

compiler/cbmc/src/goto_program/typ.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -576,9 +576,8 @@ impl Type {
576576
/// base_name: the local name of the parameter within the function `x`
577577
/// typ: The type of the parameter
578578
pub fn as_parameter(self, identifier: Option<String>, base_name: Option<String>) -> Parameter {
579-
// FIXME: https://github.com/model-checking/rmc/issues/570
580579
assert!(
581-
self.is_empty() || self.is_lvalue(),
580+
self.is_lvalue(),
582581
"Expected lvalue from {:?} {:?} {:?}",
583582
self,
584583
identifier,

compiler/rustc_codegen_rmc/src/codegen/typ.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,10 @@ use ty::layout::HasParamEnv;
3636
const UNIT_TYPE_EMPTY_STRUCT_NAME: &str = "Unit";
3737
pub const FN_RETURN_VOID_VAR_NAME: &str = "VoidUnit";
3838

39+
/// Map the never i.e. `!` type to an empty struct.
40+
/// The never type can appear as a function argument, e.g. in library/core/src/num/error.rs
41+
const NEVER_TYPE_EMPTY_STRUCT_NAME: &str = "Never";
42+
3943
pub trait TypeExt {
4044
fn is_rust_fat_ptr(&self, st: &SymbolTable) -> bool;
4145
fn is_rust_slice_fat_ptr(&self, st: &SymbolTable) -> bool;
@@ -544,11 +548,7 @@ impl<'tcx> GotocCtx<'tcx> {
544548
ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
545549
ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
546550
ty::Generator(_, subst, _) => self.codegen_ty_generator(subst),
547-
ty::Never =>
548-
// unfortunately, there is no bottom in C. We must pick a type
549-
{
550-
Type::empty()
551-
}
551+
ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, None, |_, _| vec![]),
552552
ty::Tuple(ts) => {
553553
if ts.is_empty() {
554554
self.codegen_ty_unit()

src/test/rmc/Never/main.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
#![feature(never_type)]
4+
use std::convert::Infallible;
5+
6+
/// Test using the never type
7+
pub fn foo(never: !) -> i32 {
8+
return 1;
9+
}
10+
11+
pub fn bar(infalliable: Infallible) -> i32 {
12+
return 1;
13+
}
14+
15+
// Give an empty main to make rustc happy.
16+
pub fn main() {}

0 commit comments

Comments
 (0)