#include <stdio.h>
#include <stdint.h>

void
blend (uint32_t pixel_value_1,
                        uint32_t pixel_value_2)
{
      uint8_t alpha_1, red_1, red_2;
      uint_least16_t red;

      alpha_1 = (uint8_t) (pixel_value_1 >> 24);
      red_1 = (uint8_t) (pixel_value_1 >> 16);
      red_2 = (uint8_t) (pixel_value_2 >> 16);

      /* here red_1 and red_2 are 0x40, and we expect the result to be 7f80 */
      red = red_1 * 255 + red_2 * (255 - alpha_1);

      printf("%hx\n", red);
}

int
main(int argc, char**argv)
{
    blend(0x00404040, 0xFF404040);
    return 0;
}