diff options
| author | Valentin Robert <valentin.robert.42@gmail.com> | 2025-12-08 06:03:00 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-12-08 14:03:00 +0000 |
| commit | 1993f2d414fe6326dc0855a901d620b82f582c71 (patch) | |
| tree | 6f10a57683f003767eb0ea4cddd4af72278c08a7 /model/CMakeLists.txt | |
| parent | 1c7910bc1a23107a9c36297e4ff733e457e052a4 (diff) | |
| download | sail-riscv-master.zip sail-riscv-master.tar.gz sail-riscv-master.tar.bz2 | |
Scatter the termination module in such a way that one could require some
termination measures without having to include every single instruction
in the output. This makes building a subset of the model easier.
The termination measures for `vmem_read_addr` and `vmem_write_addr` no
longer need to be protected only for the Rocq output, so they get taken
out of the `$iftarget coq`.
Diffstat (limited to 'model/CMakeLists.txt')
| -rw-r--r-- | model/CMakeLists.txt | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt index 957ab3c..191e77f 100644 --- a/model/CMakeLists.txt +++ b/model/CMakeLists.txt @@ -35,8 +35,6 @@ execute_process( ${SAIL_BIN} ${project_file} --require-version ${SAIL_REQUIRED_VER} - # include termination.sail in the list of dependencies - --variable "TERMINATION_FILE = true" --all-modules --list-files OUTPUT_VARIABLE sail_list_files @@ -380,7 +378,6 @@ foreach (xlen IN ITEMS 32 64) --config ${config_file} # Input files. ${SAIL_MODULES} - --variable "TERMINATION_FILE = true" ${project_file} ) add_custom_command( @@ -448,7 +445,6 @@ foreach (xlen IN ITEMS 32 64) ${lean_sail_common} ${lean_sail_default} ${SAIL_MODULES} - --variable "TERMINATION_FILE = true" ${project_file} ) add_custom_command( @@ -467,7 +463,6 @@ foreach (xlen IN ITEMS 32 64) ${lean_sail_common} ${lean_sail_executable} ${SAIL_MODULES} - --variable "TERMINATION_FILE = true" ${project_file} ) |