diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /arm/Stacklayout.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'arm/Stacklayout.v')
| -rw-r--r-- | arm/Stacklayout.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index 7694dcfe..82d11727 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -112,7 +112,7 @@ Proof. set (x1 := 4 * bound_outgoing b). assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. set (x2 := align x1 8). - assert (8 | x2). apply align_divides. omega. + assert (8 | x2). apply align_divides. omega. set (x3 := x2 + 4 * bound_local b). assert (4 | x3). apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists (bound_local b); ring. @@ -121,10 +121,10 @@ Proof. set (x5 := x4 + 8 * bound_float_callee_save b). assert (8 | x5). apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. assert (4 | x5). apply Zdivides_trans with 8; auto. exists 2; auto. - set (x6 := x5 + 4). + set (x6 := x5 + 4). assert (4 | x6). apply Zdivide_plus_r; auto. exists 1; auto. set (x7 := x6 + 4). - assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega. + assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega. apply Zdivide_plus_r; auto. exists 1; auto. set (x8 := align (x7 + bound_stack_data b) 8). assert (8 | x8). apply align_divides. omega. |