Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
dff562c4
Commit
dff562c4
authored
Apr 22, 2021
by
Léo Gourdin
Browse files
moving my tests
parent
e37d655d
Changes
26
Hide whitespace changes
Inline
Side-by-side
test/aarch64/README.md
deleted
100644 → 0
View file @
e37d655d
# Testing the Machblock --> Asmblock translation
1.
Get the reference version of compcert-aarch in the father's directory if this repo (checkout
`aarch64-ref`
)
2.
Compile both repo for aarch64
3.
CD in this folder (
`test/aarch64`
)
4.
Launch
`./asmb_aarch64_gen_test.sh`
## Options
The script takes following options :
-
`-c`
to clear generated files at the end
-
`-w`
to suppress warnings from Compcert
## Tests files
The variable
`DIRS`
in the script takes the list of directories containing c files.
The tests under
`test/aarch64/c`
are simpler and useful to debug only one feature at a time.
Most of them comes from
[
here
](
https://cis.temple.edu/~ingargio/cis71/code/
)
.
test/aarch64/gen_tests/asmb_aarch64_gen_test.sh
deleted
100755 → 0
View file @
e37d655d
#!/bin/bash
CLEAN
=
0
WOFF
=
0
while
getopts
':cw'
'OPTKEY'
;
do
case
${
OPTKEY
}
in
c
)
CLEAN
=
1
;;
w
)
WOFF
=
1
;;
esac
done
DIRS
=(
../c/
*
.c
# Special simple tests
#../../c/*.c
../../clightgen/
*
.c
#../../compression/*.c
../../cse2/
*
.c
# Monniaux test directory
../../monniaux/binary_search/
*
.c
../../monniaux/complex/
*
.c
#../../monniaux/crypto-algorithms/*.c # Warnings
../../monniaux/cse2/
*
.c
#../../monniaux/des/*.c # Unsupported feature?
../../monniaux/expect/
*
.c
../../monniaux/fill_buffer/
*
.c
../../monniaux/genann/
*
.c
#../../monniaux/heptagon_radio_transmitter/*.c # Warnings
../../monniaux/idea/
*
.c
../../monniaux/jumptable/
*
.c
../../monniaux/licm/
*
.c
../../monniaux/longjmp/
*
.c
../../monniaux/loop/
*
.c
../../monniaux/lustrev4_lustrec_heater_control/
*
.c
../../monniaux/lustrev4_lv4_heater_control/
*
.c
../../monniaux/lustrev4_lv6-en-2cgc_heater_control/
*
.c
#../../monniaux/lustrev6-carlightV2/*.c # Warnings
#../../monniaux/lustrev6-convertible-2cgc/*.c # Unsupported feature?
#../../monniaux/lustrev6-convertible-en-2cgc/*.c
#../../monniaux/lustrev6-convertible/*.c # Warnings
../../monniaux/madd/
*
.c
#../../monniaux/math/*.c # Unsupported feature?
../../monniaux/memcpy/
*
.c
#../../monniaux/micro-bunzip/*.c # Warnings
../../monniaux/moves/
*
.c
../../monniaux/multithreaded_volatile/
*
.c
../../monniaux/nand/
*
.c
#../../monniaux/ncompress/*.c # Warnings
../../monniaux/number_theoretic_transform/
*
.c
../../monniaux/predicated/
*
.c
../../monniaux/regalloc/
*
.c
../../monniaux/rotate/
*
.c
../../monniaux/scheduling/
*
.c
../../monniaux/send_through/
*
.c
../../monniaux/tiny-AES-c/
*
.c
../../monniaux/varargs/
*
.c
../../monniaux/xor_and_mat/
*
.c
#../../monniaux/zlib-1.2.11/*.c # Warnings
)
#FILES=../c/*.c
CCOMP_BBLOCKS
=
"../../../ccomp -fno-postpass"
CCOMP_REF
=
"../../../../CompCert_kvx/ccomp"
COUNT
=
0
if
[
$WOFF
-eq
1
]
then
CCOMP_BBLOCKS
=
"
${
CCOMP_BBLOCKS
}
-w"
CCOMP_REF
=
"
${
CCOMP_REF
}
-w"
fi
for
files
in
${
DIRS
[@]
}
do
for
f
in
$files
do
BNAME
=
$(
basename
-s
.c
$f
)
SNAME
=
"
$BNAME
"
.s
SREFNAME
=
"
$BNAME
"
_ref.s
./
$CCOMP_BBLOCKS
-S
$f
-o
$SNAME
./
$CCOMP_REF
-dmach
-S
$f
-o
$SREFNAME
#diff -I '^//*' <(cut -c-5 $SNAME) <(cut -c-5 $SREFNAME) > /dev/null 2>&1
diff
-I
'^//*'
$SNAME
$SREFNAME
>
/dev/null 2>&1
error
=
$?
if
[
$error
-eq
0
]
then
echo
"[
$BNAME
] OK"
COUNT
=
$((
COUNT
+
1
))
elif
[
$error
-eq
1
]
then
echo
"[
$BNAME
] FAIL"
diff
-I
'^//*'
-y
$SNAME
$SREFNAME
exit
1
else
echo
"[
$BNAME
] FAIL"
echo
"[WARNING] There was something wrong with the diff command !"
exit
1
fi
done
done
echo
"[TOTAL]
$COUNT
tests PASSED"
if
[
$CLEAN
-eq
1
]
then
rm
*
.s
*
.mach
fi
test/aarch64/postpass_tests/postpass_exec_c_test.sh
deleted
100755 → 0
View file @
e37d655d
#!/bin/bash
CLEAN
=
0
WOFF
=
0
SRC
=
""
while
getopts
':cwi:'
'OPTKEY'
;
do
case
${
OPTKEY
}
in
c
)
CLEAN
=
1
;;
w
)
WOFF
=
1
;;
i
)
SRC
=
${
OPTARG
}
;;
esac
done
CCOMP
=
"../../../ccomp -static"
if
[
$WOFF
-eq
1
]
then
CCOMP
=
"
${
CCOMP
}
-w"
fi
BNAME
=
$(
basename
-s
.c
$SRC
)
SNAME
=
"
$BNAME
"
.s
SREFNAME
=
"
$BNAME
"
_ref.s
ENAME
=
"
$BNAME
"
EREFNAME
=
"
$BNAME
"
_ref
./
$CCOMP
-S
$SRC
-o
$SNAME
./
$CCOMP
-fno-postpass
-S
$SRC
-o
$SREFNAME
./
$CCOMP
$SRC
-o
$ENAME
./
$CCOMP
-fno-postpass
$SRC
-o
$EREFNAME
#diff -I '^//*' -y $SNAME $SREFNAME
if
[
$CLEAN
-eq
1
]
then
rm
$SNAME
$SREFNAME
$ENAME
$EREFNAME
fi
test/
aarch64
/c/add_return.c
→
test/
gourdinl
/c/add_return.c
View file @
dff562c4
File moved
test/
aarch64
/c/addresses.c
→
test/
gourdinl
/c/addresses.c
View file @
dff562c4
File moved
test/
aarch64
/c/arith.c
→
test/
gourdinl
/c/arith.c
View file @
dff562c4
File moved
test/
aarch64
/c/arith_print.c
→
test/
gourdinl
/c/arith_print.c
View file @
dff562c4
File moved
test/
aarch64
/c/armstrong.c
→
test/
gourdinl
/c/armstrong.c
View file @
dff562c4
File moved
test/
aarch64
/c/array1.c
→
test/
gourdinl
/c/array1.c
View file @
dff562c4
File moved
test/
aarch64
/c/array2.c
→
test/
gourdinl
/c/array2.c
View file @
dff562c4
File moved
test/
aarch64
/c/biggest_of_3_int.c
→
test/
gourdinl
/c/biggest_of_3_int.c
View file @
dff562c4
File moved
test/
aarch64
/c/bitwise1.c
→
test/
gourdinl
/c/bitwise1.c
View file @
dff562c4
File moved
test/
aarch64
/c/cpintarray.c
→
test/
gourdinl
/c/cpintarray.c
View file @
dff562c4
File moved
test/
aarch64
/c/enum1.c
→
test/
gourdinl
/c/enum1.c
View file @
dff562c4
File moved
test/
aarch64
/c/enum2.c
→
test/
gourdinl
/c/enum2.c
View file @
dff562c4
File moved
test/
aarch64
/c/floop.c
→
test/
gourdinl
/c/floop.c
View file @
dff562c4
File moved
test/
aarch64
/c/floor.c
→
test/
gourdinl
/c/floor.c
View file @
dff562c4
File moved
test/
aarch64
/c/funcs.c
→
test/
gourdinl
/c/funcs.c
View file @
dff562c4
File moved
test/
aarch64
/c/hello.c
→
test/
gourdinl
/c/hello.c
View file @
dff562c4
File moved
test/
aarch64
/c/if.c
→
test/
gourdinl
/c/if.c
View file @
dff562c4
File moved
Prev
1
2
Next
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment