merge.gold

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

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

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

merge_driver: merge.o merge_driver.o
	${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}

clean:
	rm -f *.o

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

#ifndef SBV_GENERATED_merge_HEADER_INCLUDED
#define SBV_GENERATED_merge_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 merge(const SWord8 *xs, SWord8 *ys);

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

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

int main(void)
{
  const SWord8 sbv_driver_input_0[5] = {
      10,  6,  4, 82, 71
  };

  printf("Contents of input array xs:\n");
  int sbv_driver_input_0_ctr;
  for(sbv_driver_input_0_ctr = 0; sbv_driver_input_0_ctr < 5 ; ++sbv_driver_input_0_ctr)
  { printf("  xs[%1d] = ", sbv_driver_input_0_ctr);
    printf("%"PRIu8"", sbv_driver_input_0[sbv_driver_input_0_ctr]);
    printf("\n");
  }

  SWord8 sbv_driver_output_0[5];

  merge(sbv_driver_input_0, sbv_driver_output_0);

  printf("merge(xs, ys) ->\n");
  int sbv_driver_output_0_ctr;
  for(sbv_driver_output_0_ctr = 0; sbv_driver_output_0_ctr < 5 ; ++sbv_driver_output_0_ctr)
  { printf("  ys[%1d] = ", sbv_driver_output_0_ctr);
    printf("%"PRIu8"", sbv_driver_output_0[sbv_driver_output_0_ctr]);
    printf("\n");
  }

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

#include "merge.h"

void merge(const SWord8 *sbv_input_0, SWord8 *sbv_output_0)
{
  const SWord8 s0 = sbv_input_0[0];
  const SWord8 s1 = sbv_input_0[1];
  const SWord8 s2 = sbv_input_0[2];
  const SWord8 s3 = sbv_input_0[3];
  const SWord8 s4 = sbv_input_0[4];
  const SBool  s5 = s0 < s1;
  const SWord8 s6 = s5 ? s0 : s1;
  const SBool  s7 = s3 < s4;
  const SWord8 s8 = s7 ? s3 : s4;
  const SBool  s9 = s2 < s8;
  const SWord8 s10 = s9 ? s2 : s8;
  const SBool  s11 = s6 < s10;
  const SWord8 s12 = s11 ? s6 : s10;
  const SWord8 s13 = s5 ? s1 : s0;
  const SBool  s14 = s13 < s10;
  const SWord8 s15 = s14 ? s13 : s10;
  const SWord8 s16 = s7 ? s4 : s3;
  const SBool  s17 = s2 < s16;
  const SWord8 s18 = s17 ? s2 : s16;
  const SWord8 s19 = s9 ? s8 : s18;
  const SBool  s20 = s6 < s19;
  const SWord8 s21 = s20 ? s6 : s19;
  const SWord8 s22 = s11 ? s15 : s21;
  const SBool  s23 = s13 < s19;
  const SWord8 s24 = s23 ? s13 : s19;
  const SWord8 s25 = s14 ? s10 : s24;
  const SWord8 s26 = s17 ? s16 : s2;
  const SWord8 s27 = s9 ? s16 : s26;
  const SBool  s28 = s6 < s27;
  const SWord8 s29 = s28 ? s6 : s27;
  const SWord8 s30 = s20 ? s24 : s29;
  const SWord8 s31 = s11 ? s25 : s30;
  const SBool  s32 = s13 < s27;
  const SWord8 s33 = s32 ? s13 : s27;
  const SWord8 s34 = s23 ? s19 : s33;
  const SWord8 s35 = s14 ? s19 : s34;
  const SWord8 s36 = s28 ? s33 : s6;
  const SWord8 s37 = s20 ? s34 : s36;
  const SWord8 s38 = s11 ? s35 : s37;
  const SWord8 s39 = s32 ? s27 : s13;
  const SWord8 s40 = s23 ? s27 : s39;
  const SWord8 s41 = s14 ? s27 : s40;
  const SWord8 s42 = s28 ? s39 : s13;
  const SWord8 s43 = s20 ? s40 : s42;
  const SWord8 s44 = s11 ? s41 : s43;

  sbv_output_0[0] = s12;
  sbv_output_0[1] = s22;
  sbv_output_0[2] = s31;
  sbv_output_0[3] = s38;
  sbv_output_0[4] = s44;
}
== END: "merge.c" ==================