diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 10:09:12 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 10:09:12 +0100 |
| commit | 9491b9dda35897c8abde560b79a323d47aac0ec4 (patch) | |
| tree | afe20a1f1e169c68e25a6a9c138b5898f6ce6693 /src/verilog | |
| parent | c5170915a81ca1bca420cd4683855cc7ba8ff8c4 (diff) | |
| parent | e05b93c540d2e0e2cb9f4ab01460eba080b65401 (diff) | |
| download | vericert-9491b9dda35897c8abde560b79a323d47aac0ec4.tar.gz vericert-9491b9dda35897c8abde560b79a323d47aac0ec4.zip | |
Merge branch 'arrays-proof' into develop
Diffstat (limited to 'src/verilog')
| -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 := |