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
	${CC} ${CCFLAGS} -c $< -o $@

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

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 __merge__HEADER_INCLUDED__
#define __merge__HEADER_INCLUDED__

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.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: */
void merge(const SWord8 *xs, SWord8 *ys);

#endif /* __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 <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <math.h>
#include <stdio.h>
#include "merge.h"

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

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

  SWord8 ys[5];

  merge(xs, ys);

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

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

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <math.h>
#include "merge.h"

void merge(const SWord8 *xs, SWord8 *ys)
{
  const SWord8 s0 = xs[0];
  const SWord8 s1 = xs[1];
  const SWord8 s2 = xs[2];
  const SWord8 s3 = xs[3];
  const SWord8 s4 = xs[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;

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