Skip to content

Bitvector issue with --type-system-refresh #6196

@MikaelMayer

Description

@MikaelMayer

Dafny version

Latest nightly

Code to produce this issue

newtype Uint8 = x: int | 0 <= x < 256

type CustomBv16 = bv16

method Main() {
  var x: Uint8 := 2;
  // Correct rendering of expressions that can interpret the first '<' as a generic argument
  var y: bv16 := (x as CustomBv16) << 2;
}

Command to run and resulting output

> dafny run --target=rs --enforce-determinism --type-system-refresh 

...
error[E0277]: no implementation for `u16 << DafnyInt`
  --> src\conversions.rs:57:41
   |
57 |             let mut y: u16 = (x as u16) << int!(2);
   |                                         ^^ no implementation for `u16 << DafnyInt`
   |
   = help: the trait `Shl<DafnyInt>` is not implemented for `u16`
   = help: the following other types implement trait `Shl<Rhs>`:
             `&u16` implements `Shl<&i128>`
             `&u16` implements `Shl<&i16>`
             `&u16` implements `Shl<&i32>`
             `&u16` implements `Shl<&i64>`
             `&u16` implements `Shl<&i8>`
             `&u16` implements `Shl<&isize>`
             `&u16` implements `Shl<&u128>`
             `&u16` implements `Shl<&u32>`

What happened?

This bug appeared since #5653
I nailed it down to a single line that needs to be updated. Fix will be provided soon.

What type of operating system are you experiencing the problem on?

Windows

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions