selUnchecked.gold

== BEGIN: "Makefile" ================
# Makefile for selUnChecked. Automatically generated by SBV. Do not edit!

CC=gcc
CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer

all: selUnChecked_driver

selUnChecked.o: selUnChecked.c selUnChecked.h
	${CC} ${CCFLAGS} -c selUnChecked.c -o selUnChecked.o

selUnChecked_driver.o: selUnChecked_driver.c
	${CC} ${CCFLAGS} -c selUnChecked_driver.c -o selUnChecked_driver.o

selUnChecked_driver: selUnChecked.o selUnChecked_driver.o
	${CC} ${CCFLAGS} selUnChecked.o selUnChecked_driver.o -o selUnChecked_driver

clean:
	rm -f selUnChecked_driver.o selUnChecked.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 <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: */
SWord8 selUnChecked(const SWord8 s0);

#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 <inttypes.h>
#include <stdint.h>
#include <stdio.h>
#include "selUnChecked.h"

int main(void)
{
  const SWord8 out0 = selUnChecked(65);
  
  printf("selUnChecked(65) = %"PRIu8"\n", out0);
  
  return 0;
}
== END: "selUnChecked_driver.c" ==================
== BEGIN: "selUnChecked.c" ================
/* File: "selUnChecked.c". Automatically generated by SBV. Do not edit! */

#include <inttypes.h>
#include <stdint.h>
#include "selUnChecked.h"

SWord8 selUnChecked(const SWord8 s0)
{
  const SWord8 s3 = s0 + 2;
  const SWord8 table0[] = {
      1, s3
  };
  const SWord8 s5 = table0[s0];
  
  return s5;
}
== END: "selUnChecked.c" ==================