gcd.gold

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

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

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

sgcd_driver: sgcd.o sgcd_driver.o
	${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}

clean:
	rm -f *.o

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

#ifndef SBV_GENERATED_sgcd_HEADER_INCLUDED
#define SBV_GENERATED_sgcd_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 sgcd(const SWord8 x, const SWord8 y);

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

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

int main(void)
{
  const SWord8 sbv_result = sgcd(55, 154);

  printf("sgcd(55, 154) = %"PRIu8"\n", sbv_result);

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

#include "sgcd.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_rem(SWord8 a, SWord8 b)
{
  if (b == (SWord8) 0) return a;
  return (SWord8) (a % b);
}


SWord8 sgcd(const SWord8 sbv_input_0, const SWord8 sbv_input_1)
{
  const SWord8 s0 = sbv_input_0;
  const SWord8 s1 = sbv_input_1;
  const SBool  s3 = s1 == 0;
  const SWord8 s4 = sbv_bv_u8_rem(s0, s1);
  const SWord8 s5 = s3 ? s0 : s4;
  const SBool  s6 = 0 == s5;
  const SWord8 s7 = sbv_bv_u8_rem(s1, s5);
  const SWord8 s8 = s6 ? s1 : s7;
  const SBool  s9 = 0 == s8;
  const SWord8 s10 = sbv_bv_u8_rem(s5, s8);
  const SWord8 s11 = s9 ? s5 : s10;
  const SBool  s12 = 0 == s11;
  const SWord8 s13 = sbv_bv_u8_rem(s8, s11);
  const SWord8 s14 = s12 ? s8 : s13;
  const SBool  s15 = 0 == s14;
  const SWord8 s16 = sbv_bv_u8_rem(s11, s14);
  const SWord8 s17 = s15 ? s11 : s16;
  const SBool  s18 = 0 == s17;
  const SWord8 s19 = sbv_bv_u8_rem(s14, s17);
  const SWord8 s20 = s18 ? s14 : s19;
  const SBool  s21 = 0 == s20;
  const SWord8 s22 = sbv_bv_u8_rem(s17, s20);
  const SWord8 s23 = s21 ? s17 : s22;
  const SBool  s24 = 0 == s23;
  const SWord8 s25 = sbv_bv_u8_rem(s20, s23);
  const SWord8 s26 = s24 ? s20 : s25;
  const SBool  s27 = 0 == s26;
  const SWord8 s28 = sbv_bv_u8_rem(s23, s26);
  const SWord8 s29 = s27 ? s23 : s28;
  const SBool  s30 = 0 == s29;
  const SWord8 s31 = sbv_bv_u8_rem(s26, s29);
  const SWord8 s32 = s30 ? s26 : s31;
  const SBool  s33 = 0 == s32;
  const SWord8 s34 = sbv_bv_u8_rem(s29, s32);
  const SWord8 s35 = s33 ? s29 : s34;
  const SBool  s36 = 0 == s35;
  const SWord8 s37 = s36 ? s32 : s35;
  const SWord8 s38 = s33 ? s29 : s37;
  const SWord8 s39 = s30 ? s26 : s38;
  const SWord8 s40 = s27 ? s23 : s39;
  const SWord8 s41 = s24 ? s20 : s40;
  const SWord8 s42 = s21 ? s17 : s41;
  const SWord8 s43 = s18 ? s14 : s42;
  const SWord8 s44 = s15 ? s11 : s43;
  const SWord8 s45 = s12 ? s8 : s44;
  const SWord8 s46 = s9 ? s5 : s45;
  const SWord8 s47 = s6 ? s1 : s46;
  const SWord8 s48 = s3 ? s0 : s47;

  return s48;
}
== END: "sgcd.c" ==================