diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-03-27 16:58:38 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-03-27 16:58:38 +0200 |
| commit | 96abbcd8f25f03352ff397c2dd442015269722b8 (patch) | |
| tree | 317386fd16faf3cc279248af63c3aa36112b3e79 /cparser/Elab.ml | |
| parent | 3837216731df1417eeb8885d472ffbd8f87fa144 (diff) | |
| download | compcert-96abbcd8f25f03352ff397c2dd442015269722b8.tar.gz compcert-96abbcd8f25f03352ff397c2dd442015269722b8.zip | |
Arrays should decay to pointers (#65)
Arrays should decay to pointers except if they are used as operands of sizeof, _Alignof or as
operand of the unary &. The "comma" sequencing operator was missing a "decay" on the type of its second argument. All other operators "decay" their operands correctly.
Bug 23299
Bug 23311
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index e878a2b2..3ef489c1 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1557,7 +1557,7 @@ let elab_expr vararg loc env a = emit_elab ~linkage env loc (Gdecl(sto, id, ty, None)); { edesc = EVar id; etyp = ty },env | _ -> elab env a1 in - let bl = mmap elab env al in + let bl = mmap elab env al in (* Extract type information *) let (res, args, vararg) = match unroll env b1.etyp with @@ -1956,7 +1956,8 @@ let elab_expr vararg loc env a = | BINARY(COMMA, a1, a2) -> let b1,env = elab env a1 in let b2,env = elab env a2 in - { edesc = EBinop (Ocomma, b1, b2, b2.etyp); etyp = b2.etyp },env + let ty2 = pointer_decay env b2.etyp in + { edesc = EBinop (Ocomma, b1, b2, ty2); etyp = ty2 },env (* Elaboration of pre- or post- increment/decrement *) and elab_pre_post_incr_decr op msg a1 = |