diff options
| author | Thomas Bauereiss | 2018-05-04 20:29:19 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-04 20:29:19 +0100 |
| commit | f469001209e0333dbdd8fe42c7232c92a6c1be6f (patch) | |
| tree | 0673f2b58eef0efc16da0219dde61328b1ef22b9 /cheri/Makefile | |
| parent | 05a4a75d328d3bd8469167f6f23dda918146117a (diff) | |
Add back purely sequential Lem generation
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
Diffstat (limited to 'cheri/Makefile')
| -rw-r--r-- | cheri/Makefile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 01583280..d053fc67 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -54,6 +54,11 @@ cheri.lem: $(CHERI_SAILS) $(SAIL) -lem -o cheri -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri_types.lem: cheri.lem +cheri_sequential.lem: $(CHERI_SAILS) + $(SAIL) -lem -o cheri_sequential -auto_mono -mono_rewrites -lem_mwords -lem_sequential -lem_lib Mips_extras_sequential -undefined_gen -memo_z3 $^ +cheri_sequential_types.lem: cheri_sequential.lem +Cheri_sequential.thy: $(MIPS_SAIL_DIR)/mips_extras_sequential.lem + cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS) $(SAIL) -lem -o cheri128_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri128_no_tlb_types.lem: cheri128_no_tlb.lem |