diff options
Diffstat (limited to 'lib/coq/Sail2_state.v')
| -rw-r--r-- | lib/coq/Sail2_state.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index 7e10aba3..1d5cb342 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -15,6 +15,7 @@ let rec liftState ra s = match s with | (Write_tagv t k) -> bindS (write_tagS t) (fun v -> liftState ra (k v)) | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) + | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) | (Footprint k) -> liftState ra k |