addSub.gold

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

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

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

addSub_driver: addSub.o addSub_driver.o
	${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}

clean:
	rm -f *.o

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

#ifndef SBV_GENERATED_addSub_HEADER_INCLUDED
#define SBV_GENERATED_addSub_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: */
void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
            SWord8 *dif);

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

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

int main(void)
{
  SWord8 sbv_driver_output_0;
  SWord8 sbv_driver_output_1;

  addSub(76, 92, &sbv_driver_output_0, &sbv_driver_output_1);

  printf("addSub(76, 92, &sum, &dif) ->\n");
  printf("  sum = %"PRIu8"\n", sbv_driver_output_0);
  printf("  dif = %"PRIu8"\n", sbv_driver_output_1);

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

#include "addSub.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 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;
}

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


void addSub(const SWord8 sbv_input_0, const SWord8 sbv_input_1,
            SWord8 *sbv_output_0, SWord8 *sbv_output_1)
{
  const SWord8 s0 = sbv_input_0;
  const SWord8 s1 = sbv_input_1;
  const SWord8 s2 = sbv_bv_u8_add(s0, s1);
  const SWord8 s3 = sbv_bv_u8_sub(s0, s1);

  *sbv_output_0 = s2;
  *sbv_output_1 = s3;
}
== END: "addSub.c" ==================