popCount1.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 popCount.h
	${CC} ${CCFLAGS} -c $< -o $@

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

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 SBV_GENERATED_popCount_HEADER_INCLUDED
#define SBV_GENERATED_popCount_HEADER_INCLUDED


#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <math.h>

/* Floating-point calling convention:
 * Enter generated code in FE_TONEAREST (round-to-nearest, ties-to-even).
 * Callbacks must preserve this mode before returning or re-entering.
 * Generated code does not check or change the hardware rounding mode.
 * Custom builds must disable implicit FP contraction, including at LTO link time.
 */

/* The boolean type */
typedef bool SBool;

/* The float type */
typedef float SFloat;

/* The double type */
typedef double SDouble;

/* Unsigned bit-vectors */
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 /* SBV_GENERATED_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 <stdio.h>
#include "popCount.h"

int main(void)
{
  const SWord8 sbv_result = popCount(0x0123456789abcdefULL);

  printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", sbv_result);

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

#include "popCount.h"

/* Exact bit-vector runtime. All arithmetic is modulo the declared width. */
#ifndef SBV_CGEN_UNUSED
#if defined(__GNUC__) || defined(__clang__)
#define SBV_CGEN_UNUSED __attribute__((unused))
#else
#define SBV_CGEN_UNUSED
#endif
#endif

static inline SBV_CGEN_UNUSED SWord64 sbv_bv_u64_shl(SWord64 a, SWord64 amount)
{
  const uint64_t n = (uint64_t) (SWord64) amount;
  const SWord64 result = n >= 64 ? (SWord64) 0 : (SWord64) ((uint64_t) (SWord64) a << n);
  return result;
}

static inline SBV_CGEN_UNUSED SWord64 sbv_bv_u64_lshr(SWord64 a, SWord64 amount)
{
  const uint64_t n = (uint64_t) (SWord64) amount;
  return n >= 64 ? (SWord64) 0 : (SWord64) ((uint64_t) (SWord64) a >> n);
}

static inline SBV_CGEN_UNUSED SWord8 sbv_bv_u8_add(SWord8 a, SWord8 b)
{
  const SWord8 bits = (SWord8) ((((uint64_t) (SWord8) a) + ((uint64_t) (SWord8) b)) & UINT64_C(0x00000000000000ff));
  return (SWord8) bits;
}


SWord8 popCount(const SWord64 sbv_input_0)
{
  const SWord64 s0 = sbv_input_0;
  const SWord64 s11 = s0 & 0x00000000000000ffULL;
  const SWord64 s14 = sbv_bv_u64_lshr(s0, 0x0000000000000008ULL);
  const SWord64 s15 = 0x00000000000000ffULL & s14;
  const SWord64 s18 = sbv_bv_u64_lshr(s14, 0x0000000000000008ULL);
  const SWord64 s19 = 0x00000000000000ffULL & s18;
  const SWord64 s22 = sbv_bv_u64_lshr(s18, 0x0000000000000008ULL);
  const SWord64 s23 = 0x00000000000000ffULL & s22;
  const SWord64 s26 = sbv_bv_u64_lshr(s22, 0x0000000000000008ULL);
  const SWord64 s27 = 0x00000000000000ffULL & s26;
  const SWord64 s30 = sbv_bv_u64_lshr(s26, 0x0000000000000008ULL);
  const SWord64 s31 = 0x00000000000000ffULL & s30;
  const SWord64 s34 = sbv_bv_u64_lshr(s30, 0x0000000000000008ULL);
  const SWord64 s35 = 0x00000000000000ffULL & s34;
  const SWord64 s38 = sbv_bv_u64_lshr(s34, 0x0000000000000008ULL);
  const SWord64 s39 = 0x00000000000000ffULL & s38;
        SWord8  s12;
        SWord8  s16;
        SWord8  s17;
        SWord8  s20;
        SWord8  s21;
        SWord8  s24;
        SWord8  s25;
        SWord8  s28;
        SWord8  s29;
        SWord8  s32;
        SWord8  s33;
        SWord8  s36;
        SWord8  s37;
        SWord8  s40;
        SWord8  s41;
  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
  };
  s12 = table0[s11];
  s16 = table0[s15];
  s17 = sbv_bv_u8_add(s12, s16);
  s20 = table0[s19];
  s21 = sbv_bv_u8_add(s17, s20);
  s24 = table0[s23];
  s25 = sbv_bv_u8_add(s21, s24);
  s28 = table0[s27];
  s29 = sbv_bv_u8_add(s25, s28);
  s32 = table0[s31];
  s33 = sbv_bv_u8_add(s29, s32);
  s36 = table0[s35];
  s37 = sbv_bv_u8_add(s33, s36);
  s40 = table0[s39];
  s41 = sbv_bv_u8_add(s37, s40);

  return s41;
}
== END: "popCount.c" ==================