Profiles and new platform support

Match/C-semantics profiles

If a program is strictly-conforming, then the basic C semantics with no extensions should be enough to interpret that program and detect undefined behavior. But the reality of how C is actually used means it is much more common for programs to depend on implementation-specific details of particular hardware or software platforms. Profiles are meant to allow the interpreter generated from the C semantics to analyze programs in the context of such platform-specific behavior.

Platform-specific extensions and behavior should optimally be confined to a profile. These behaviors can broadly be understood as behaviors originating from the compiler, the operating system, or the underlying hardware. We have broken them down into more specific categories below.

• Command-line flags
• Preprocessor macros and extensions
• Implementation-specific choices
• Language extensions: pragmas, attributes
• Language extensions: built-in functions
• Language extensions: new syntax -- parser, semantics extensions
• Native execution/FFI support

State of current profile support

We currently support a few different profiles, all based on gcc and x86_64.

• x86_64 default
• x86_64 GNUC
• x86_64 limited
• x86_64 default reverse
• x86_64 GNUC reverse