Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed

12 files changed, 604 insertions, 420 deletions

diff --git a/test/Makefile b/test/Makefile
index c371e18a..50cf57fb 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -1,12 +1,13 @@
 include ../Makefile.config
 
-#DIRS=c compression raytracer spass regression
+#DIRS=c compression raytracer spass regression abi
 
 # Kalray note - removing compression, raytracer and spass that cannot be executed by the simulator in reasonable time
+# TODO: abi for Kalray ?
 ifeq ($(ARCH),kvx)
 	DIRS=c regression
 else
-	DIRS=c compression raytracer spass regression
+	DIRS=c compression raytracer spass regression abi
 endif
 
 ifeq ($(CLIGHTGEN),true)
diff --git a/test/abi/.gitignore b/test/abi/.gitignore
new file mode 100644
index 00000000..c115947e
--- /dev/null
+++ b/test/abi/.gitignore
@@ -0,0 +1,8 @@
+*.exe
+*.c
+*.h
+*.compcert
+*.cc2compcert
+*.compcert2cc
+*.light.c
+*.s
diff --git a/test/abi/Makefile b/test/abi/Makefile
new file mode 100644
index 00000000..eb9ca292
--- /dev/null
+++ b/test/abi/Makefile
@@ -0,0 +1,75 @@
+include ../../Makefile.config
+
+CCOMP=../../ccomp -stdlib ../../runtime
+CCOMPFLAGS=
+CFLAGS=-O -Wno-overflow -Wno-constant-conversion
+
+TESTS=fixed.compcert fixed.cc2compcert fixed.compcert2cc \
+     vararg.compcert vararg.cc2compcert vararg.compcert2cc \
+     struct.compcert struct.cc2compcert struct.compcert2cc
+
+all: $(TESTS)
+
+all_s: fixed_def_compcert.s fixed_use_compcert.s \
+       vararg_def_compcert.s vararg_use_compcert.s \
+       struct_def_compcert.s struct_use_compcert.s
+
+test:
+	@set -e; for t in $(TESTS); do \
+          SIMU='$(SIMU)' ARCH=$(ARCH) MODEL=$(MODEL) ABI=$(ABI) SYSTEM=$(SYSTEM) ./Runtest $$t; \
+         done
+
+generator.exe: generator.ml
+	ocamlopt -g -o $@ generator.ml
+
+clean::
+	rm -f generator.exe *.cm[iox]
+
+fixed_decl.h: generator.exe
+	./generator.exe -rnd 500 -o fixed
+
+fixed_def.c fixed_use.c: fixed_decl.h
+
+clean::
+	rm -f fixed_decl.h fixed_def.c fixed_use.c
+
+vararg_decl.h: generator.exe
+	./generator.exe -vararg -rnd 500 -o vararg
+
+vararg_def.c vararg_use.c: vararg_decl.h
+
+clean::
+	rm -f vararg_decl.h vararg_def.c vararg_use.c
+
+struct_decl.h: generator.exe
+	./generator.exe -structs -o struct
+
+struct_def.c struct_use.c: struct_decl.h
+
+clean::
+	rm -f struct_decl.h struct_def.c struct_use.c
+
+struct%.o: CCOMPFLAGS += -fstruct-passing -dclight
+
+%_compcert.o: %.c
+	$(CCOMP) $(CCOMPFLAGS) -c -o $@ $*.c
+%_cc.o: %.c
+	$(CC) $(CFLAGS) -c -o $@ $*.c
+
+%_compcert.s: %.c
+	$(CCOMP) -S -o $@ $*.c
+%_cc.s: %.c
+	$(CC) $(CFLAGS) -S -o $@ $*.c
+
+%.compcert: %_def_compcert.o %_use_compcert.o
+	$(CCOMP) -o $@ $*_def_compcert.o $*_use_compcert.o
+
+%.cc2compcert: %_def_compcert.o %_use_cc.o
+	$(CCOMP) -o $@ $*_def_compcert.o $*_use_cc.o
+
+%.compcert2cc: %_def_cc.o %_use_compcert.o
+	$(CCOMP) -o $@ $*_def_cc.o $*_use_compcert.o
+
+clean::
+	rm -f *.[os] *.compcert *.cc2compcert *.compcert2cc *.light.c
+
diff --git a/test/abi/Runtest b/test/abi/Runtest
new file mode 100755
index 00000000..7ec63188
--- /dev/null
+++ b/test/abi/Runtest
@@ -0,0 +1,41 @@
+#!/bin/sh
+
+# The name of the test
+name="$1"
+
+# Skip the test if known to fail
+
+skip () {
+  echo "$name: skipped"
+  exit 0
+}
+
+case "$name" in
+  fixed.cc2compcert|fixed.compcert2cc)
+    if [ $ARCH = arm ] && [ $ABI = hardfloat ] ; then skip; fi
+    ;;
+  struct.cc2compcert|struct.compcert2cc)
+    if [ $ARCH = x86 ] && [ $MODEL = 32sse2 ] ; then
+       # works except on Cygwin
+       if [ $SYSTEM = cygwin ] ; then skip; fi
+    elif [ $ARCH = powerpc ] && [ $ABI = linux ] ; then
+       # works
+       :
+    else
+       skip
+    fi
+    ;;
+esac
+
+# Administer the test
+
+if $SIMU ./$name
+then
+  echo "$name: passed"
+  exit 0
+else
+  echo "$name: FAILED"
+  exit 2
+fi
+
+  
diff --git a/test/abi/generator.ml b/test/abi/generator.ml
new file mode 100644
index 00000000..aecee7cf
--- /dev/null
+++ b/test/abi/generator.ml
@@ -0,0 +1,458 @@
+open Printf
+
+type ty =
+  | Int8u  | Int8s
+  | Int16u | Int16s
+  | Int32
+  | Int64
+  | Float32
+  | Float64
+  | String
+  | Struct of int * (string * ty) list
+
+type funsig = {
+    args: ty list;
+    varargs: ty list;    (* empty list if fixed-argument function *)
+    res: ty option
+  }
+
+type value =
+  | VInt of int
+  | VInt32 of int32
+  | VInt64 of int64
+  | VFloat of float
+  | VString of string
+  | VStruct of value list
+
+(* Print a value.  If [norm] is true, re-normalize values of
+   small numerical types. *)
+
+let zero_ext n k =
+  n land ((1 lsl k) - 1)
+
+let sign_ext n k =
+  (n lsl (Sys.int_size - k)) asr (Sys.int_size - k)
+
+let normalize_float32 n =
+  Int32.float_of_bits (Int32.bits_of_float n)
+
+let rec print_value ~norm oc (ty, v) =
+  match (ty, v) with
+  | (Int8u, VInt n) ->
+      fprintf oc "%d" (if norm then zero_ext n 8 else n)
+  | (Int8s, VInt n) ->
+      fprintf oc "%d" (if norm then sign_ext n 8 else n)
+  | (Int16u, VInt n) ->
+      fprintf oc "%d" (if norm then zero_ext n 16 else n)
+  | (Int16s, VInt n) ->
+      fprintf oc "%d" (if norm then sign_ext n 16 else n)
+  | (Int32, VInt32 n) ->
+      fprintf oc "%ld" n
+  | (Int64, VInt64 n) ->
+      fprintf oc "%Ld" n
+  | (Float32, VFloat f) ->
+      if norm
+      then fprintf oc "%hF" (normalize_float32 f)
+      else fprintf oc "%h" f
+  | (Float64, VFloat f) ->
+      fprintf oc "%h" f
+  | (String, VString s) ->
+      fprintf oc "%S" s
+  | (Struct(id, (fld1, ty1) :: members), VStruct (v1 :: vl)) ->
+      fprintf oc "(struct s%d){" id;
+      print_value ~norm oc (ty1, v1);
+      List.iter2
+        (fun (fld, ty) v -> fprintf oc ", %a" (print_value ~norm) (ty, v))
+        members vl;
+      fprintf oc "}"
+  | _, _ ->
+      assert false
+
+(* Generate random values of the given type *)
+
+let random_char () = Char.chr (Char.code 'a' + Random.int 26)
+
+let random_string () =
+  let len = Random.int 3 in
+  String.init len (fun _ -> random_char ())
+
+let random_int () =
+  Random.bits() - (1 lsl 29)
+
+let random_int32 () =
+  Int32.(logxor (of_int (Random.bits()))
+                (shift_left (of_int (Random.bits())) 30))
+
+let random_int64 () =
+  Int64.(logxor (of_int (Random.bits()))
+                (logxor (shift_left (of_int (Random.bits())) 30)
+                        (shift_left (of_int (Random.bits())) 60)))
+
+let random_float64 () =
+  Random.float 100.0 -. 50.0
+
+(* Returns a random value.  Small numerical types are not normalized. *)
+
+let rec random_value = function
+  | Int8u | Int8s | Int16u | Int16s ->
+      VInt (random_int())
+  | Int32 ->
+      VInt32 (random_int32())
+  | Int64 ->
+      VInt64 (random_int64())
+  | Float32 | Float64 ->
+      VFloat (random_float64())
+  | String ->
+      VString (random_string())
+  | Struct(id, members) ->
+      VStruct (List.map (fun (fld, ty) -> random_value ty) members)
+
+let random_retvalue = function
+  | None -> VInt 0 (* meaningless *)
+  | Some ty -> random_value ty
+
+(* Generate function declaration, definition, and call *)
+
+let string_of_ty = function
+  | Int8u -> "unsigned char"
+  | Int8s -> "signed char"
+  | Int16u -> "unsigned short"
+  | Int16s -> "short"
+  | Int32 -> "int"
+  | Int64 -> "long long"
+  | Float32 -> "float"
+  | Float64 -> "double"
+  | String -> "char *"
+  | Struct(id, _) -> sprintf "struct s%d" id
+
+let string_of_optty = function
+  | None -> "void"
+  | Some t -> string_of_ty t
+
+let declare_struct oc id members =
+  fprintf oc "struct s%d {\n" id;
+  List.iter
+    (fun (fld, ty) -> fprintf oc "  %s %s;\n" (string_of_ty ty) fld)
+    members;
+  fprintf oc "};\n"
+
+let declare_function oc name sg =
+  fprintf oc "%s %s(" (string_of_optty sg.res) name;
+  begin match sg.args with
+  | [] -> fprintf oc "void"
+  | t0 :: tl ->
+      fprintf oc "%s x0" (string_of_ty t0);
+      List.iteri (fun n t -> fprintf oc ", %s x%d" (string_of_ty t) (n + 1)) tl;
+      if sg.varargs <> [] then fprintf oc ", ..."
+  end;
+  fprintf oc ")"
+
+let rec compare_value oc variable value ty =
+  match ty with
+  | Struct(id, members) ->
+      begin match value with
+      | VStruct vl ->
+          List.iter2
+            (fun (fld, ty) v ->
+              compare_value oc (sprintf "%s.%s" variable fld) v ty)
+            members vl
+      | _ ->
+          assert false
+      end
+  | String ->
+      fprintf oc "  check (strcmp(%s, %a) == 0);\n"
+                 variable (print_value ~norm:true) (ty, value)
+  | _ ->
+      fprintf oc "  check (%s == %a);\n"
+                 variable (print_value ~norm:true) (ty, value)
+
+let define_function oc name sg vargs vres =
+  declare_function oc name sg;
+  fprintf oc "\n{\n";
+  if sg.varargs <> [] then begin
+    fprintf oc "  va_list l;\n";
+    fprintf oc "  va_start(l, x%d);\n" (List.length sg.args - 1);
+    List.iteri
+      (fun n t ->
+        fprintf oc "  %s x%d = va_arg(l, %s);\n"
+                   (string_of_ty t) (n + List.length sg.args) (string_of_ty t))
+      sg.varargs;
+    fprintf oc "  va_end(l);\n";
+  end;
+  List.iteri
+    (fun n (t, v) -> compare_value oc (sprintf "x%d" n) v t)
+    (List.combine (sg.args @ sg.varargs) vargs);
+  begin match sg.res with
+    | None -> ()
+    | Some tres ->
+        fprintf oc "  return %a;\n" (print_value ~norm:false) (tres, vres)
+  end;
+  fprintf oc "}\n\n"
+
+let call_function oc name sg vargs vres =
+  fprintf oc "void call_%s(void)\n" name;
+  fprintf oc "{\n";
+  begin match sg.res with
+  | None -> fprintf oc "  %s(" name
+  | Some t -> fprintf oc "  %s r = %s(" (string_of_ty t) name
+  end;
+  begin match (sg.args @ sg.varargs), vargs with
+  | [], [] -> ()
+  | ty1 :: tyl, v1 :: vl ->
+      print_value ~norm:false oc (ty1, v1);
+      List.iter2
+        (fun ty v -> fprintf oc ", %a" (print_value ~norm:false) (ty, v))
+        tyl vl
+  | _, _ ->
+      assert false
+  end;
+  fprintf oc ");\n";
+  begin match sg.res with
+  | None -> ()
+  | Some tyres -> compare_value oc "r" vres tyres
+  end;
+  fprintf oc "}\n\n"
+
+let function_counter = ref 0
+
+let generate_one_test oc0 oc1 oc2 sg =
+  incr function_counter;
+  let num = !function_counter in
+  let vargs = List.map random_value (sg.args @ sg.varargs) in
+  let vres = random_retvalue sg.res in
+  let name = "f" ^ string_of_int num in
+  fprintf oc0 "extern ";
+  declare_function oc0 name sg;
+  fprintf oc0 ";\n";
+  define_function oc1 name sg vargs vres;
+  call_function oc2 name sg vargs vres
+
+let call_all_test oc =
+  fprintf oc "int main(void)\n";
+  fprintf oc "{\n";
+  fprintf oc "  alarm(60);\n";
+  for i = 1 to !function_counter do
+    fprintf oc "  call_f%d();\n" i
+  done;
+  fprintf oc "  return failed;\n";
+  fprintf oc "}\n"
+
+(* Generate interesting function signatures *)
+
+let all_ty =
+  [| Int8u; Int8s; Int16u; Int16s; Int32; Int64; Float32; Float64; String |]
+
+let base_ty =
+  [| Int32; Int64; Float32; Float64 |]
+
+let makerun pat len =
+  let rec make i l =
+    if l <= 0
+    then []
+    else pat.(i) :: make ((i + 1) mod (Array.length pat)) (l - 1)
+  in make 0 len
+
+let gen_fixed_sigs f =
+  (* All possible return types *)
+  Array.iter
+    (fun ty -> f { args = []; varargs = []; res = Some ty })
+    all_ty;
+  (* All possible argument types *)
+  Array.iter
+    (fun ty -> f { args = [ty]; varargs = []; res = None })
+    all_ty;
+  (* 2 arguments of base types *)
+  Array.iter
+    (fun ty1 ->
+      Array.iter
+        (fun ty2 -> f { args = [ty1; ty2]; varargs = []; res = None })
+        base_ty)
+    base_ty;
+  (* 3 arguments of base types *)
+  Array.iter
+    (fun ty1 ->
+      Array.iter
+        (fun ty2 ->
+          Array.iter
+            (fun ty3 -> f { args = [ty1; ty2; ty3]; varargs = []; res = None })
+            base_ty)
+        base_ty)
+    base_ty;
+  (* 4 arguments of base types *)
+  Array.iter
+    (fun ty1 ->
+      Array.iter
+        (fun ty2 ->
+          Array.iter
+            (fun ty3 ->
+              Array.iter
+                (fun ty4 ->
+                   f { args = [ty1; ty2; ty3; ty4]; varargs = []; res = None })
+                base_ty)
+            base_ty)
+        base_ty)
+    base_ty;
+  (* Runs of 6, 8, 10, 12, 16, 32 arguments of various patterns *)
+  Array.iter
+    (fun pat ->
+      Array.iter
+        (fun len ->
+          f { args = makerun pat len; varargs = []; res = None })
+        [| 6;8;10;12;16;32 |])
+    [| [|Int32|]; [|Int64|]; [|Float32|]; [|Float64|];
+       [|Int32;Int64|]; [|Int32;Float32|]; [|Int32;Float64|]; 
+       [|Int64;Float32|]; [|Int64;Float64|]; [|Float32;Float64|];
+       [|Int32;Int64;Float32;Float64|]
+    |]
+
+let split_list l n =
+  let rec split l n accu =
+    if n <= 0 then (List.rev accu, l) else
+      match l with
+      | [] -> assert false
+      | h :: t -> split t (n - 1) (h :: accu)
+  in split l n []
+
+let is_vararg_type = function
+  | Int32 | Int64 | Float64 | String -> true
+  | _ -> false
+
+let gen_vararg_sigs f =
+  let make_vararg sg n =
+    if List.length sg.args > n then begin
+      let (fixed, varia) = split_list sg.args n in
+      if List.for_all is_vararg_type varia
+      && is_vararg_type (List.nth fixed (n - 1)) then
+        f { args = fixed; varargs = varia; res = sg.res }
+    end
+  in
+    gen_fixed_sigs
+     (fun sg -> make_vararg sg 2; make_vararg sg 6; make_vararg sg 14)
+
+(* Generate interesting struct types *)
+
+let struct_counter = ref 0
+
+let mkstruct oc members =
+  incr struct_counter;
+  let id = !struct_counter in
+  declare_struct oc id members;
+  Struct(id, members)
+
+let member_ty =
+  [| Int8u; Int16u; Int32; Int64; Float32; Float64 |]
+
+let gen_structs oc f =
+  (* One field of any type *)
+  Array.iter
+    (fun ty -> f (mkstruct oc [("a", ty)]))
+    all_ty;
+  (* Two fields of interesting types *)
+  Array.iter
+    (fun ty1 ->
+      Array.iter
+        (fun ty2 -> f (mkstruct oc [("a", ty1); ("b", ty2)]))
+        member_ty)
+    member_ty;
+  (* 3, 4, 6, 8 fields of identical interesting type *)
+  Array.iter
+    (fun ty ->
+       f (mkstruct oc [("a", ty); ("b", ty); ("c", ty)]);
+       f (mkstruct oc [("a", ty); ("b", ty); ("c", ty); ("d", ty)]);
+       f (mkstruct oc [("a", ty); ("b", ty); ("c", ty); ("d", ty);
+                       ("e", ty); ("f", ty)]);
+       f (mkstruct oc [("a", ty); ("b", ty); ("c", ty); ("d", ty);
+                       ("e", ty); ("f", ty); ("g", ty); ("h", ty)]))
+    member_ty
+
+let gen_struct_sigs oc f =
+  let make ty =
+    (* Struct return *)
+    f { args = []; varargs = []; res = Some ty };
+    (* Struct passing (once, twice) *)
+    f { args = [ty]; varargs = []; res = None };
+    f { args = [ty;ty]; varargs = []; res = None };
+    (* Struct passing mixed with scalar arguments *)
+    f { args = [Int32;ty]; varargs = []; res = None };
+    f { args = [Float64;ty]; varargs = []; res = None }
+  in
+    gen_structs oc make
+
+(* Random generation *)
+
+let pick arr =
+  arr.(Random.int (Array.length arr))
+
+let big_ty = [| Int32; Int64; Float32; Float64; String |]
+
+let vararg_ty =  [| Int32; Int64; Float64; String |]
+
+let random_funsig vararg =
+  let res = if Random.bool() then Some (pick all_ty) else None in
+  let numargs = Random.int 12 in
+  let args = List.init numargs (fun _ -> pick big_ty) in
+  let numvarargs = 
+    if vararg && numargs > 0 && is_vararg_type (List.nth args (numargs - 1))
+    then 1 + Random.int 12
+    else 0 in
+  let varargs = List.init numvarargs (fun _ -> pick vararg_ty) in
+  { args; varargs; res }
+
+let header =
+{|#include <stdarg.h>
+#include <stdio.h>
+#include <string.h>
+#include <unistd.h>
+|}
+
+let checking_code = {|
+extern int failed;
+
+static void failure(const char * assertion, const char * file,
+                    int line, const char * fn)
+{
+  fprintf(stderr, "%s:%d:%s: assertion %s failed\n", file, line, fn, assertion);
+  failed = 1;
+}
+
+#define check(expr) ((expr) ? (void)0 : failure(#expr,__FILE__,__LINE__,__func__))
+|}
+
+let output_prefix = ref "abifuzz"
+let gen_vararg = ref false
+let gen_struct = ref false
+let num_random = ref 0
+
+let _ =
+  Arg.parse [
+     "-plain", Arg.Unit (fun () -> gen_vararg := false; gen_struct := false),
+       " generate fixed-argument functions without structs";
+     "-vararg", Arg.Set gen_vararg,
+       " generate variable-argument functions";
+     "-structs", Arg.Set gen_struct,
+       " generate functions that exchange structs";
+     "-o", Arg.String (fun s -> output_prefix := s),
+       " <prefix> produce <prefix>.h, <prefix>def.c and <prefix>use.c files";
+     "-rnd", Arg.Int (fun n -> num_random := n),
+       " <num> produce <num> extra functions with random signatures";
+     "-seed", Arg.Int Random.init,
+       " <seed> use the given seed for randomization"
+  ]
+  (fun s -> raise (Arg.Bad ("don't know what to do with " ^ s)))
+  "Usage: gencalls [options]\n\nOptions are:";
+  let oc0 = open_out (!output_prefix ^ "_decl.h")
+  and oc1 = open_out (!output_prefix ^ "_def.c")
+  and oc2 = open_out (!output_prefix ^ "_use.c") in
+  fprintf oc0 "%s\n%s\n" header checking_code;
+  fprintf oc1 "%s#include \"%s_decl.h\"\n\n" header !output_prefix;
+  fprintf oc2 "%s#include \"%s_decl.h\"\n\nint failed = 0;\n\n"
+              header !output_prefix;
+  let cont = generate_one_test oc0 oc1 oc2 in
+  if !gen_vararg then gen_vararg_sigs cont
+  else if !gen_struct then gen_struct_sigs oc0 cont
+  else gen_fixed_sigs cont;
+  for i = 1 to !num_random do
+    cont (random_funsig !gen_vararg)
+  done;
+  call_all_test oc2;
+  close_out oc0; close_out oc1; close_out oc2
diff --git a/test/clightgen/annotations.c b/test/clightgen/annotations.c
index e91c7fbc..993fa7d0 100644
--- a/test/clightgen/annotations.c
+++ b/test/clightgen/annotations.c
@@ -1,6 +1,6 @@
 int f(int x, long y)
 {
-#if !defined(SYSTEM_macosx) && !defined(SYSTEM_cygwin)
+#if !defined(SYSTEM_macos) && !defined(SYSTEM_cygwin)
   __builtin_ais_annot("x is %e1, y is %e2", x, y);
 #endif
   __builtin_annot("x is %1, y is %2", x, y);
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 56d90469..f74e1441 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -17,7 +17,7 @@ TESTS?=int32 int64 floats floats-basics floats-lit \
   volatile1 volatile2 volatile3 volatile4 \
   funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \
   sizeof1 sizeof2 binops bool for1 for2 switch switch2 compound \
-  decl1 interop1 bitfields9 ptrs3 \
+  decl1 bitfields9 ptrs3 \
   parsing krfun ifconv
 
 # Can run, but only in compiled mode, and have reference output in Results
@@ -54,13 +54,6 @@ all: $(TESTS:%=%.compcert) $(TESTS_COMP:%=%.compcert) $(TESTS_DIFF:%=%.compcert)
 
 all_s: $(TESTS:%=%.s) $(TESTS_COMP:%=%.s) $(TESTS_DIFF:%=%.s) $(EXTRAS:%=%.s)
 
-interop1.compcert: interop1.c
-	$(CC) -DCC_SIDE -c -o interop1n.o interop1.c
-	$(CCOMP) $(CCOMPFLAGS) -DCOMPCERT_SIDE -o interop1.compcert interop1.c interop1n.o $(LIBS)
-
-interop1.s: interop1.c
-	$(CCOMP) $(CCOMPFLAGS) -S interop1.c
-
 %.compcert: %.c
 	$(CCOMP) $(CCOMPFLAGS) -o $*.compcert $*.c $(LIBS)
 
diff --git a/test/regression/Results/interop1 b/test/regression/Results/interop1
deleted file mode 100644
index 6e32c1cb..00000000
--- a/test/regression/Results/interop1
+++ /dev/null
@@ -1,98 +0,0 @@
---- CompCert calling native:
-si8u: 177
-si8s: -79
-si16u: 64305
-si16s: -1231
-s1: { a = 'a' }
-s2: { a = 'a', b = 'b' }
-s3: { a = 'a', b = 'b', c = ' c' }
-s4: { a = 'a', b = 'b', c = ' c', d = 'd' }
-s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
-s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
-s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
-s8: "Hello world!"
-t1: { a = 123 }
-t2: { a = 123, b = 456 }
-t3: { a = 123, b = 456, c = 789 }
-t4: { a = 123, b = 456, c = 789, d = -111 }
-t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
-u1: { a = 12 }
-u2: { a = 12, b = -34 }
-u3: { a = 12, b = 34, c = -56 }
-u4: { a = 12, b = 34, c = 56, d = -78 }
-u5: { a = 1234, b = 'u' }
-u6: { a = 55555, b = 666 }
-u7: { a = -10001, b = -789, c = 'z' }
-u8: { a = 'x', b = 12345 }
-after ms4, x = { 's', 'a', 'm', 'e' }
-after mu4, x = { a = { 11, 22, 33, 44 } }
-rs1: { a = 'a' }
-rs2: { a = 'a', b = 'b' }
-rs3: { a = 'a', b = 'b', c = ' c' }
-rs4: { a = 'a', b = 'b', c = ' c', d = 'd' }
-rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
-rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
-rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
-rs8: "Hello world!"
-rt1: { a = 123 }
-rt2: { a = 123, b = 456 }
-rt3: { a = 123, b = 456, c = 789 }
-rt4: { a = 123, b = 456, c = 789, d = -111 }
-rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
-ru1: { a = 12 }
-ru2: { a = 12, b = -34 }
-ru3: { a = 12, b = 34, c = -56 }
-ru4: { a = 12, b = 34, c = 56, d = -78 }
-ru5: { a = 1234, b = 'u' }
-ru6: { a = 55555, b = 666 }
-ru7: { a = -10001, b = -789, c = 'z' }
-ru8: { a = 'x', b = 12345 }
---- native calling CompCert:
-si8u: 177
-si8s: -79
-si16u: 64305
-si16s: -1231
-s1: { a = 'a' }
-s2: { a = 'a', b = 'b' }
-s3: { a = 'a', b = 'b', c = ' c' }
-s4: { a = 'a', b = 'b', c = ' c', d = 'd' }
-s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
-s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
-s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
-s8: "Hello world!"
-t1: { a = 123 }
-t2: { a = 123, b = 456 }
-t3: { a = 123, b = 456, c = 789 }
-t4: { a = 123, b = 456, c = 789, d = -111 }
-t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
-u1: { a = 12 }
-u2: { a = 12, b = -34 }
-u3: { a = 12, b = 34, c = -56 }
-u4: { a = 12, b = 34, c = 56, d = -78 }
-u5: { a = 1234, b = 'u' }
-u6: { a = 55555, b = 666 }
-u7: { a = -10001, b = -789, c = 'z' }
-u8: { a = 'x', b = 12345 }
-after ms4, x = { 's', 'a', 'm', 'e' }
-after mu4, x = { a = { 11, 22, 33, 44 } }
-rs1: { a = 'a' }
-rs2: { a = 'a', b = 'b' }
-rs3: { a = 'a', b = 'b', c = ' c' }
-rs4: { a = 'a', b = 'b', c = ' c', d = 'd' }
-rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
-rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
-rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
-rs8: "Hello world!"
-rt1: { a = 123 }
-rt2: { a = 123, b = 456 }
-rt3: { a = 123, b = 456, c = 789 }
-rt4: { a = 123, b = 456, c = 789, d = -111 }
-rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
-ru1: { a = 12 }
-ru2: { a = 12, b = -34 }
-ru3: { a = 12, b = 34, c = -56 }
-ru4: { a = 12, b = 34, c = 56, d = -78 }
-ru5: { a = 1234, b = 'u' }
-ru6: { a = 55555, b = 666 }
-ru7: { a = -10001, b = -789, c = 'z' }
-ru8: { a = 'x', b = 12345 }
diff --git a/test/regression/Results/varargs2 b/test/regression/Results/varargs2
index 96ee9d63..9e77da1b 100644
--- a/test/regression/Results/varargs2
+++ b/test/regression/Results/varargs2
@@ -10,4 +10,5 @@ Twice: -1 1.23
 With va_copy: -1 1.23
 With va_copy: -1 1.23
 With extra args: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746
+With extra FP args: 3.141592654 & 2.718281746 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 42
 va_list compatibility: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746
diff --git a/test/regression/interop1.c b/test/regression/interop1.c
deleted file mode 100644
index 6836b89e..00000000
--- a/test/regression/interop1.c
+++ /dev/null
@@ -1,301 +0,0 @@
-#if defined(COMPCERT_SIDE)
-#define US(x) compcert_##x
-#define THEM(x) native_##x
-#elif defined(CC_SIDE)
-#define US(x) native_##x
-#define THEM(x) compcert_##x
-#else
-#define US(x) x
-#define THEM(x) x
-#endif
-
-#include <stdio.h>
-
-/* Alignment 1 */
-
-struct S1 { char a; };
-static struct S1 init_S1 = { 'a' };
-#define print_S1(x) printf("{ a = '%c' }\n", x.a)
-
-struct S2 { char a, b; };
-static struct S2 init_S2 = { 'a', 'b' };
-#define print_S2(x) printf("{ a = '%c', b = '%c' }\n", x.a, x.b)
-
-struct S3 { char a, b, c; };
-static struct S3 init_S3 = { 'a', 'b', 'c' };
-#define print_S3(x) \
-   printf("{ a = '%c', b = '%c', c = ' %c' }\n", x.a, x.b, x.c)
-
-struct S4 { char a, b, c, d; };
-static struct S4 init_S4 = { 'a', 'b', 'c', 'd' };
-#define print_S4(x) \
-   printf("{ a = '%c', b = '%c', c = ' %c', d = '%c' }\n", \
-          x.a, x.b, x.c, x.d);
-
-struct S5 { char a, b, c, d, e; };
-static struct S5 init_S5 = { 'a', 'b', 'c', 'd', 'e' };
-#define print_S5(x) \
-  printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c' }\n", \
-         x.a, x.b, x.c, x.d, x.e)
-
-struct S6 { char a, b, c, d, e, f; };
-static struct S6 init_S6 = { 'a', 'b', 'c', 'd', 'e', 'f' };
-#define print_S6(x) \
-  printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c', f = '%c' }\n", \
-         x.a, x.b, x.c, x.d, x.e, x.f)
-
-struct S7 { char a, b, c, d, e, f, g; };
-static struct S7 init_S7 = { 'a', 'b', 'c', 'd', 'e', 'f', 'g' };
-#define print_S7(x) \
-  printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c', f = '%c', g = '%c' }\n", \
-         x.a, x.b, x.c, x.d, x.e, x.f, x.g)
-
-struct S8 { char a[32]; };
-static struct S8 init_S8 = { "Hello world!" };
-/* Do not use printf("%s") to avoid undefined behavior in the
-   reference interpreter */
-#define print_S8(x) \
-  { char * p;       \
-    printf("\"");   \
-    for (p = x.a; *p != 0; p++) printf("%c", *p); \
-    printf("\"\n");   \
-  }
-
-/* Alignment 2 */
-
-struct T1 { short a; };
-static struct T1 init_T1 = { 123 };
-#define print_T1(x) printf("{ a = %d }\n", x.a)
-
-struct T2 { short a, b; };
-static struct T2 init_T2 = { 123, 456 };
-#define print_T2(x) printf("{ a = %d, b = %d }\n", x.a, x.b)
-
-struct T3 { short a, b, c; };
-static struct T3 init_T3 = { 123, 456, 789 };
-#define print_T3(x) printf("{ a = %d, b = %d, c = %d }\n", x.a, x.b, x.c)
-
-struct T4 { short a, b, c, d; };
-static struct T4 init_T4 = { 123, 456, 789, -111 };
-#define print_T4(x) \
-  printf("{ a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d)
-
-struct T5 { short a, b, c, d; char e; };
-static struct T5 init_T5 = { 123, 456, 789, -999, 'x' };
-#define print_T5(x) \
-  printf("{ a = %d, b = %d, c = %d, d = %d, e = '%c' }\n", \
-         x.a, x.b, x.c, x.d, x.e)
-
-/* Alignment >= 4 */
-
-struct U1 { int a; };
-static struct U1 init_U1 = { 12 };
-#define print_U1(x) printf("{ a = %d }\n", x.a)
-
-struct U2 { int a, b; };
-static struct U2 init_U2 = { 12, -34 };
-#define print_U2(x) printf("{ a = %d, b = %d }\n", x.a, x.b)
-
-struct U3 { int a, b, c; };
-static struct U3 init_U3 = { 12, 34, -56};
-#define print_U3(x) printf("{ a = %d, b = %d, c = %d }\n", x.a, x.b, x.c)
-
-struct U4 { int a, b, c, d; };
-static struct U4 init_U4 = { 12, 34, 56, -78 };
-#define print_U4(x) \
-  printf("{ a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d)
-
-struct U5 { int a; char b; };
-static struct U5 init_U5 = { 1234, 'u' };
-#define print_U5(x) \
-  printf("{ a = %d, b = '%c' }\n", x.a, x.b)
-
-struct U6 { int a; short b; };
-static struct U6 init_U6 = { 55555, 666 };
-#define print_U6(x) \
-  printf("{ a = %d, b = %d }\n", x.a, x.b)
-
-struct U7 { int a; short b; char c; };
-static struct U7 init_U7 = { -10001, -789, 'z' };
-#define print_U7(x) \
-  printf("{ a = %d, b = %d, c = '%c' }\n", x.a, x.b, x.c)
-
-struct U8 { char a; int b; };
-static struct U8 init_U8 = { 'x', 12345 };
-#define print_U8(x) \
-  printf("{ a = '%c', b = %d }\n", x.a, x.b)
-
-/* Struct passing */
-
-#define PRINT(name,ty,print) \
-extern void THEM(name) (struct ty x); \
-void US(name) (struct ty x) { print(x); }
-
-PRINT(s1,S1,print_S1)
-PRINT(s2,S2,print_S2)
-PRINT(s3,S3,print_S3)
-PRINT(s4,S4,print_S4)
-PRINT(s5,S5,print_S5)
-PRINT(s6,S6,print_S6)
-PRINT(s7,S7,print_S7)
-PRINT(s8,S8,print_S8)
-PRINT(t1,T1,print_T1)
-PRINT(t2,T2,print_T2)
-PRINT(t3,T3,print_T3)
-PRINT(t4,T4,print_T4)
-PRINT(t5,T5,print_T5)
-PRINT(u1,U1,print_U1)
-PRINT(u2,U2,print_U2)
-PRINT(u3,U3,print_U3)
-PRINT(u4,U4,print_U4)
-PRINT(u5,U5,print_U5)
-PRINT(u6,U6,print_U6)
-PRINT(u7,U7,print_U7)
-PRINT(u8,U8,print_U8)
-
-/* Struct passing with modification in the callee */
-
-extern void THEM (ms4) (struct S4 x);
-void US (ms4) (struct S4 x)
-{
-  x.a += 1; x.d -= 1;
-}
-
-extern void THEM (mu4) (struct U4 x);
-void US (mu4) (struct U4 x)
-{
-  x.a = 1; x.b = 2;
-}
-
-/* Struct return */
-
-#define RETURN(name,ty,init) \
-extern struct ty THEM(name)(void); \
-struct ty US(name)(void) { return init; }
-
-RETURN(rs1,S1,init_S1)
-RETURN(rs2,S2,init_S2)
-RETURN(rs3,S3,init_S3)
-RETURN(rs4,S4,init_S4)
-RETURN(rs5,S5,init_S5)
-RETURN(rs6,S6,init_S6)
-RETURN(rs7,S7,init_S7)
-RETURN(rs8,S8,init_S8)
-RETURN(rt1,T1,init_T1)
-RETURN(rt2,T2,init_T2)
-RETURN(rt3,T3,init_T3)
-RETURN(rt4,T4,init_T4)
-RETURN(rt5,T5,init_T5)
-RETURN(ru1,U1,init_U1)
-RETURN(ru2,U2,init_U2)
-RETURN(ru3,U3,init_U3)
-RETURN(ru4,U4,init_U4)
-RETURN(ru5,U5,init_U5)
-RETURN(ru6,U6,init_U6)
-RETURN(ru7,U7,init_U7)
-RETURN(ru8,U8,init_U8)
-
-/* Returning small integers */
-
-#define SMALLINT(name,ty) \
-extern ty THEM(name)(int); \
-ty US(name)(int x) { return x * x; }
-
-SMALLINT(si8u, unsigned char)
-SMALLINT(si8s, signed char)
-SMALLINT(si16u, unsigned short)
-SMALLINT(si16s, signed short)
-
-/* Test function, calling the functions compiled by the other compiler */
-
-#define CALLPRINT(name,ty,init) \
-  printf(#name": "); THEM(name)(init);
-
-#define CALLRETURN(name,ty,print) \
-  { struct ty x = THEM(name)(); \
-    printf(#name": "); print(x); }
-
-extern void THEM(test) (void);
-void US(test) (void)
-{
-  printf("si8u: %d\n", THEM(si8u)(12345));
-  printf("si8s: %d\n", THEM(si8s)(12345));
-  printf("si16u: %d\n", THEM(si16u)(1234567));
-  printf("si16s: %d\n", THEM(si16s)(1234567));
-  CALLPRINT(s1,S1,init_S1)
-  CALLPRINT(s2,S2,init_S2)
-  CALLPRINT(s3,S3,init_S3)
-  CALLPRINT(s4,S4,init_S4)
-  CALLPRINT(s5,S5,init_S5)
-  CALLPRINT(s6,S6,init_S6)
-  CALLPRINT(s7,S7,init_S7)
-  CALLPRINT(s8,S8,init_S8)
-  CALLPRINT(t1,T1,init_T1)
-  CALLPRINT(t2,T2,init_T2)
-  CALLPRINT(t3,T3,init_T3)
-  CALLPRINT(t4,T4,init_T4)
-  CALLPRINT(t5,T5,init_T5)
-  CALLPRINT(u1,U1,init_U1)
-  CALLPRINT(u2,U2,init_U2)
-  CALLPRINT(u3,U3,init_U3)
-  CALLPRINT(u4,U4,init_U4)
-  CALLPRINT(u5,U5,init_U5)
-  CALLPRINT(u6,U6,init_U6)
-  CALLPRINT(u7,U7,init_U7)
-  CALLPRINT(u8,U8,init_U8)
-
-  { struct S4 x = { 's', 'a', 'm', 'e' };
-    THEM(ms4)(x);
-    printf("after ms4, x = { '%c', '%c', '%c', '%c' }\n", x.a, x.b, x.c, x.d); }
-  { struct U4 x = { 11, 22, 33, 44 };
-    THEM(mu4)(x);
-    printf("after mu4, x = { a = { %d, %d, %d, %d } }\n", x.a, x.b, x.c, x.d); }
-
-  CALLRETURN(rs1,S1,print_S1)
-  CALLRETURN(rs2,S2,print_S2)
-  CALLRETURN(rs3,S3,print_S3)
-  CALLRETURN(rs4,S4,print_S4)
-  CALLRETURN(rs5,S5,print_S5)
-  CALLRETURN(rs6,S6,print_S6)
-  CALLRETURN(rs7,S7,print_S7)
-  CALLRETURN(rs8,S8,print_S8)
-  CALLRETURN(rt1,T1,print_T1)
-  CALLRETURN(rt2,T2,print_T2)
-  CALLRETURN(rt3,T3,print_T3)
-  CALLRETURN(rt4,T4,print_T4)
-  CALLRETURN(rt5,T5,print_T5)
-  CALLRETURN(ru1,U1,print_U1)
-  CALLRETURN(ru2,U2,print_U2)
-  CALLRETURN(ru3,U3,print_U3)
-  CALLRETURN(ru4,U4,print_U4)
-  CALLRETURN(ru5,U5,print_U5)
-  CALLRETURN(ru6,U6,print_U6)
-  CALLRETURN(ru7,U7,print_U7)
-  CALLRETURN(ru8,U8,print_U8)
-}
-
-#if defined(COMPCERT_SIDE)
-
-int main()
-{
-  printf("--- CompCert calling native:\n");
-  compcert_test();
-  printf("--- native calling CompCert:\n");
-  native_test();
-  return 0;
-}
-
-#elif !defined(CC_SIDE)
-
-int main()
-{
-  printf("--- CompCert calling native:\n");
-  test();
-  printf("--- native calling CompCert:\n");
-  test();
-  return 0;
-}
-
-#endif
-
-
diff --git a/test/regression/interop1.cond b/test/regression/interop1.cond
deleted file mode 100644
index 77904189..00000000
--- a/test/regression/interop1.cond
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/sh
-arch=`sed -n -e 's/^ARCH=//p' ../../Makefile.config`
-model=`sed -n -e 's/^MODEL=//p' ../../Makefile.config`
-system=`sed -n -e 's/^SYSTEM=//p' ../../Makefile.config`
-
-case "$arch,$model,$system" in
-  *,*,cygwin)  exit $SKIP;;
-  x86,32sse2,*|arm,*,*|powerpc,*,*)  exit $RUN;;
-  *) exit $SKIP;;
-esac
diff --git a/test/regression/varargs2.c b/test/regression/varargs2.c
index 3e785a63..e3492ead 100644
--- a/test/regression/varargs2.c
+++ b/test/regression/varargs2.c
@@ -104,6 +104,17 @@ void miniprintf_extra(int i1, int i2, int i3, int i4,
   va_end(va);
 }
 
+/* Add a few dummy FP arguments to test passing of variadic FP arguments
+   in integer registers (mostly relevant for RISC-V) */
+
+void miniprintf_float(double f1, double f2, const char * fmt, ...)
+{
+  va_list va;
+  va_start(va, fmt);
+  minivprintf(fmt, va);
+  va_end(va);
+}
+
 /* Test va_list compatibility with the C library */
 
 void printf_compat(const char * fmt, ...)
@@ -157,6 +168,11 @@ int main()
                    123456789012345LL,
                    3.141592654,
                    2.71828182);
+  miniprintf_float(0.0, 0.5,
+                   "With extra FP args: %e & %f & %e & %e & %e & %e & %e & %e & %e & %e & %d\n",
+                   3.141592654,
+                   2.71828182,
+                   1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 42);
   printf_compat("va_list compatibility: %c & %s & %d & %lld & %.10g & %.10g\n",
                 'x',
                 "Hello, world!",