This project is read-only.

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

Apr 4, 2011 at 7: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?


Apr 4, 2011 at 7: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 10:24 AM
Edited Apr 5, 2011 at 10: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

Apr 5, 2011 at 12:07 PM

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))


Apr 5, 2011 at 2: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;