aboutsummaryrefslogtreecommitdiffstats
path: root/test
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-04-02 14:53:39 +0100
committerYann Herklotz <git@yannherklotz.com>2020-04-02 14:53:39 +0100
commit7a76e9d632756a4d3f044d6742a5defb83ce6ae7 (patch)
tree2cb909cfe974953c019f120e06101e686402ba07 /test
parentb22dfebd3a1638c431e9ab32fac391aa95f846eb (diff)
downloadvericert-7a76e9d632756a4d3f044d6742a5defb83ce6ae7.tar.gz
vericert-7a76e9d632756a4d3f044d6742a5defb83ce6ae7.zip
Add tests
Diffstat (limited to 'test')
-rw-r--r--test/add.c6
-rw-r--r--test/conditional.c7
-rw-r--r--test/loop.c10
-rwxr-xr-xtest/test_all.sh45
4 files changed, 68 insertions, 0 deletions
diff --git a/test/add.c b/test/add.c
new file mode 100644
index 0000000..ab03976
--- /dev/null
+++ b/test/add.c
@@ -0,0 +1,6 @@
+int main () {
+ int x = 1;
+ int y = 2;
+ int z = x + y;
+ return z;
+}
diff --git a/test/conditional.c b/test/conditional.c
new file mode 100644
index 0000000..041e55b
--- /dev/null
+++ b/test/conditional.c
@@ -0,0 +1,7 @@
+int main() {
+ int x = 2;
+ if (x > 1)
+ return 5;
+ else
+ return 2;
+}
diff --git a/test/loop.c b/test/loop.c
new file mode 100644
index 0000000..b459e3a
--- /dev/null
+++ b/test/loop.c
@@ -0,0 +1,10 @@
+int main() {
+ int max = 5;
+ int acc = 0;
+
+ for (int i = 0; i < max; i++) {
+ acc += i;
+ }
+
+ return acc + 2;
+}
diff --git a/test/test_all.sh b/test/test_all.sh
new file mode 100755
index 0000000..67b5c8f
--- /dev/null
+++ b/test/test_all.sh
@@ -0,0 +1,45 @@
+mytmpdir=$(mktemp -d 2>/dev/null || mktemp -d -t 'mytmpdir')
+echo "--------------------------------------------------"
+echo "Created working directory: $mytmpdir"
+echo "--------------------------------------------------"
+
+if [[ -z $1 ]]; then
+ test_dir=.
+else
+ test_dir=$1
+fi
+
+test_command() {
+ local loc=$(command -v $1)
+ if [[ $? -eq 0 ]]; then
+ echo "Found $1: $loc"
+ else
+ echo "Could not find $1"
+ exit 1
+ fi
+}
+
+test_command iverilog
+test_command gcc
+
+echo "--------------------------------------------------"
+
+for cfile in $test_dir/*.c; do
+ echo "Testing $cfile"
+ outbase=$mytmpdir/$(basename $cfile)
+ gcc -o $outbase.gcc $cfile
+ $outbase.gcc
+ expected=$?
+ ./bin/coqup --hls -drtl -o $outbase.v $cfile
+ iverilog -o $outbase.iverilog $outbase.v
+ actual=$($outbase.iverilog | sed -E -e 's/[^0-9]+([0-9]+)/\1/')
+ if [[ $expected = $actual ]]; then
+ echo "OK"
+ else
+ echo "FAILED: $expected != $actual"
+ fi
+done
+
+echo "--------------------------------------------------"
+
+rm -rf $mytmpdir