#include <stdint.h>

extern "C" {
int32_t forty_two_from_cc() { return 42; }
}