CompCert

CompCert copied to clipboard

aarch64 assembler error: conditional branch out of range

4

I encountered an issue when compiling [libccv](https://libccv.org/) with CompCert 3.16 on a Raspberry Pi 5 (Arm Cortex A76) running Raspberry Pi OS. Some of the functions in libccv are apparently...

bagnalla

Add support for indirect branch tracking (IBT)

6

On newer Intel x86/64 CPUs and on OpenBSD, CompCert produced binaries will crash due to lack of IBT support. As a quick solution we can append “-z nobtcfi” to clinker_options...

didickman

Support x86 Indirect Branch Tracking.

3

This PR adds support for IBT, a control-flow integrity mechanism in the x86 architecture. It adds `endbr64` instructions at function entry points, so that they can be called via a...

xavierleroy

Unexpected undefined behavior on IA32 ?

4

On architecture IA32, `./ccomp -interp` on the following program printfs `ERROR: Initial state undefined` (just tested on commit ce0f6ca). ```C typedef struct { char is_float; union { long long i;...

boulme