== BEGIN: "Makefile" ================ # Makefile for fib1. 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: fib1_driver fib1.o: fib1.c fib1.h ${CC} ${CCFLAGS} -c $< -o $@ fib1_driver.o: fib1_driver.c ${CC} ${CCFLAGS} -c $< -o $@ fib1_driver: fib1.o fib1_driver.o ${CC} ${CCFLAGS} $^ -o $@ clean: rm -f *.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 #include /* 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: */ SWord64 fib1(const SWord64 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 #include #include #include "fib1.h" int main(void) { const SWord64 __result = fib1(0x000000000000000cULL); printf("fib1(0x000000000000000cULL) = 0x%016"PRIx64"ULL\n", __result); return 0; } == END: "fib1_driver.c" ================== == BEGIN: "fib1.c" ================ /* File: "fib1.c". Automatically generated by SBV. Do not edit! */ #include #include #include "fib1.h" SWord64 fib1(const SWord64 n) { const SWord64 s0 = n; const SBool s2 = s0 == 0x0000000000000000ULL; const SBool s4 = s0 == 0x0000000000000001ULL; const SBool s6 = s0 == 0x0000000000000002ULL; const SBool s8 = s0 == 0x0000000000000003ULL; const SBool s10 = s0 == 0x0000000000000004ULL; const SBool s12 = s0 == 0x0000000000000005ULL; const SBool s14 = s0 == 0x0000000000000006ULL; const SBool s17 = s0 == 0x0000000000000007ULL; const SBool s19 = s0 == 0x0000000000000008ULL; const SBool s22 = s0 == 0x0000000000000009ULL; const SBool s25 = s0 == 0x000000000000000aULL; const SBool s28 = s0 == 0x000000000000000bULL; const SBool s31 = s0 == 0x000000000000000cULL; const SBool s33 = s0 == 0x000000000000000dULL; const SBool s36 = s0 == 0x000000000000000eULL; const SBool s39 = s0 == 0x000000000000000fULL; const SBool s42 = s0 == 0x0000000000000010ULL; const SBool s45 = s0 == 0x0000000000000011ULL; const SBool s48 = s0 == 0x0000000000000012ULL; const SBool s51 = s0 == 0x0000000000000013ULL; const SBool s54 = s0 == 0x0000000000000014ULL; const SBool s56 = s0 == 0x0000000000000015ULL; const SBool s59 = s0 == 0x0000000000000016ULL; const SBool s62 = s0 == 0x0000000000000017ULL; const SBool s65 = s0 == 0x0000000000000018ULL; const SBool s68 = s0 == 0x0000000000000019ULL; const SBool s71 = s0 == 0x000000000000001aULL; const SBool s74 = s0 == 0x000000000000001bULL; const SBool s77 = s0 == 0x000000000000001cULL; const SBool s80 = s0 == 0x000000000000001dULL; const SBool s83 = s0 == 0x000000000000001eULL; const SBool s86 = s0 == 0x000000000000001fULL; const SBool s89 = s0 == 0x0000000000000020ULL; const SBool s92 = s0 == 0x0000000000000021ULL; const SBool s94 = s0 == 0x0000000000000022ULL; const SBool s97 = s0 == 0x0000000000000023ULL; const SBool s100 = s0 == 0x0000000000000024ULL; const SBool s103 = s0 == 0x0000000000000025ULL; const SBool s106 = s0 == 0x0000000000000026ULL; const SBool s109 = s0 == 0x0000000000000027ULL; const SBool s112 = s0 == 0x0000000000000028ULL; const SBool s115 = s0 == 0x0000000000000029ULL; const SBool s118 = s0 == 0x000000000000002aULL; const SBool s121 = s0 == 0x000000000000002bULL; const SBool s124 = s0 == 0x000000000000002cULL; const SBool s127 = s0 == 0x000000000000002dULL; const SBool s130 = s0 == 0x000000000000002eULL; const SBool s133 = s0 == 0x000000000000002fULL; const SBool s136 = s0 == 0x0000000000000030ULL; const SBool s139 = s0 == 0x0000000000000031ULL; const SBool s142 = s0 == 0x0000000000000032ULL; const SBool s145 = s0 == 0x0000000000000033ULL; const SBool s148 = s0 == 0x0000000000000034ULL; const SBool s151 = s0 == 0x0000000000000035ULL; const SBool s154 = s0 == 0x0000000000000036ULL; const SBool s156 = s0 == 0x0000000000000037ULL; const SBool s159 = s0 == 0x0000000000000038ULL; const SBool s162 = s0 == 0x0000000000000039ULL; const SBool s165 = s0 == 0x000000000000003aULL; const SBool s168 = s0 == 0x000000000000003bULL; const SBool s171 = s0 == 0x000000000000003cULL; const SBool s174 = s0 == 0x000000000000003dULL; const SBool s177 = s0 == 0x000000000000003eULL; const SBool s180 = s0 == 0x000000000000003fULL; const SWord64 s183 = s180 ? 0x000005f6c7b064e2ULL : 0x000009a661ca20bbULL; const SWord64 s184 = s177 ? 0x000003af9a19bbd9ULL : s183; const SWord64 s185 = s174 ? 0x000002472d96a909ULL : s184; const SWord64 s186 = s171 ? 0x000001686c8312d0ULL : s185; const SWord64 s187 = s168 ? 0x000000dec1139639ULL : s186; const SWord64 s188 = s165 ? 0x00000089ab6f7c97ULL : s187; const SWord64 s189 = s162 ? 0x0000005515a419a2ULL : s188; const SWord64 s190 = s159 ? 0x0000003495cb62f5ULL : s189; const SWord64 s191 = s156 ? 0x000000207fd8b6adULL : s190; const SWord64 s192 = s154 ? 0x0000001415f2ac48ULL : s191; const SWord64 s193 = s151 ? 0x0000000c69e60a65ULL : s192; const SWord64 s194 = s148 ? 0x00000007ac0ca1e3ULL : s193; const SWord64 s195 = s145 ? 0x00000004bdd96882ULL : s194; const SWord64 s196 = s142 ? 0x00000002ee333961ULL : s195; const SWord64 s197 = s139 ? 0x00000001cfa62f21ULL : s196; const SWord64 s198 = s136 ? 0x000000011e8d0a40ULL : s197; const SWord64 s199 = s133 ? 0x00000000b11924e1ULL : s198; const SWord64 s200 = s130 ? 0x000000006d73e55fULL : s199; const SWord64 s201 = s127 ? 0x0000000043a53f82ULL : s200; const SWord64 s202 = s124 ? 0x0000000029cea5ddULL : s201; const SWord64 s203 = s121 ? 0x0000000019d699a5ULL : s202; const SWord64 s204 = s118 ? 0x000000000ff80c38ULL : s203; const SWord64 s205 = s115 ? 0x0000000009de8d6dULL : s204; const SWord64 s206 = s112 ? 0x0000000006197ecbULL : s205; const SWord64 s207 = s109 ? 0x0000000003c50ea2ULL : s206; const SWord64 s208 = s106 ? 0x0000000002547029ULL : s207; const SWord64 s209 = s103 ? 0x0000000001709e79ULL : s208; const SWord64 s210 = s100 ? 0x0000000000e3d1b0ULL : s209; const SWord64 s211 = s97 ? 0x00000000008cccc9ULL : s210; const SWord64 s212 = s94 ? 0x00000000005704e7ULL : s211; const SWord64 s213 = s92 ? 0x000000000035c7e2ULL : s212; const SWord64 s214 = s89 ? 0x0000000000213d05ULL : s213; const SWord64 s215 = s86 ? 0x0000000000148addULL : s214; const SWord64 s216 = s83 ? 0x00000000000cb228ULL : s215; const SWord64 s217 = s80 ? 0x000000000007d8b5ULL : s216; const SWord64 s218 = s77 ? 0x000000000004d973ULL : s217; const SWord64 s219 = s74 ? 0x000000000002ff42ULL : s218; const SWord64 s220 = s71 ? 0x000000000001da31ULL : s219; const SWord64 s221 = s68 ? 0x0000000000012511ULL : s220; const SWord64 s222 = s65 ? 0x000000000000b520ULL : s221; const SWord64 s223 = s62 ? 0x0000000000006ff1ULL : s222; const SWord64 s224 = s59 ? 0x000000000000452fULL : s223; const SWord64 s225 = s56 ? 0x0000000000002ac2ULL : s224; const SWord64 s226 = s54 ? 0x0000000000001a6dULL : s225; const SWord64 s227 = s51 ? 0x0000000000001055ULL : s226; const SWord64 s228 = s48 ? 0x0000000000000a18ULL : s227; const SWord64 s229 = s45 ? 0x000000000000063dULL : s228; const SWord64 s230 = s42 ? 0x00000000000003dbULL : s229; const SWord64 s231 = s39 ? 0x0000000000000262ULL : s230; const SWord64 s232 = s36 ? 0x0000000000000179ULL : s231; const SWord64 s233 = s33 ? 0x00000000000000e9ULL : s232; const SWord64 s234 = s31 ? 0x0000000000000090ULL : s233; const SWord64 s235 = s28 ? 0x0000000000000059ULL : s234; const SWord64 s236 = s25 ? 0x0000000000000037ULL : s235; const SWord64 s237 = s22 ? 0x0000000000000022ULL : s236; const SWord64 s238 = s19 ? 0x0000000000000015ULL : s237; const SWord64 s239 = s17 ? 0x000000000000000dULL : s238; const SWord64 s240 = s14 ? 0x0000000000000008ULL : s239; const SWord64 s241 = s12 ? 0x0000000000000005ULL : s240; const SWord64 s242 = s10 ? 0x0000000000000003ULL : s241; const SWord64 s243 = s8 ? 0x0000000000000002ULL : s242; const SWord64 s244 = s6 ? 0x0000000000000001ULL : s243; const SWord64 s245 = s4 ? 0x0000000000000001ULL : s244; const SWord64 s246 = s2 ? 0x0000000000000000ULL : s245; return s246; } == END: "fib1.c" ==================