error VC8518: Assertion 'c fits range of int8_t' did not verify.

Apr 4, 2011 at 6:36 PM

I am getting a VC8518 error with VCC 2.1.40403.0 when I attempt to cast an int parameter to a char:

#include <vcc.h>

char to_char(int c)
{
	return (char) c;
}

The error is correct, but how do I add a requirement that the int object is safely convertible to a char object?

Daniel

Apr 4, 2011 at 6:48 PM

I should add that I can use this:

_(requires -128 <= c && c <= 127)

However, a char is neither a signed nor unsigned integer type. Also, this assumes that CHAR_BIT is 8.

I am hoping that there is some special syntax, such as \in_range(c, char) or \convertible(c, char).

Apr 5, 2011 at 9:24 AM
Edited Apr 5, 2011 at 9:25 AM

I don't see the problem with the requires clause. As c is an integer it can naturally be negative. Only after you cast it to char the bit string gets a new interpretation.

But maybe there is in deed some syntactic sugar for this, however I'm not aware of it. Anyway you can still define your own C preprocessor macros to abbreviate lengthy and recurring annotations (which might be overkill in this case).

Concerning the char length I think this is fixed to 8 bits in VCC

Coordinator
Apr 5, 2011 at 11:07 AM

Indeed, chars are bound to 8bit in VCC. We do have functions in the prelude that define the ranges for the integer types, but we currently do not expose them to C, although it would be easy enought to do so. On the other hand, it should be fairly easy to write these yourself:

_(logic bool in_range_u8(\integer n) = 0 <= n && n <= 255)

void foo() {
  int i = 100;
  _(assert in_range_u8(i))
}

 

Coordinator
Apr 5, 2011 at 1:28 PM

The one below also works (taking advantage of constant propagation), it's not very nice, though :)

#include <vcc.h>

#define in_range(type,val) \
  (((type)(-1)) < 0 && \
    -((\integer)(1UI64 << (sizeof(type)*8-1))) <= ((\integer)val) && \
    ((\integer)val) < ((\integer)(1UI64 << (sizeof(type)*8-1))) || \
  ((type)(-1)) >= 0 && \
    0 <= ((\integer)val) && \
    ((\integer)val) <= ((\integer)(2*(1UI64 << (sizeof(type)*8-1))-1)))

char conv(int i)
  _(requires in_range(char,i))
{
  return (char) i;
}