sbv-0.9.13: SBVUnitTest/GoldFiles/fib1.gold
== BEGIN: "Makefile" ================
# Makefile for fib1. Automatically generated by SBV. Do not edit!
CC=gcc
CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
all: fib1_driver
fib1.o: fib1.c fib1.h
${CC} ${CCFLAGS} -c fib1.c -o fib1.o
fib1_driver.o: fib1_driver.c
${CC} ${CCFLAGS} -c fib1_driver.c -o fib1_driver.o
fib1_driver: fib1.o fib1_driver.o
${CC} ${CCFLAGS} fib1.o fib1_driver.o -o fib1_driver
clean:
rm -f fib1_driver.o fib1.o
veryclean: clean
rm -f fib1_driver
== END: "Makefile" ==================
== BEGIN: "fib1.h" ================
/* Header file for fib1. Automatically generated by SBV. Do not edit! */
#ifndef __fib1__HEADER_INCLUDED__
#define __fib1__HEADER_INCLUDED__
#include <inttypes.h>
#include <stdint.h>
/* Unsigned bit-vectors */
typedef uint8_t SBool ;
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 fib1(const SWord32 n);
#endif /* __fib1__HEADER_INCLUDED__ */
== END: "fib1.h" ==================
== BEGIN: "fib1_driver.c" ================
/* Example driver program for fib1. */
/* Automatically generated by SBV. Edit as you see fit! */
#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>
#include "fib1.h"
int main(void)
{
const SWord32 out0 = fib1(0x0000000cUL);
printf("fib1(0x0000000cUL) = 0x%08"PRIx32"UL\n", out0);
return 0;
}
== END: "fib1_driver.c" ==================
== BEGIN: "fib1.c" ================
/* File: "fib1.c". Automatically generated by SBV. Do not edit! */
#include <inttypes.h>
#include <stdint.h>
#include "fib1.h"
SWord32 fib1(const SWord32 n)
{
const SWord32 s0 = n;
const SBool s2 = s0 == 0x00000000UL;
const SBool s4 = s0 == 0x00000001UL;
const SBool s6 = s0 == 0x00000002UL;
const SBool s8 = s0 == 0x00000003UL;
const SBool s10 = s0 == 0x00000004UL;
const SBool s12 = s0 == 0x00000005UL;
const SBool s14 = s0 == 0x00000006UL;
const SBool s17 = s0 == 0x00000007UL;
const SBool s19 = s0 == 0x00000008UL;
const SBool s22 = s0 == 0x00000009UL;
const SBool s25 = s0 == 0x0000000aUL;
const SBool s28 = s0 == 0x0000000bUL;
const SBool s31 = s0 == 0x0000000cUL;
const SBool s33 = s0 == 0x0000000dUL;
const SBool s36 = s0 == 0x0000000eUL;
const SBool s39 = s0 == 0x0000000fUL;
const SBool s42 = s0 == 0x00000010UL;
const SBool s45 = s0 == 0x00000011UL;
const SBool s48 = s0 == 0x00000012UL;
const SBool s51 = s0 == 0x00000013UL;
const SBool s54 = s0 == 0x00000014UL;
const SBool s56 = s0 == 0x00000015UL;
const SBool s59 = s0 == 0x00000016UL;
const SBool s62 = s0 == 0x00000017UL;
const SBool s65 = s0 == 0x00000018UL;
const SBool s68 = s0 == 0x00000019UL;
const SBool s71 = s0 == 0x0000001aUL;
const SBool s74 = s0 == 0x0000001bUL;
const SBool s77 = s0 == 0x0000001cUL;
const SBool s80 = s0 == 0x0000001dUL;
const SBool s83 = s0 == 0x0000001eUL;
const SBool s86 = s0 == 0x0000001fUL;
const SBool s89 = s0 == 0x00000020UL;
const SBool s92 = s0 == 0x00000021UL;
const SBool s94 = s0 == 0x00000022UL;
const SBool s97 = s0 == 0x00000023UL;
const SBool s100 = s0 == 0x00000024UL;
const SBool s103 = s0 == 0x00000025UL;
const SBool s106 = s0 == 0x00000026UL;
const SBool s109 = s0 == 0x00000027UL;
const SBool s112 = s0 == 0x00000028UL;
const SBool s115 = s0 == 0x00000029UL;
const SBool s118 = s0 == 0x0000002aUL;
const SBool s121 = s0 == 0x0000002bUL;
const SBool s124 = s0 == 0x0000002cUL;
const SBool s127 = s0 == 0x0000002dUL;
const SBool s130 = s0 == 0x0000002eUL;
const SBool s133 = s0 == 0x0000002fUL;
const SBool s136 = s0 == 0x00000030UL;
const SBool s139 = s0 == 0x00000031UL;
const SBool s142 = s0 == 0x00000032UL;
const SBool s145 = s0 == 0x00000033UL;
const SBool s148 = s0 == 0x00000034UL;
const SBool s151 = s0 == 0x00000035UL;
const SBool s154 = s0 == 0x00000036UL;
const SBool s156 = s0 == 0x00000037UL;
const SBool s159 = s0 == 0x00000038UL;
const SBool s162 = s0 == 0x00000039UL;
const SBool s165 = s0 == 0x0000003aUL;
const SBool s168 = s0 == 0x0000003bUL;
const SBool s171 = s0 == 0x0000003cUL;
const SBool s174 = s0 == 0x0000003dUL;
const SBool s177 = s0 == 0x0000003eUL;
const SBool s180 = s0 == 0x0000003fUL;
const SWord32 s183 = s180 ? 0xc7b064e2UL : 0x61ca20bbUL;
const SWord32 s184 = s177 ? 0x9a19bbd9UL : s183;
const SWord32 s185 = s174 ? 0x2d96a909UL : s184;
const SWord32 s186 = s171 ? 0x6c8312d0UL : s185;
const SWord32 s187 = s168 ? 0xc1139639UL : s186;
const SWord32 s188 = s165 ? 0xab6f7c97UL : s187;
const SWord32 s189 = s162 ? 0x15a419a2UL : s188;
const SWord32 s190 = s159 ? 0x95cb62f5UL : s189;
const SWord32 s191 = s156 ? 0x7fd8b6adUL : s190;
const SWord32 s192 = s154 ? 0x15f2ac48UL : s191;
const SWord32 s193 = s151 ? 0x69e60a65UL : s192;
const SWord32 s194 = s148 ? 0xac0ca1e3UL : s193;
const SWord32 s195 = s145 ? 0xbdd96882UL : s194;
const SWord32 s196 = s142 ? 0xee333961UL : s195;
const SWord32 s197 = s139 ? 0xcfa62f21UL : s196;
const SWord32 s198 = s136 ? 0x1e8d0a40UL : s197;
const SWord32 s199 = s133 ? 0xb11924e1UL : s198;
const SWord32 s200 = s130 ? 0x6d73e55fUL : s199;
const SWord32 s201 = s127 ? 0x43a53f82UL : s200;
const SWord32 s202 = s124 ? 0x29cea5ddUL : s201;
const SWord32 s203 = s121 ? 0x19d699a5UL : s202;
const SWord32 s204 = s118 ? 0x0ff80c38UL : s203;
const SWord32 s205 = s115 ? 0x09de8d6dUL : s204;
const SWord32 s206 = s112 ? 0x06197ecbUL : s205;
const SWord32 s207 = s109 ? 0x03c50ea2UL : s206;
const SWord32 s208 = s106 ? 0x02547029UL : s207;
const SWord32 s209 = s103 ? 0x01709e79UL : s208;
const SWord32 s210 = s100 ? 0x00e3d1b0UL : s209;
const SWord32 s211 = s97 ? 0x008cccc9UL : s210;
const SWord32 s212 = s94 ? 0x005704e7UL : s211;
const SWord32 s213 = s92 ? 0x0035c7e2UL : s212;
const SWord32 s214 = s89 ? 0x00213d05UL : s213;
const SWord32 s215 = s86 ? 0x00148addUL : s214;
const SWord32 s216 = s83 ? 0x000cb228UL : s215;
const SWord32 s217 = s80 ? 0x0007d8b5UL : s216;
const SWord32 s218 = s77 ? 0x0004d973UL : s217;
const SWord32 s219 = s74 ? 0x0002ff42UL : s218;
const SWord32 s220 = s71 ? 0x0001da31UL : s219;
const SWord32 s221 = s68 ? 0x00012511UL : s220;
const SWord32 s222 = s65 ? 0x0000b520UL : s221;
const SWord32 s223 = s62 ? 0x00006ff1UL : s222;
const SWord32 s224 = s59 ? 0x0000452fUL : s223;
const SWord32 s225 = s56 ? 0x00002ac2UL : s224;
const SWord32 s226 = s54 ? 0x00001a6dUL : s225;
const SWord32 s227 = s51 ? 0x00001055UL : s226;
const SWord32 s228 = s48 ? 0x00000a18UL : s227;
const SWord32 s229 = s45 ? 0x0000063dUL : s228;
const SWord32 s230 = s42 ? 0x000003dbUL : s229;
const SWord32 s231 = s39 ? 0x00000262UL : s230;
const SWord32 s232 = s36 ? 0x00000179UL : s231;
const SWord32 s233 = s33 ? 0x000000e9UL : s232;
const SWord32 s234 = s31 ? 0x00000090UL : s233;
const SWord32 s235 = s28 ? 0x00000059UL : s234;
const SWord32 s236 = s25 ? 0x00000037UL : s235;
const SWord32 s237 = s22 ? 0x00000022UL : s236;
const SWord32 s238 = s19 ? 0x00000015UL : s237;
const SWord32 s239 = s17 ? 0x0000000dUL : s238;
const SWord32 s240 = s14 ? 0x00000008UL : s239;
const SWord32 s241 = s12 ? 0x00000005UL : s240;
const SWord32 s242 = s10 ? 0x00000003UL : s241;
const SWord32 s243 = s8 ? 0x00000002UL : s242;
const SWord32 s244 = s6 ? 0x00000001UL : s243;
const SWord32 s245 = s4 ? 0x00000001UL : s244;
const SWord32 s246 = s2 ? 0x00000000UL : s245;
return s246;
}
== END: "fib1.c" ==================