diff options
| author | James Pollard <james@pollard.dev> | 2020-07-02 21:57:03 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-07-02 21:57:03 +0100 |
| commit | 1d8afa5949cd192620e4649ae32df49bca4da3f8 (patch) | |
| tree | 2ecee8adc006452da1cf44a206f9e61db79773cc /src/verilog | |
| parent | 2b24cee5c228d36bfbe27799063df9797e85f17f (diff) | |
| download | vericert-1d8afa5949cd192620e4649ae32df49bca4da3f8.tar.gz vericert-1d8afa5949cd192620e4649ae32df49bca4da3f8.zip | |
Switch to uvalueToZ in lessdef.
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/Value.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 116986b..acabcf2 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -304,8 +304,8 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | val_value_lessdef_ptr: forall b off v', - off = Ptrofs.repr (valueToZ v') -> - (Z.modulo (valueToZ v') 4) = 0%Z -> + off = Ptrofs.repr (uvalueToZ v') -> + (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. |