Skip to content

Using f64::powi causes type error. #135

@vecchiot-aws

Description

@vecchiot-aws

I tried this code:

fn main() {
    let _x: f64 = 1.0f64.powi(2);
}

using the following command line invocation:
rmc <filename.rs>

with RMC version:

  • Branch: main-152-2021-05-18
  • Hash: 662d19b

I expect to get a VERIFICATION SUCCESSFUL, but instead, I get

thread 'rustc' panicked at 'Function call does not type check:
func: Expr { value: Symbol { identifier: "powi" }, typ: Code { parameters: [Parameter { typ: Double, identifier: None, base_name: None }, Parameter { typ: CInteger(Int), identifier: None, base_name: None }], return_type: Double }, location: Loc { file: "/Users/vecchiot/Documents/rmc/library/std/src/f64.rs", function: Some("_ZN3std3f6421_$LT$impl$u20$f64$GT$4powi17hcd722778935aab23E"), line: 305, col: Some(18) } }
args: [Expr { value: Symbol { identifier: "_ZN3std3f6421_$LT$impl$u20$f64$GT$4powi17hcd722778935aab23E::1::var_3" }, typ: Double, location: None }, Expr { value: Symbol { identifier: "_ZN3std3f6421_$LT$impl$u20$f64$GT$4powi17hcd722778935aab23E::1::var_4" }, typ: Signedbv { width: 32 }, location: None }]', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:501:9

Summary of the error: There is a type mismatch for f64::powi, which expects a CInteger but receives a i32.

To fix: Allow function calls to automatically cast between number types of the same size and signedness.

Metadata

Metadata

Assignees

Labels

[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions