diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-06 11:01:34 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-06 11:01:34 +0200 |
| commit | 3c605199ab0d096cd66ba671a4e23eac9e79bbc2 (patch) | |
| tree | 93e52e7505a47dd1e08db105d24c7fcd66097829 /cfrontend/Ctyping.v | |
| parent | fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69 (diff) | |
| download | compcert-kvx-3c605199ab0d096cd66ba671a4e23eac9e79bbc2.tar.gz compcert-kvx-3c605199ab0d096cd66ba671a4e23eac9e79bbc2.zip | |
Regression: handling of integer + pointer in CompCert C
During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented.
On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does.
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 521ae519..ba1d34fb 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -113,19 +113,13 @@ Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type := match op with | Oadd => match classify_add ty1 ty2 with - | add_case_pi ty _ (*| add_case_ip ty*) - | add_case_pl ty (*| add_case_lp ty*) => OK (Tpointer ty noattr) + | add_case_pi ty _ | add_case_ip _ ty + | add_case_pl ty | add_case_lp ty => OK (Tpointer ty noattr) | add_default => binarith_type ty1 ty2 "operator +" end | Osub => match classify_sub ty1 ty2 with | sub_case_pi ty _ | sub_case_pl ty => OK (Tpointer ty noattr) -(* - | sub_case_pp ty1 ty2 => - if type_eq (remove_attributes ty1) (remove_attributes ty2) - then OK (Tint I32 Signed noattr) - else Error (msg "operator - : incompatible pointer types") -*) | sub_case_pp ty => OK ptrdiff_t | sub_default => binarith_type ty1 ty2 "operator infix -" end @@ -1504,7 +1498,7 @@ Proof. intros until m; intros TY SEM WT1 WT2. destruct op; simpl in TY; simpl in SEM. - (* add *) - unfold sem_add in SEM; DestructCases; auto with ty. + unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty. eapply pres_sem_binarith; eauto; intros; exact I. - (* sub *) unfold sem_sub in SEM; DestructCases; auto with ty. |