sbv-3.0: SBVUnitTest/GoldFiles/codeGen1.gold
== 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>
#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: */
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 <math.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 <math.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" ==================