diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-10-26 15:43:56 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-10-26 15:43:56 +0000 |
| commit | 4d82ea5f5930bcef8bd547f415c8c040165511e1 (patch) | |
| tree | a4ccb1282441dba555f16fc3ed1bf169b04111da /src/hls/ValueVal.v | |
| parent | 5cc780e10afa2851980fd3157644cccb1f528b1c (diff) | |
| download | vericert-4d82ea5f5930bcef8bd547f415c8c040165511e1.tar.gz vericert-4d82ea5f5930bcef8bd547f415c8c040165511e1.zip | |
Fix build error with ValueVal
Diffstat (limited to 'src/hls/ValueVal.v')
| -rw-r--r-- | src/hls/ValueVal.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v index e978782..b882dc6 100644 --- a/src/hls/ValueVal.v +++ b/src/hls/ValueVal.v @@ -34,14 +34,19 @@ on the size of the [value]. This is necessary so that we can easily store Using the default [word], this would not be possible, as the size is part of the type. *) -Definition value : Type := val. +(* Definition value : Type := val. (** ** Value conversions Various conversions to different number types such as [N], [Z], [positive] and [int], where the last one is a theory of integers of powers of 2 in CompCert. *) -Definition valueToNat (v : value) : nat := . +Definition valueToNat (v : value) : nat := + match v with + | value_bool b => Nat.b2n b + | value_int i => Z.to_nat (Int.unsigned i) + | value_int64 i => Z.to_nat (Int64.unsigned i) + end. Definition natToValue (n : nat) : value := value_int (Int.repr (Z.of_nat n)). @@ -201,3 +206,4 @@ Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_i ptrToValue in *) (*Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.*) +*) |