diff options
| author | James Pollard <james@pollard.dev> | 2020-06-23 23:00:08 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-23 23:01:44 +0100 |
| commit | ec0fa1ac249a8eeb0df9700c50a3e6c4f1b540f2 (patch) | |
| tree | e168031be13a7e4ed5f7b245c03b18fc48d8b49c /src/common/Coquplib.v | |
| parent | b70f007eae5886990a8ffc1e7b94294702e238f8 (diff) | |
| download | vericert-ec0fa1ac249a8eeb0df9700c50a3e6c4f1b540f2.tar.gz vericert-ec0fa1ac249a8eeb0df9700c50a3e6c4f1b540f2.zip | |
Normalise entire expression to avoid overflow issues.
Diffstat (limited to 'src/common/Coquplib.v')
| -rw-r--r-- | src/common/Coquplib.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 59b23ae..b4ca906 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -84,6 +84,11 @@ Ltac unfold_constants := | [ H : context[Integers.Ptrofs.max_signed] |- _ ] => replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity + | [ _ : _ |- context[Integers.Ptrofs.max_unsigned] ] => + replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity + | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] => + replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity + | [ _ : _ |- context[Integers.Int.modulus] ] => replace Integers.Int.modulus with 4294967296 by reflexivity | [ H : context[Integers.Int.modulus] |- _ ] => @@ -98,6 +103,11 @@ Ltac unfold_constants := replace Integers.Int.max_signed with 2147483647 by reflexivity | [ H : context[Integers.Int.max_signed] |- _ ] => replace Integers.Int.max_signed with 2147483647 in H by reflexivity + + | [ _ : _ |- context[Integers.Int.max_unsigned] ] => + replace Integers.Int.max_unsigned with 4294967295 by reflexivity + | [ H : context[Integers.Int.max_unsigned] |- _ ] => + replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity end. Ltac simplify := unfold_constants; simpl in *; |