How to add two uint16_t numbers?

[necto]

Hello, I am working with uint16_t numbers. And I am trying simple arithmetic:

#include <stdint.h>

int to_verify()
//@ requires true;
//@ ensures true;
{
  uint16_t x = 1;
  uint16_t y = 38;
  uint16_t z = x + y; //<-- This does not work
}

➡️ Type mismatch. Actual: uint32. Expected: uint16.

How do I compute sum of two short numbers so that VeriFast accepts it?

[btj]

For now, VeriFast requires that you insert a cast:

uint16_t z = (uint16_t)(x + y);

[necto]

It does not work. The current VeriFast master branch gives another error:
➡️ No such variable, constructor, regular function, predicate, enum element, global variable, or module: uint16_t
for

#include <stdint.h>

int to_verify()
//@ requires true;
//@ ensures true;
{
  uint16_t x = 1;
  uint16_t y = 38;
  uint16_t z = (uint16_t)(x + y); //<-- for this line
}

[btj]

Ah, yes. The parsing of casts is brittle. This should work:

uint16_t z = (unsigned short)(x + y);

[necto]

That works. Thank you.

[btj]

Update: Commit 9e8b145 fixes the cast parsing problem. (But a cast is still needed.)