summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-11 08:22:38 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-11 08:22:38 +0000
commit99b02bd388f2b84acf9c2c226bf2ac7703c03ba8 (patch)
tree535f92607fe6e16d05750d07234efe1cd6297141 /cfrontend
parent9e76f90bc5255d6ec933d705bf99baf3ca80d5d5 (diff)
Strip quotes from section names during #pragma parsing.
Reinstall the quotes when printing asm. The idea is that .sdump files now contain unquoted section names, which is easier on cchecklink. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1967 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/CPragmas.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 63bd3f9..7bf80bb 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -61,8 +61,8 @@ let re_start_pragma_section = Str.regexp "section\\b"
let re_pragma_section = Str.regexp(
"section[ \t]+"
^ "\\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+" (* class_name *)
-^ "\\(\"[^\"]*\"\\)?[ \t]*" (* istring *)
-^ "\\(\"[^\"]*\"\\)?[ \t]*" (* ustring *)
+^ "\"\\([^\"]*\\)\"?[ \t]*" (* istring *)
+^ "\"\\([^\"]*\\)\"?[ \t]*" (* ustring *)
^ "\\([a-zA-Z-]+\\)?[ \t]*" (* addressing mode *)
^ "\\([RWXON]*\\)" (* access mode *)
)