Unsupported C Features

Unfortunately there is still a number of C features, which are as of yet unsupported by VCC.

Floating point numbers

VCC currently only treats floating point numbers as abstract types with uninterpreted operations (i.e., you cannot deduce x > 0 && y > 0 ==> x + y > 0, or something like that). There are more level of supports possible:
  • the same as above plus some axioms
  • full decision procedure support

The last option is unlikely in near future.

Compiler Intrinsic Type

Like __m128. They don't seem like much of work, except for the number of types and operations required.

Irreducible Control Flow Graphs

These are not supported by Boogie. This occurs with really funny goto structures, normal code usually doesn't have it. Note that gotos are supported in general, and in fact are no different from the regular for/while loops.

Last edited Oct 16, 2009 at 3:06 PM by MarkHillebrand, version 4


No comments yet.