diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
| commit | 5664fddcab15ef4482d583673c75e07bd1e96d0a (patch) | |
| tree | 878b22860e69405ba5cf6fd2798731dac8ce660c /arm/Stacklayout.v | |
| parent | b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff) | |
| parent | fe73ed58ef80da7c53c124302a608948fb190229 (diff) | |
| download | compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip | |
Merge remote-tracking branch 'origin/master' into parser_fix
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. |