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

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

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

foo_driver: foo.o foo_driver.o
	${CC} ${CCFLAGS} $^ -o $@

clean:
	rm -f *.o

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

#ifndef __foo__HEADER_INCLUDED__
#define __foo__HEADER_INCLUDED__

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>

/* The boolean type */
typedef bool SBool;

/* 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: */
SInt16 foo(const SInt16 x, const SInt64 *xArr, SWord16 *z,
           SInt16 *zArr, SInt64 *yArr);

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

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <stdio.h>
#include "foo.h"

int main(void)
{
  const SInt64 xArr[45] = {
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
      0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL
  };

  printf("Contents of input array xArr:\n");
  int xArr_ctr;
  for(xArr_ctr = 0; xArr_ctr < 45 ; ++xArr_ctr)
    printf("  xArr[%d] = %"PRId64"LL\n", xArr_ctr ,xArr[xArr_ctr]);

  SWord16 z;
  SInt16 zArr[7];
  SInt64 yArr[45];

  const SInt16 __result = foo(0x0000, xArr, &z, zArr, yArr);

  printf("foo(0x0000, xArr, &z, zArr, yArr) = %"PRId16"\n", __result);
  printf("  z = 0x%04"PRIx16"U\n", z);
  int zArr_ctr;
  for(zArr_ctr = 0; zArr_ctr < 7 ; ++zArr_ctr)
    printf("  zArr[%d] = %"PRId16"\n", zArr_ctr ,zArr[zArr_ctr]);
  int yArr_ctr;
  for(yArr_ctr = 0; yArr_ctr < 45 ; ++yArr_ctr)
    printf("  yArr[%d] = %"PRId64"LL\n", yArr_ctr ,yArr[yArr_ctr]);

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

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include "foo.h"

SInt16 foo(const SInt16 x, const SInt64 *xArr, SWord16 *z,
           SInt16 *zArr, SInt64 *yArr)
{
  const SInt16 s0 = x;
  const SInt64 s1 = xArr[0];
  const SInt64 s2 = xArr[1];
  const SInt64 s3 = xArr[2];
  const SInt64 s4 = xArr[3];
  const SInt64 s5 = xArr[4];
  const SInt64 s6 = xArr[5];
  const SInt64 s7 = xArr[6];
  const SInt64 s8 = xArr[7];
  const SInt64 s9 = xArr[8];
  const SInt64 s10 = xArr[9];
  const SInt64 s11 = xArr[10];
  const SInt64 s12 = xArr[11];
  const SInt64 s13 = xArr[12];
  const SInt64 s14 = xArr[13];
  const SInt64 s15 = xArr[14];
  const SInt64 s16 = xArr[15];
  const SInt64 s17 = xArr[16];
  const SInt64 s18 = xArr[17];
  const SInt64 s19 = xArr[18];
  const SInt64 s20 = xArr[19];
  const SInt64 s21 = xArr[20];
  const SInt64 s22 = xArr[21];
  const SInt64 s23 = xArr[22];
  const SInt64 s24 = xArr[23];
  const SInt64 s25 = xArr[24];
  const SInt64 s26 = xArr[25];
  const SInt64 s27 = xArr[26];
  const SInt64 s28 = xArr[27];
  const SInt64 s29 = xArr[28];
  const SInt64 s30 = xArr[29];
  const SInt64 s31 = xArr[30];
  const SInt64 s32 = xArr[31];
  const SInt64 s33 = xArr[32];
  const SInt64 s34 = xArr[33];
  const SInt64 s35 = xArr[34];
  const SInt64 s36 = xArr[35];
  const SInt64 s37 = xArr[36];
  const SInt64 s38 = xArr[37];
  const SInt64 s39 = xArr[38];
  const SInt64 s40 = xArr[39];
  const SInt64 s41 = xArr[40];
  const SInt64 s42 = xArr[41];
  const SInt64 s43 = xArr[42];
  const SInt64 s44 = xArr[43];
  const SInt64 s45 = xArr[44];
  const SInt16 s48 = s0 + 0x0001;
  const SInt16 s50 = s0 * 0x0002;

  *z = 0x0005U;
  zArr[0] = s48;
  zArr[1] = s48;
  zArr[2] = s48;
  zArr[3] = s48;
  zArr[4] = s48;
  zArr[5] = s48;
  zArr[6] = s48;
  yArr[0] = s1;
  yArr[1] = s2;
  yArr[2] = s3;
  yArr[3] = s4;
  yArr[4] = s5;
  yArr[5] = s6;
  yArr[6] = s7;
  yArr[7] = s8;
  yArr[8] = s9;
  yArr[9] = s10;
  yArr[10] = s11;
  yArr[11] = s12;
  yArr[12] = s13;
  yArr[13] = s14;
  yArr[14] = s15;
  yArr[15] = s16;
  yArr[16] = s17;
  yArr[17] = s18;
  yArr[18] = s19;
  yArr[19] = s20;
  yArr[20] = s21;
  yArr[21] = s22;
  yArr[22] = s23;
  yArr[23] = s24;
  yArr[24] = s25;
  yArr[25] = s26;
  yArr[26] = s27;
  yArr[27] = s28;
  yArr[28] = s29;
  yArr[29] = s30;
  yArr[30] = s31;
  yArr[31] = s32;
  yArr[32] = s33;
  yArr[33] = s34;
  yArr[34] = s35;
  yArr[35] = s36;
  yArr[36] = s37;
  yArr[37] = s38;
  yArr[38] = s39;
  yArr[39] = s40;
  yArr[40] = s41;
  yArr[41] = s42;
  yArr[42] = s43;
  yArr[43] = s44;
  yArr[44] = s45;
  return s50;
}
== END: "foo.c" ==================