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

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

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

tstShiftLeft_driver: tstShiftLeft.o tstShiftLeft_driver.o
	${CC} ${CCFLAGS} $^ -o $@

clean:
	rm -f *.o

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

#ifndef __tstShiftLeft__HEADER_INCLUDED__
#define __tstShiftLeft__HEADER_INCLUDED__

#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.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: */
SWord32 tstShiftLeft(const SWord32 *vs);

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

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

int main(void)
{
  const SWord32 vs[3] = {
      0x00000001UL, 0x00000002UL, 0x00000003UL
  };

  printf("Contents of input array vs:\n");
  int vs_ctr;
  for(vs_ctr = 0; vs_ctr < 3 ; ++vs_ctr)
    printf("  vs[%d] = 0x%08"PRIx32"UL\n", vs_ctr ,vs[vs_ctr]);


  const SWord32 __result = tstShiftLeft(vs);

  printf("tstShiftLeft(vs) = 0x%08"PRIx32"UL\n", __result);

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

#include "tstShiftLeft.h"

/* User specified custom code for "SBV_SHIFTLEFT" */
#define SBV_SHIFTLEFT(x, y) ((x) << (y))

SWord32 tstShiftLeft(const SWord32 *vs)
{
  const SWord32 s0 = vs[0];
  const SWord32 s1 = vs[1];
  const SWord32 s2 = vs[2];
  const SWord32 s3 = /* Uninterpreted function */ SBV_SHIFTLEFT(s0,
                                                                s2);
  const SWord32 s4 = /* Uninterpreted function */ SBV_SHIFTLEFT(s1,
                                                                s2);
  const SWord32 s5 = s3 + s4;

  return s5;
}
== END: "tstShiftLeft.c" ==================