1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
== BEGIN: "Makefile" ================
# Makefile for merge. 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: merge_driver
merge.o: merge.c merge.h
${CC} ${CCFLAGS} -c $< -o $@
merge_driver.o: merge_driver.c
${CC} ${CCFLAGS} -c $< -o $@
merge_driver: merge.o merge_driver.o
${CC} ${CCFLAGS} $^ -o $@
clean:
rm -f *.o
veryclean: clean
rm -f merge_driver
== END: "Makefile" ==================
== BEGIN: "merge.h" ================
/* Header file for merge. Automatically generated by SBV. Do not edit! */
#ifndef __merge__HEADER_INCLUDED__
#define __merge__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 merge(const SWord8 *xs, SWord8 *ys);
#endif /* __merge__HEADER_INCLUDED__ */
== END: "merge.h" ==================
== BEGIN: "merge_driver.c" ================
/* Example driver program for merge. */
/* Automatically generated by SBV. Edit as you see fit! */
#include <stdio.h>
#include "merge.h"
int main(void)
{
const SWord8 xs[5] = {
10, 6, 4, 82, 71
};
printf("Contents of input array xs:\n");
int xs_ctr;
for(xs_ctr = 0; xs_ctr < 5 ; ++xs_ctr)
printf(" xs[%d] = %"PRIu8"\n", xs_ctr ,xs[xs_ctr]);
SWord8 ys[5];
merge(xs, ys);
printf("merge(xs, ys) ->\n");
int ys_ctr;
for(ys_ctr = 0; ys_ctr < 5 ; ++ys_ctr)
printf(" ys[%d] = %"PRIu8"\n", ys_ctr ,ys[ys_ctr]);
return 0;
}
== END: "merge_driver.c" ==================
== BEGIN: "merge.c" ================
/* File: "merge.c". Automatically generated by SBV. Do not edit! */
#include "merge.h"
void merge(const SWord8 *xs, SWord8 *ys)
{
const SWord8 s0 = xs[0];
const SWord8 s1 = xs[1];
const SWord8 s2 = xs[2];
const SWord8 s3 = xs[3];
const SWord8 s4 = xs[4];
const SBool s5 = s0 < s1;
const SWord8 s6 = s5 ? s0 : s1;
const SBool s7 = s3 < s4;
const SWord8 s8 = s7 ? s3 : s4;
const SBool s9 = s2 < s8;
const SWord8 s10 = s9 ? s2 : s8;
const SBool s11 = s6 < s10;
const SWord8 s12 = s11 ? s6 : s10;
const SWord8 s13 = s5 ? s1 : s0;
const SBool s14 = s13 < s10;
const SWord8 s15 = s14 ? s13 : s10;
const SWord8 s16 = s7 ? s4 : s3;
const SBool s17 = s2 < s16;
const SWord8 s18 = s17 ? s2 : s16;
const SWord8 s19 = s9 ? s8 : s18;
const SBool s20 = s6 < s19;
const SWord8 s21 = s20 ? s6 : s19;
const SWord8 s22 = s11 ? s15 : s21;
const SBool s23 = s13 < s19;
const SWord8 s24 = s23 ? s13 : s19;
const SWord8 s25 = s14 ? s10 : s24;
const SWord8 s26 = s17 ? s16 : s2;
const SWord8 s27 = s9 ? s16 : s26;
const SBool s28 = s6 < s27;
const SWord8 s29 = s28 ? s6 : s27;
const SWord8 s30 = s20 ? s24 : s29;
const SWord8 s31 = s11 ? s25 : s30;
const SBool s32 = s13 < s27;
const SWord8 s33 = s32 ? s13 : s27;
const SWord8 s34 = s23 ? s19 : s33;
const SWord8 s35 = s14 ? s19 : s34;
const SWord8 s36 = s28 ? s33 : s6;
const SWord8 s37 = s20 ? s34 : s36;
const SWord8 s38 = s11 ? s35 : s37;
const SWord8 s39 = s32 ? s27 : s13;
const SWord8 s40 = s23 ? s27 : s39;
const SWord8 s41 = s14 ? s27 : s40;
const SWord8 s42 = s28 ? s39 : s13;
const SWord8 s43 = s20 ? s40 : s42;
const SWord8 s44 = s11 ? s41 : s43;
ys[0] = s12;
ys[1] = s22;
ys[2] = s31;
ys[3] = s38;
ys[4] = s44;
}
== END: "merge.c" ==================
|
