sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.CodeGeneration.AddSub

Description

Simple code generation example.

Synopsis

- addSub :: SWord8 -> SWord8 -> (SWord8, SWord8)
- genAddSub :: IO ()

# Documentation

addSub :: SWord8 -> SWord8 -> (SWord8, SWord8) Source #

Simple function that returns add/sum of args

genAddSub :: IO () Source #

Generate C code for addSub. Here's the output showing the generated C code:

    >>> genAddSub
    == BEGIN: "Makefile" ================
    # Makefile for addSub. 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: addSub_driver

    addSub.o: addSub.c addSub.h
    	${CC} ${CCFLAGS} -c $< -o $@

    addSub_driver.o: addSub_driver.c
    	${CC} ${CCFLAGS} -c $< -o $@

    addSub_driver: addSub.o addSub_driver.o
    	${CC} ${CCFLAGS} $^ -o $@

    clean:
    	rm -f *.o

    veryclean: clean
    	rm -f addSub_driver
    == END: "Makefile" ==================
    == BEGIN: "addSub.h" ================
    /* Header file for addSub. Automatically generated by SBV. Do not edit! */

    #ifndef __addSub__HEADER_INCLUDED__
    #define __addSub__HEADER_INCLUDED__

    #include <stdio.h>
    #include <stdlib.h>
    #include <inttypes.h>
    #include <stdint.h>
    #include <stdbool.h>
    #include <string.h>
    #include <math.h>

    /* 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: */
    void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
                SWord8 *dif);

    #endif /* __addSub__HEADER_INCLUDED__ */
    == END: "addSub.h" ==================
    == BEGIN: "addSub_driver.c" ================
    /* Example driver program for addSub. */
    /* Automatically generated by SBV. Edit as you see fit! */

    #include <stdio.h>
    #include "addSub.h"

    int main(void)
    {
      SWord8 sum;
      SWord8 dif;

      addSub(132, 241, &sum, &dif);

      printf("addSub(132, 241, &sum, &dif) ->\n");
      printf("  sum = %"PRIu8"\n", sum);
      printf("  dif = %"PRIu8"\n", dif);

      return 0;
    }
    == END: "addSub_driver.c" ==================
    == BEGIN: "addSub.c" ================
    /* File: "addSub.c". Automatically generated by SBV. Do not edit! */

    #include "addSub.h"

    void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
                SWord8 *dif)
    {
      const SWord8 s0 = x;
      const SWord8 s1 = y;
      const SWord8 s2 = s0 + s1;
      const SWord8 s3 = s0 - s1;

      *sum = s2;
      *dif = s3;
    }
    == END: "addSub.c" ==================