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.

2 files changed, 5 insertions, 4 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 810514a3..80e33b2b 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -100,7 +100,7 @@ let rec fixup_variadic_call ri rf tyl =
         end
         
 let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
+  if (sg.sig_cc.cc_vararg <> None) then fixup_variadic_call 0 0 sg.sig_args
 
 (* Handling of annotations *)
 
@@ -588,7 +588,7 @@ let expand_instruction instr =
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (X30, X2));
-      if sg.sig_cc.cc_vararg then begin
+      if (sg.sig_cc.cc_vararg <> None) then begin
         let n = arguments_size sg in
         let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
@@ -606,7 +606,7 @@ let expand_instruction instr =
   | Pfreeframe (sz, ofs) ->
      let sg = get_current_function_sig() in
      let extra_sz =
-      if sg.sig_cc.cc_vararg then begin
+      if (sg.sig_cc.cc_vararg <> None) then begin
         let n = arguments_size sg in
         if n >= 8 then 0 else align ((8 - n) * wordsize) 16
       end else 0 in
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 17326139..74c99d07 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -281,7 +281,8 @@ Fixpoint loc_arguments_rec (va: bool)
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
+  let va := match s.(sig_cc).(cc_vararg) with Some _ => true | None => false end in
+  loc_arguments_rec va s.(sig_args) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)