aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2020-03-29 11:35:58 +0200
committerGitHub <noreply@github.com>2020-03-29 11:35:58 +0200
commit14f89bf9c397a4268d2b47418de234992b008d6c (patch)
treeb8a4c89a7762d00121a71308bfb99d0af9b487f9 /cfrontend
parent039b532ae972292ec2f726505422afd49569b738 (diff)
downloadcompcert-kvx-14f89bf9c397a4268d2b47418de234992b008d6c.tar.gz
compcert-kvx-14f89bf9c397a4268d2b47418de234992b008d6c.zip
Explicit error messages for ill-formed section attributes (#232)
Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them.
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 293e79f0..7f796fe3 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1234,7 +1234,7 @@ let convertFundef loc env fd =
{ a_storage = fd.fd_storage;
a_alignment = None;
a_size = None;
- a_sections = Sections.for_function env id' fd.fd_attrib;
+ a_sections = Sections.for_function env loc id' fd.fd_attrib;
a_access = Sections.Access_default;
a_inline = inline;
a_loc = loc };
@@ -1311,7 +1311,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
| Some i ->
convertInitializer env ty i in
let (section, access) =
- Sections.for_variable env id' ty (optinit <> None) in
+ Sections.for_variable env loc id' ty (optinit <> None) in
if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then
error "'%s' is too big (%s bytes)"
id.name (Z.to_string sz);