diff options
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 18a69ef..ad946ca 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -294,6 +294,11 @@ Inductive val_value_lessdef: val -> value -> Prop := forall i v', i = valueToInt v' -> 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 -> + val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. Inductive opt_val_value_lessdef: option val -> value -> Prop := |