From 8c2e9c25bab0118a71fe27bbe539ac6464effde2 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 23 Apr 2015 11:56:13 +0200
Subject: Update clightgen to the new annotations and the new inline asm.

---
 exportclight/Clightgen.ml    |  2 +-
 exportclight/ExportClight.ml | 33 +++++++++------------------------
 2 files changed, 10 insertions(+), 25 deletions(-)

(limited to 'exportclight')

diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index c1009b4f..a1dba2d9 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -112,7 +112,7 @@ let parse_c_file sourcename ifile =
   in
   (* Parsing and production of a simplified C AST *)
   let ast =
-    match Parse.preprocessed_file simplifs sourcename ifile with
+    match fst (Parse.preprocessed_file simplifs sourcename ifile) with
     | None -> exit 2
     | Some p -> p in
   (* Save C AST if requested *)
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 51dd0757..397d04b1 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -233,15 +233,7 @@ let signatur p sg =
      (print_option asttype) sg.sig_res 
      callconv sg.sig_cc
 
-let assertions = ref ([]: (ident * annot_arg list) list)
-
-let annot_arg p = function
-  | AA_arg ty ->
-      fprintf p "AA_arg %a" asttype ty
-  | AA_int n ->
-      fprintf p "AA_int %a" coqint n
-  | AA_float n ->
-      fprintf p "AA_float %a" coqfloat n
+let assertions = ref ([]: (ident * typ list) list)
 
 let external_function p = function
   | EF_external(name, sg) ->
@@ -262,12 +254,15 @@ let external_function p = function
       fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
   | EF_annot(text, targs) -> 
       assertions := (text, targs) :: !assertions;
-      fprintf p "(EF_annot %ld%%positive %a)" (P.to_int32 text) (print_list annot_arg) targs
+      fprintf p "(EF_annot %ld%%positive %a)" (P.to_int32 text) (print_list asttype) targs
   | EF_annot_val(text, targ) ->
-      assertions := (text, [AA_arg targ]) :: !assertions;
+      assertions := (text, [targ]) :: !assertions;
       fprintf p "(EF_annot_val %ld%%positive %a)" (P.to_int32 text) asttype targ
-  | EF_inline_asm(text) ->
-      fprintf p "(EF_inline_asm %ld%%positive)" (P.to_int32 text)
+  | EF_inline_asm(text, sg, clob) ->
+      fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]"
+              (P.to_int32 text)
+              signatur sg
+              (print_list ident) clob
 
 (* Expressions *)
 
@@ -461,19 +456,9 @@ let print_assertion p (txt, targs) =
     frags;
   fprintf p "  | %ld%%positive, " (P.to_int32 txt);
   list_iteri
-    (fun i targ ->
-      match targ with
-      | AA_arg _ -> fprintf p "_x%d :: " (i + 1)
-      | _ -> ())
+    (fun i targ -> fprintf p "_x%d :: " (i + 1))
     targs;
   fprintf p "nil =>@ ";
-  list_iteri
-    (fun i targ ->
-      match targ with
-      | AA_arg _ -> ()
-      | AA_int n ->  fprintf p "    let _x%d := %a in@ " (i + 1) coqint n
-      | AA_float n ->  fprintf p "    let _x%d := %a in@ " (i + 1) coqfloat n)
-    targs;
   fprintf p "    ";
   List.iter
     (function
-- 
cgit