From 6e0b5c4d5f70da024ef50cd45336041bff490034 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Mon, 9 Sep 2024 16:05:36 +0100 Subject: [PATCH] Remove ability to compile to OCaml This will allow the OCaml backend to be improved in the Sail compiler. --- Makefile | 4 ---- README.md | 9 --------- 2 files changed, 13 deletions(-) diff --git a/Makefile b/Makefile index 0f44685e9..34fd2bf68 100644 --- a/Makefile +++ b/Makefile @@ -228,10 +228,6 @@ riscv.smt_model: $(SAIL_SRCS) cgen: $(SAIL_SRCS) model/main.sail $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -generated_definitions/ocaml/$(ARCH)/riscv.ml: $(SAIL_SRCS) Makefile - mkdir -p generated_definitions/ocaml/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml/$(ARCH) -o riscv $(SAIL_SRCS) - cloc: cloc --by-file --force-lang C,sail $(SAIL_SRCS) diff --git a/README.md b/README.md index 0e54773cd..d8edcca03 100644 --- a/README.md +++ b/README.md @@ -204,15 +204,6 @@ Those tests have also been run on RISC-V hardware, on a SiFive RISC-V FU540 multicore proto board (Freedom Unleashed), kindly on loan from Imperas. To date, only sequentially consistent behaviour was observed there. -Use in test generation ----------------------- - -The Sail OCaml backend can produce QuickCheck-style random generators for -types in Sail specifications, which have been used to produce random -instructions sequences for testing. The generation of individual -types can be overridden by the developer to, for example, remove -implementation-specific instructions or introduce register biasing. - Generating theorem-prover definitions --------------------------------------