packages feed

sbv-14.8: SBVTestSuite/GoldFiles/crcUSB5_1.gold

== BEGIN: "Makefile" ================
# Makefile for crcUSB5. 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: crcUSB5_driver

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

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

crcUSB5_driver: crcUSB5.o crcUSB5_driver.o
	${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}

clean:
	rm -f *.o

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

#ifndef SBV_GENERATED_crcUSB5_HEADER_INCLUDED
#define SBV_GENERATED_crcUSB5_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: */
SWord16 crcUSB5(const SWord16 msg);

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

#include <stdio.h>
#include "crcUSB5.h"

int main(void)
{
  const SWord16 sbv_result = crcUSB5(0xfedcU);

  printf("crcUSB5(0xfedcU) = 0x%04"PRIx16"U\n", sbv_result);

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

#include "crcUSB5.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 SBool sbv_bv_extract_u16_10_10_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 10)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_9_9_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 9)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_8_8_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 8)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_7_7_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 7)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_6_6_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 6)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_5_5_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 5)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_4_4_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 4)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_3_3_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 3)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_2_2_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 2)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_1_1_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 1)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}

static inline SBV_CGEN_UNUSED SBool sbv_bv_extract_u16_0_0_u1(SWord16 a)
{
  SBool r = (SBool) 0;
  uint64_t i;
  for (i = 0; i < 1; ++i) { r = (SBool) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i)) & UINT64_C(1)) != 0) << (i))); }
  return r;
}


SWord16 crcUSB5(const SWord16 sbv_input_0)
{
  const SWord16 s0 = sbv_input_0;
  const SBool   s1 = sbv_bv_extract_u16_10_10_u1(s0);
  const SBool   s3 = s1 != false;
  const SBool   s4 = sbv_bv_extract_u16_9_9_u1(s0);
  const SBool   s5 = false != s4;
  const SBool   s6 = sbv_bv_extract_u16_8_8_u1(s0);
  const SBool   s7 = false != s6;
  const SBool   s8 = sbv_bv_extract_u16_7_7_u1(s0);
  const SBool   s9 = false != s8;
  const SBool   s10 = sbv_bv_extract_u16_6_6_u1(s0);
  const SBool   s11 = false != s10;
  const SBool   s12 = sbv_bv_extract_u16_5_5_u1(s0);
  const SBool   s13 = false != s12;
  const SBool   s14 = sbv_bv_extract_u16_4_4_u1(s0);
  const SBool   s15 = false != s14;
  const SBool   s16 = sbv_bv_extract_u16_3_3_u1(s0);
  const SBool   s17 = false != s16;
  const SBool   s18 = sbv_bv_extract_u16_2_2_u1(s0);
  const SBool   s19 = false != s18;
  const SBool   s20 = sbv_bv_extract_u16_1_1_u1(s0);
  const SBool   s21 = false != s20;
  const SBool   s22 = sbv_bv_extract_u16_0_0_u1(s0);
  const SBool   s23 = false != s22;
  const SBool   s24 = !s9;
  const SBool   s25 = s3 ? s24 : s9;
  const SBool   s26 = !s11;
  const SBool   s27 = s5 ? s26 : s11;
  const SBool   s28 = !s13;
  const SBool   s29 = s3 ? s28 : s13;
  const SBool   s30 = !s29;
  const SBool   s31 = s7 ? s30 : s29;
  const SBool   s32 = !s15;
  const SBool   s33 = s5 ? s32 : s15;
  const SBool   s34 = !s33;
  const SBool   s35 = s25 ? s34 : s33;
  const SBool   s36 = !s17;
  const SBool   s37 = s7 ? s36 : s17;
  const SBool   s38 = !s37;
  const SBool   s39 = s27 ? s38 : s37;
  const SBool   s40 = !s19;
  const SBool   s41 = s25 ? s40 : s19;
  const SBool   s42 = !s41;
  const SBool   s43 = s31 ? s42 : s41;
  const SBool   s44 = !s21;
  const SBool   s45 = s27 ? s44 : s21;
  const SBool   s46 = !s45;
  const SBool   s47 = s35 ? s46 : s45;
  const SBool   s48 = !s23;
  const SBool   s49 = s31 ? s48 : s23;
  const SBool   s50 = !s49;
  const SBool   s51 = s39 ? s50 : s49;
  const SBool   s52 = !s35;
  const SBool   s53 = s43 ? s52 : s35;
  const SBool   s54 = !s39;
  const SBool   s55 = s47 ? s54 : s39;
  const SBool   s56 = !s43;
  const SBool   s57 = s51 ? s56 : s43;
  const SWord16 s60 = s51 ? 0x0001U : 0x0000U;
  const SWord16 s62 = s60 | 0x0002U;
  const SWord16 s63 = s47 ? s62 : s60;
  const SWord16 s65 = s63 | 0x0004U;
  const SWord16 s66 = s57 ? s65 : s63;
  const SWord16 s68 = s66 | 0x0008U;
  const SWord16 s69 = s55 ? s68 : s66;
  const SWord16 s71 = s69 | 0x0010U;
  const SWord16 s72 = s53 ? s71 : s69;
  const SWord16 s74 = s72 | 0x0020U;
  const SWord16 s75 = s23 ? s74 : s72;
  const SWord16 s77 = s75 | 0x0040U;
  const SWord16 s78 = s21 ? s77 : s75;
  const SWord16 s80 = s78 | 0x0080U;
  const SWord16 s81 = s19 ? s80 : s78;
  const SWord16 s83 = s81 | 0x0100U;
  const SWord16 s84 = s17 ? s83 : s81;
  const SWord16 s86 = s84 | 0x0200U;
  const SWord16 s87 = s15 ? s86 : s84;
  const SWord16 s89 = s87 | 0x0400U;
  const SWord16 s90 = s13 ? s89 : s87;
  const SWord16 s92 = s90 | 0x0800U;
  const SWord16 s93 = s11 ? s92 : s90;
  const SWord16 s95 = s93 | 0x1000U;
  const SWord16 s96 = s9 ? s95 : s93;
  const SWord16 s98 = s96 | 0x2000U;
  const SWord16 s99 = s7 ? s98 : s96;
  const SWord16 s101 = s99 | 0x4000U;
  const SWord16 s102 = s5 ? s101 : s99;
  const SWord16 s104 = s102 | 0x8000U;
  const SWord16 s105 = s3 ? s104 : s102;

  return s105;
}
== END: "crcUSB5.c" ==================