A model for `char`

[suhr]

Essential for leftpad verification. I guess it makes sense to interpret it as an integer from 0 to 0x10FFFF. This allows for char ranges, for example.

[xldenis]

Essential for leftpad verification. I guess it makes sense to interpret it as an integer from 0 to 0x10FFFF. This allows for char ranges, for example.

You can define leftpad in a generic manner over any slice of type T.

I think char will require a new abstract mathematical type since we don't want to allow things like addition of characters which is ill-defined.

[xldenis]

Since we already compile char to why3 char.Char I believe the suitable model here is just the identity.

[jhjourdan]

Why3's char is unicode?

[xldenis]

No, it isn't so we won't actually be able to use it. The SMT Char is though. It's defined in SMT as a unicode string of length 1

[gmorenz]

I hit two char related panics. They're both just unimplemented branches, but since they asked me to report them and I don't see any direct mentions in the issue I thought I'd make a note here - it seems to be the relevant issue for replacing implementing them.

use creusot_contracts::trusted;

#[trusted]
fn foo() -> char {
    'a'
}

fn main() {
    // Panic 1: thread 'rustc' panicked at 'not implemented', creusot/src/translation/function/terminator.rs:313:14
    match foo() {
        'a' => (),
        _ => (),
    }

    // Panic 2: thread 'rustc' panicked at 'internal error: entered unreachable code', creusot/src/translation/fmir.rs:170:26
    22 as char;
}