diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-01 21:27:26 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-01 21:27:26 +0100 |
| commit | aa28022035b16417aaafa36a450461c5133a44b4 (patch) | |
| tree | eab9b670cf05d4d86d8789ed221bc6acbae98ed0 /src/translation/HTLgenspec.v | |
| parent | 7af499d9fb8e98a1d2fec35cd433bf676e31e93a (diff) | |
| parent | 995ab555d848fcf6188734e6b46677131d4cc173 (diff) | |
| download | vericert-aa28022035b16417aaafa36a450461c5133a44b4.tar.gz vericert-aa28022035b16417aaafa36a450461c5133a44b4.zip | |
Merge remote-tracking branch 'james/develop' into develop
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a78256b..0cdecba 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -426,7 +426,7 @@ Proof. destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; - simplify; + crush; monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) |