== BEGIN: "Makefile" ================ # Makefile for selUnChecked. 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: selUnChecked_driver selUnChecked.o: selUnChecked.c selUnChecked.h ${CC} ${CCFLAGS} -c $< -o $@ selUnChecked_driver.o: selUnChecked_driver.c ${CC} ${CCFLAGS} -c $< -o $@ selUnChecked_driver: selUnChecked.o selUnChecked_driver.o ${CC} ${CCFLAGS} $^ -o $@ clean: rm -f *.o veryclean: clean rm -f selUnChecked_driver == END: "Makefile" ================== == BEGIN: "selUnChecked.h" ================ /* Header file for selUnChecked. Automatically generated by SBV. Do not edit! */ #ifndef __selUnChecked__HEADER_INCLUDED__ #define __selUnChecked__HEADER_INCLUDED__ #include #include #include #include #include #include #include /* 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: */ SWord8 selUnChecked(const SWord8 x); #endif /* __selUnChecked__HEADER_INCLUDED__ */ == END: "selUnChecked.h" ================== == BEGIN: "selUnChecked_driver.c" ================ /* Example driver program for selUnChecked. */ /* Automatically generated by SBV. Edit as you see fit! */ #include #include "selUnChecked.h" int main(void) { const SWord8 __result = selUnChecked(65); printf("selUnChecked(65) = %"PRIu8"\n", __result); return 0; } == END: "selUnChecked_driver.c" ================== == BEGIN: "selUnChecked.c" ================ /* File: "selUnChecked.c". Automatically generated by SBV. Do not edit! */ #include "selUnChecked.h" SWord8 selUnChecked(const SWord8 x) { const SWord8 s0 = x; const SWord8 s3 = s0 + 2; const SWord8 table0[] = { 1, s3 }; const SWord8 s5 = table0[s0]; return s5; } == END: "selUnChecked.c" ==================