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
. 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
structures, normal code usually doesn't have it. Note that
s are supported in general, and in fact are no different from the regular