diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 23:27:05 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 23:27:05 +0100 |
| commit | 128b5d3a20647db3d0b17cc918d17fe5cadc07ff (patch) | |
| tree | 8dae891dc2f7d2387d823bd129da277123fec185 /src/verilog/ValueInt.v | |
| parent | 78e549331ba3f136ebe94955f68767bd384df454 (diff) | |
| download | vericert-128b5d3a20647db3d0b17cc918d17fe5cadc07ff.tar.gz vericert-128b5d3a20647db3d0b17cc918d17fe5cadc07ff.zip | |
Add top level backward simulation
Diffstat (limited to 'src/verilog/ValueInt.v')
| -rw-r--r-- | src/verilog/ValueInt.v | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index aa99fbd..f0f6de6 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -81,9 +81,7 @@ Search Ptrofs.of_int Ptrofs.to_int. Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) - | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z - then Some (ptrToValue off) - else None + | Values.Vptr b off => Some (ptrToValue off) | Values.Vundef => Some (ZToValue 0%Z) | _ => None end. @@ -117,7 +115,6 @@ Inductive val_value_lessdef: val -> value -> Prop := | val_value_lessdef_ptr: forall b off v', off = valueToPtr v' -> - (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -162,8 +159,5 @@ Proof. destruct v; try discriminate; constructor. unfold valToValue in H. inversion H. unfold valueToInt. unfold intToValue in H1. auto. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. - inv H1. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. - inv H1. apply Z.eqb_eq. apply Heqb0. + inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. Qed. |