sbv-7.2: SBVTestSuite/GoldFiles/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 <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <math.h>
/* 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 /* __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 __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 "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 s14 = s0 >> 8;
const SWord64 s15 = 0x00000000000000ffULL & s14;
const SWord8 s16 = s15 >= 256 ? 0 : table0[s15];
const SWord8 s17 = s12 + s16;
const SWord64 s18 = s14 >> 8;
const SWord64 s19 = 0x00000000000000ffULL & s18;
const SWord8 s20 = s19 >= 256 ? 0 : table0[s19];
const SWord8 s21 = s17 + s20;
const SWord64 s22 = s18 >> 8;
const SWord64 s23 = 0x00000000000000ffULL & s22;
const SWord8 s24 = s23 >= 256 ? 0 : table0[s23];
const SWord8 s25 = s21 + s24;
const SWord64 s26 = s22 >> 8;
const SWord64 s27 = 0x00000000000000ffULL & s26;
const SWord8 s28 = s27 >= 256 ? 0 : table0[s27];
const SWord8 s29 = s25 + s28;
const SWord64 s30 = s26 >> 8;
const SWord64 s31 = 0x00000000000000ffULL & s30;
const SWord8 s32 = s31 >= 256 ? 0 : table0[s31];
const SWord8 s33 = s29 + s32;
const SWord64 s34 = s30 >> 8;
const SWord64 s35 = 0x00000000000000ffULL & s34;
const SWord8 s36 = s35 >= 256 ? 0 : table0[s35];
const SWord8 s37 = s33 + s36;
const SWord64 s38 = s34 >> 8;
const SWord64 s39 = 0x00000000000000ffULL & s38;
const SWord8 s40 = s39 >= 256 ? 0 : table0[s39];
const SWord8 s41 = s37 + s40;
return s41;
}
== END: "popCount.c" ==================