popCount2.gold

== BEGIN: "Makefile" ================
# Makefile for popCount. Automatically generated by SBV. Do not edit!

# include any user-defined .mk file in the current directory.
-include *.mk

CC=gcc
CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer

all: popCount_driver

popCount.o: popCount.c popCount.h
	${CC} ${CCFLAGS} -c $< -o $@

popCount_driver.o: popCount_driver.c
	${CC} ${CCFLAGS} -c $< -o $@

popCount_driver: popCount.o popCount_driver.o
	${CC} ${CCFLAGS} $^ -o $@

clean:
	rm -f *.o

veryclean: clean
	rm -f popCount_driver
== END: "Makefile" ==================
== BEGIN: "popCount.h" ================
/* Header file for popCount. Automatically generated by SBV. Do not edit! */

#ifndef __popCount__HEADER_INCLUDED__
#define __popCount__HEADER_INCLUDED__

#include <inttypes.h>
#include <stdint.h>

/* Unsigned bit-vectors */
typedef uint8_t  SBool  ;
typedef uint8_t  SWord8 ;
typedef uint16_t SWord16;
typedef uint32_t SWord32;
typedef uint64_t SWord64;

/* Signed bit-vectors */
typedef int8_t  SInt8 ;
typedef int16_t SInt16;
typedef int32_t SInt32;
typedef int64_t SInt64;

/* Entry point prototype: */
SWord8 popCount(const SWord64 x);

#endif /* __popCount__HEADER_INCLUDED__ */
== END: "popCount.h" ==================
== BEGIN: "popCount_driver.c" ================
/* Example driver program for popCount. */
/* Automatically generated by SBV. Edit as you see fit! */

#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>
#include "popCount.h"

int main(void)
{
  const SWord8 __result = popCount(0x0123456789abcdefULL);
  
  printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", __result);

  return 0;
}
== END: "popCount_driver.c" ==================
== BEGIN: "popCount.c" ================
/* File: "popCount.c". Automatically generated by SBV. Do not edit! */

#include <inttypes.h>
#include <stdint.h>
#include "popCount.h"

SWord8 popCount(const SWord64 x)
{
  const SWord64 s0 = x;
  static const SWord8 table0[] = {
      0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,
      3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,
      3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,
      2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,
      3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,
      5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,
      2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,
      4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
      3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,
      4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,
      5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,
      5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8
  };
  const SWord64 s11 = s0 & 0x00000000000000ffULL;
  const SWord8  s12 = s11 >= 256 ? 0 : table0[s11];
  const SWord64 s13 = s0 >> 8;
  const SWord64 s14 = 0x00000000000000ffULL & s13;
  const SWord8  s15 = s14 >= 256 ? 0 : table0[s14];
  const SWord8  s16 = s12 + s15;
  const SWord64 s17 = s13 >> 8;
  const SWord64 s18 = 0x00000000000000ffULL & s17;
  const SWord8  s19 = s18 >= 256 ? 0 : table0[s18];
  const SWord8  s20 = s16 + s19;
  const SWord64 s21 = s17 >> 8;
  const SWord64 s22 = 0x00000000000000ffULL & s21;
  const SWord8  s23 = s22 >= 256 ? 0 : table0[s22];
  const SWord8  s24 = s20 + s23;
  const SWord64 s25 = s21 >> 8;
  const SWord64 s26 = 0x00000000000000ffULL & s25;
  const SWord8  s27 = s26 >= 256 ? 0 : table0[s26];
  const SWord8  s28 = s24 + s27;
  const SWord64 s29 = s25 >> 8;
  const SWord64 s30 = 0x00000000000000ffULL & s29;
  const SWord8  s31 = s30 >= 256 ? 0 : table0[s30];
  const SWord8  s32 = s28 + s31;
  const SWord64 s33 = s29 >> 8;
  const SWord64 s34 = 0x00000000000000ffULL & s33;
  const SWord8  s35 = s34 >= 256 ? 0 : table0[s34];
  const SWord8  s36 = s32 + s35;
  const SWord64 s37 = s33 >> 8;
  const SWord64 s38 = 0x00000000000000ffULL & s37;
  const SWord8  s39 = s38 >= 256 ? 0 : table0[s38];
  const SWord8  s40 = s36 + s39;
  
  return s40;
}
== END: "popCount.c" ==================