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

Safe HaskellSafe-Infered



Simple code generation example.



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

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 $@

	rm -f *.o

veryclean: clean
	rm -f addSub_driver
== END: "Makefile" ==================
== BEGIN: "addSub.h" ================

BLANKLINE #ifndef __addSub__HEADER_INCLUDED__ #define __addSub__HEADER_INCLUDED__ BLANKLINE #include inttypes.h #include stdint.h #include stdbool.h BLANKLINE

typedef bool SBool; BLANKLINE

typedef uint8_t SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32; typedef uint64_t SWord64; BLANKLINE

typedef int8_t SInt8 ; typedef int16_t SInt16; typedef int32_t SInt32; typedef int64_t SInt64; BLANKLINE

void addSub(const SWord8 x, const SWord8 y, SWord8 *sum, SWord8 *dif); BLANKLINE #endif == END: addSub.h ================== == BEGIN: addSub_driver.c ================

BLANKLINE #include inttypes.h #include stdint.h #include stdbool.h #include stdio.h #include addSub.h BLANKLINE int main(void) { SWord8 sum; SWord8 dif; BLANKLINE addSub(132, 241, &sum, &dif); BLANKLINE printf(addSub(132, 241, &sum, &dif) ->n); printf( sum = %PRIu8n, sum); printf( dif = %PRIu8n, dif); BLANKLINE return 0; } == END: addSub_driver.c ================== == BEGIN: addSub.c ================

BLANKLINE #include inttypes.h #include stdint.h #include stdbool.h #include addSub.h BLANKLINE 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; BLANKLINE *sum = s2; *dif = s3; } == END: addSub.c ==================