diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
| commit | b4a08d0815342b6238d307864f0823d0f07bb691 (patch) | |
| tree | 85f48254ca79a6e2bc9d7359017a5731f98f897f /kvx/unittest | |
| parent | 490a6caea1a95cfdbddf7aca244fa6a1c83aa9a2 (diff) | |
| download | compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.tar.gz compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.zip | |
k1c -> kvx changes
Diffstat (limited to 'kvx/unittest')
| -rw-r--r-- | kvx/unittest/Makefile | 13 | ||||
| -rw-r--r-- | kvx/unittest/postpass_test.ml | 12 |
2 files changed, 25 insertions, 0 deletions
diff --git a/kvx/unittest/Makefile b/kvx/unittest/Makefile new file mode 100644 index 00000000..fcbede2d --- /dev/null +++ b/kvx/unittest/Makefile @@ -0,0 +1,13 @@ +# Needs to be called from CompCert root directory +# $ make -f kvx/unittest/Makefile postpass_test + +include Makefile.extr + +TEST_CMX=kvx/unittest/postpass_test.cmx + +UNITTEST_OBJS:=$(shell $(MODORDER) $(TEST_CMX)) + +postpass_test: $(UNITTEST_OBJS) + @echo "Linking $@ $(UNITTEST_OBJS)" + @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ + diff --git a/kvx/unittest/postpass_test.ml b/kvx/unittest/postpass_test.ml new file mode 100644 index 00000000..434bfaf7 --- /dev/null +++ b/kvx/unittest/postpass_test.ml @@ -0,0 +1,12 @@ +open Printf +open Asmblock +open Integers +open PostpassSchedulingOracle +open BinNums + +let test_schedule_sd = + let sd_inst = PStore (PStoreRRO (Psd, GPR12, GPR16, (Ofsimm (Ptrofs.of_int @@ Int.intval Z0)))) + in let bb = { header = []; body = [sd_inst]; exit = None } + in List.iter print_bb (smart_schedule bb) + +let _ = test_schedule_sd; printf "Done\n" |