sbv-14.8: SBVTestSuite/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 foo.h
${CC} ${CCFLAGS} -c $< -o $@
foo_driver: foo.o foo_driver.o
${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}
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 SBV_GENERATED_foo_HEADER_INCLUDED
#define SBV_GENERATED_foo_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: */
SInt16 foo(const SInt16 x, const SInt64 *xArr, SWord16 *z,
SInt16 *zArr, SInt64 *yArr);
#endif /* SBV_GENERATED_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 <stdio.h>
#include "foo.h"
int main(void)
{
const SInt64 sbv_driver_input_1[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 sbv_driver_input_1_ctr;
for(sbv_driver_input_1_ctr = 0; sbv_driver_input_1_ctr < 45 ; ++sbv_driver_input_1_ctr)
{ printf(" xArr[%2d] = ", sbv_driver_input_1_ctr);
printf("%"PRId64"LL", sbv_driver_input_1[sbv_driver_input_1_ctr]);
printf("\n");
}
SWord16 sbv_driver_output_0;
SInt16 sbv_driver_output_1[7];
SInt64 sbv_driver_output_2[45];
const SInt16 sbv_result = foo(0x0000, sbv_driver_input_1,
&sbv_driver_output_0, sbv_driver_output_1, sbv_driver_output_2);
printf("foo(0x0000, xArr, &z, zArr, yArr) = %"PRId16"\n", sbv_result);
printf(" z = 0x%04"PRIx16"U\n", sbv_driver_output_0);
int sbv_driver_output_1_ctr;
for(sbv_driver_output_1_ctr = 0; sbv_driver_output_1_ctr < 7 ; ++sbv_driver_output_1_ctr)
{ printf(" zArr[%1d] = ", sbv_driver_output_1_ctr);
printf("%"PRId16"", sbv_driver_output_1[sbv_driver_output_1_ctr]);
printf("\n");
}
int sbv_driver_output_2_ctr;
for(sbv_driver_output_2_ctr = 0; sbv_driver_output_2_ctr < 45 ; ++sbv_driver_output_2_ctr)
{ printf(" yArr[%2d] = ", sbv_driver_output_2_ctr);
printf("%"PRId64"LL", sbv_driver_output_2[sbv_driver_output_2_ctr]);
printf("\n");
}
return 0;
}
== END: "foo_driver.c" ==================
== BEGIN: "foo.c" ================
/* File: "foo.c". Automatically generated by SBV. Do not edit! */
#include "foo.h"
/* Exact bit-vector runtime. All arithmetic is modulo the declared width. */
#ifndef SBV_CGEN_UNUSED
#if defined(__GNUC__) || defined(__clang__)
#define SBV_CGEN_UNUSED __attribute__((unused))
#else
#define SBV_CGEN_UNUSED
#endif
#endif
static inline SBV_CGEN_UNUSED SInt16 sbv_bv_s16_add(SInt16 a, SInt16 b)
{
const SWord16 bits = (SWord16) ((((uint64_t) (SWord16) a) + ((uint64_t) (SWord16) b)) & UINT64_C(0x000000000000ffff));
SInt16 result; memcpy(&result, &bits, sizeof result); return result;
}
static inline SBV_CGEN_UNUSED SInt16 sbv_bv_s16_mul(SInt16 a, SInt16 b)
{
const SWord16 bits = (SWord16) ((((uint64_t) (SWord16) a) * ((uint64_t) (SWord16) b)) & UINT64_C(0x000000000000ffff));
SInt16 result; memcpy(&result, &bits, sizeof result); return result;
}
SInt16 foo(const SInt16 sbv_input_0, const SInt64 *sbv_input_1,
SWord16 *sbv_output_0, SInt16 *sbv_output_1, SInt64 *sbv_output_2)
{
const SInt16 s0 = sbv_input_0;
const SInt64 s1 = sbv_input_1[0];
const SInt64 s2 = sbv_input_1[1];
const SInt64 s3 = sbv_input_1[2];
const SInt64 s4 = sbv_input_1[3];
const SInt64 s5 = sbv_input_1[4];
const SInt64 s6 = sbv_input_1[5];
const SInt64 s7 = sbv_input_1[6];
const SInt64 s8 = sbv_input_1[7];
const SInt64 s9 = sbv_input_1[8];
const SInt64 s10 = sbv_input_1[9];
const SInt64 s11 = sbv_input_1[10];
const SInt64 s12 = sbv_input_1[11];
const SInt64 s13 = sbv_input_1[12];
const SInt64 s14 = sbv_input_1[13];
const SInt64 s15 = sbv_input_1[14];
const SInt64 s16 = sbv_input_1[15];
const SInt64 s17 = sbv_input_1[16];
const SInt64 s18 = sbv_input_1[17];
const SInt64 s19 = sbv_input_1[18];
const SInt64 s20 = sbv_input_1[19];
const SInt64 s21 = sbv_input_1[20];
const SInt64 s22 = sbv_input_1[21];
const SInt64 s23 = sbv_input_1[22];
const SInt64 s24 = sbv_input_1[23];
const SInt64 s25 = sbv_input_1[24];
const SInt64 s26 = sbv_input_1[25];
const SInt64 s27 = sbv_input_1[26];
const SInt64 s28 = sbv_input_1[27];
const SInt64 s29 = sbv_input_1[28];
const SInt64 s30 = sbv_input_1[29];
const SInt64 s31 = sbv_input_1[30];
const SInt64 s32 = sbv_input_1[31];
const SInt64 s33 = sbv_input_1[32];
const SInt64 s34 = sbv_input_1[33];
const SInt64 s35 = sbv_input_1[34];
const SInt64 s36 = sbv_input_1[35];
const SInt64 s37 = sbv_input_1[36];
const SInt64 s38 = sbv_input_1[37];
const SInt64 s39 = sbv_input_1[38];
const SInt64 s40 = sbv_input_1[39];
const SInt64 s41 = sbv_input_1[40];
const SInt64 s42 = sbv_input_1[41];
const SInt64 s43 = sbv_input_1[42];
const SInt64 s44 = sbv_input_1[43];
const SInt64 s45 = sbv_input_1[44];
const SInt16 s48 = sbv_bv_s16_add(s0, 0x0001);
const SInt16 s50 = sbv_bv_s16_mul(s0, 0x0002);
*sbv_output_0 = 0x0005U;
sbv_output_1[0] = s48;
sbv_output_1[1] = s48;
sbv_output_1[2] = s48;
sbv_output_1[3] = s48;
sbv_output_1[4] = s48;
sbv_output_1[5] = s48;
sbv_output_1[6] = s48;
sbv_output_2[0] = s1;
sbv_output_2[1] = s2;
sbv_output_2[2] = s3;
sbv_output_2[3] = s4;
sbv_output_2[4] = s5;
sbv_output_2[5] = s6;
sbv_output_2[6] = s7;
sbv_output_2[7] = s8;
sbv_output_2[8] = s9;
sbv_output_2[9] = s10;
sbv_output_2[10] = s11;
sbv_output_2[11] = s12;
sbv_output_2[12] = s13;
sbv_output_2[13] = s14;
sbv_output_2[14] = s15;
sbv_output_2[15] = s16;
sbv_output_2[16] = s17;
sbv_output_2[17] = s18;
sbv_output_2[18] = s19;
sbv_output_2[19] = s20;
sbv_output_2[20] = s21;
sbv_output_2[21] = s22;
sbv_output_2[22] = s23;
sbv_output_2[23] = s24;
sbv_output_2[24] = s25;
sbv_output_2[25] = s26;
sbv_output_2[26] = s27;
sbv_output_2[27] = s28;
sbv_output_2[28] = s29;
sbv_output_2[29] = s30;
sbv_output_2[30] = s31;
sbv_output_2[31] = s32;
sbv_output_2[32] = s33;
sbv_output_2[33] = s34;
sbv_output_2[34] = s35;
sbv_output_2[35] = s36;
sbv_output_2[36] = s37;
sbv_output_2[37] = s38;
sbv_output_2[38] = s39;
sbv_output_2[39] = s40;
sbv_output_2[40] = s41;
sbv_output_2[41] = s42;
sbv_output_2[42] = s43;
sbv_output_2[43] = s44;
sbv_output_2[44] = s45;
return s50;
}
== END: "foo.c" ==================