aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintCsyntax.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2020-09-08 13:56:01 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2020-12-25 18:34:24 +0100
commit9ab3738ae87a554fb742420b8c81ced4cd3c66c7 (patch)
treecc17ce961dfc2f8dd13f4428b0814c8fe66be254 /cfrontend/PrintCsyntax.ml
parenta138b43ccb391be63bed2fea26cd36dab96b091f (diff)
downloadcompcert-kvx-9ab3738ae87a554fb742420b8c81ced4cd3c66c7.tar.gz
compcert-kvx-9ab3738ae87a554fb742420b8c81ced4cd3c66c7.zip
Changed cc_varargs to an option type
Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
-rw-r--r--cfrontend/PrintCsyntax.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 97a00b09..c49f6cd4 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -111,8 +111,8 @@ let rec name_cdecl id ty =
| Tnil ->
if first then
Buffer.add_string b
- (if cconv.cc_vararg then "..." else "void")
- else if cconv.cc_vararg then
+ (if cconv.cc_vararg <> None then "..." else "void")
+ else if cconv.cc_vararg <> None then
Buffer.add_string b ", ..."
else
()
@@ -400,11 +400,11 @@ let name_function_parameters name_param fun_name params cconv =
Buffer.add_char b '(';
begin match params with
| [] ->
- Buffer.add_string b (if cconv.cc_vararg then "..." else "void")
+ Buffer.add_string b (if cconv.cc_vararg <> None then "..." else "void")
| _ ->
let rec add_params first = function
| [] ->
- if cconv.cc_vararg then Buffer.add_string b ",..."
+ if cconv.cc_vararg <> None then Buffer.add_string b ",..."
| (id, ty) :: rem ->
if not first then Buffer.add_string b ", ";
Buffer.add_string b (name_cdecl (name_param id) ty);