Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

bundled version of l3 riscv model and step #195

Merged
merged 16 commits into from
Dec 5, 2024
Merged

bundled version of l3 riscv model and step #195

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
55521e9
Small fix to tutorial Makefile
didriklundberg Nov 22, 2024
72c6787
Merge pull request #194 from kth-step/dev_tutorial_fix
didriklundberg Nov 23, 2024
26c5108
Changed installation script to install branch from kth-step fork instead
didriklundberg Oct 21, 2020
d7eca9e
Bugfix for alternate branch-specific HOL4, small changes in RISC-V se…
didriklundberg Oct 27, 2020
41a1c37
Small changes to selftests, some work on CSR instruction lifting
didriklundberg Oct 28, 2020
4d178e4
CSRRW, CSRRS, CSRRC, CSRRWI, CSRRSI and CSRRCI instructions now lifti…
didriklundberg Oct 28, 2020
10ace80
Typos
didriklundberg Oct 28, 2020
cae4f3e
Fixing rebase typo
didriklundberg Dec 2, 2024
f922ca7
Typo fix + backlifter fix for latest RISC-V L3 model
didriklundberg Dec 2, 2024
9a76df9
Added support for more CSR registers in RISC-V lifter and backlifter
didriklundberg Dec 5, 2024
541d525
bundled version of l3 riscv model and step from trindemossen-1
palmskog Dec 5, 2024
caf07c3
Added the capability of executing CSR instructions to riscv_stepLib
didriklundberg Dec 5, 2024
9cc7ffb
Changed CSR addresses and names in the RISC-V L3 model to agree with …
didriklundberg Dec 5, 2024
b99b4f4
use Holmakefile path relative to HOLBADIR
palmskog Dec 5, 2024
537ad23
Merge pull request #196 from kth-step/dev_riscv_l3_lifter_t1
palmskog Dec 5, 2024
60d1af3
Failing results in selftest logs now in order of occurrence
didriklundberg Dec 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions examples/aes/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/aes/exec/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/tools/lifter \
Expand Down
4 changes: 2 additions & 2 deletions examples/aes/lifter/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/tools/exec \
$(HOLBADIR)/src/tools/lifter

Expand Down
4 changes: 2 additions & 2 deletions examples/aes/wp/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/bsl-wp-smt/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/smt \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
Expand Down
4 changes: 2 additions & 2 deletions examples/nic/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/smt \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/aes-unopt/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/aes/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/chacha/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/chachapoly/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/ifelse/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/incr-mem/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/incr/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/isqrt/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/kernel/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/mod2-mem/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/mod2/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/modexp/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/motor/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/perftest/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/poly1305-inlined/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/poly1305/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/swap/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/riscv/symbexectests/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
$(HOLBADIR)/src/theory/program_logic \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/2-lift/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/4-bir-to-arm/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/5-wp/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/6-smt/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/7-composition/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/theory/bir \
$(HOLBADIR)/src/theory/bir-support \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/8-symbexec/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLDIR)/examples/l3-machine-code/arm8/step \
$(HOLDIR)/examples/l3-machine-code/m0/model \
$(HOLDIR)/examples/l3-machine-code/m0/step \
$(HOLDIR)/examples/l3-machine-code/riscv/model \
$(HOLDIR)/examples/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
$(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
$(HOLBADIR)/src/shared \
$(HOLBADIR)/src/tools/symbexec \
$(HOLBADIR)/examples/tutorial/2-lift \
Expand Down
4 changes: 2 additions & 2 deletions examples/tutorial/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@

MAKEFILE_DIRS=1-code 3-exec 8-symbexec
HOLMAKEFILE_DIRS=2-lift 4-bir-to-arm 5-wp 6-smt 7-composition support support2
HOLMAKEFILE_DIRS=2-lift 4-bir-to-arm 5-wp 6-smt 7-composition

##########################################################

.DEFAULT_GOAL := all
all: 7-composition support2
all: 7-composition

##########################################################

Expand Down
1 change: 0 additions & 1 deletion scripts/setup/install_hol4.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,4 +117,3 @@ do
cd "${HOL4_DIR}/${dir}"
${HOL4_DIR}/bin/Holmake
done

Loading
Loading