diff options
Diffstat (limited to 'verilog/Op.v')
| -rw-r--r-- | verilog/Op.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/verilog/Op.v b/verilog/Op.v index 9f94828f..87986f78 100644 --- a/verilog/Op.v +++ b/verilog/Op.v @@ -778,7 +778,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* addrsymbol *) - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)... (* addrstack *) - - destruct sp... apply Val.Vptr_has_type. + - destruct sp... (* castsigned *) - destruct v0... - destruct v0... @@ -790,6 +790,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.sub. destruct v0; destruct v1... unfold Val.has_type; destruct Archi.ptr64... destruct Archi.ptr64... destruct (eq_block b b0)... + destruct (eq_block b b0)... (* mul, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... @@ -839,9 +840,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_addl. (* negl, subl *) - destruct v0... - - unfold Val.subl. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... + - unfold Val.subl. destruct v0; destruct v1... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... |