PowerPC/EABI port: preliminary support for #pragma section and

  #pragma use_section.
Some clean-ups in Cil2Csyntax.
Separate mach-dep parts of extraction/extraction.v into
   <arch>/extractionMachdep.v


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 19 insertions, 6 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 08e4a536..c6f6e8fe 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,6 +17,7 @@ let linker_options = ref ([]: string list)
 let exe_name = ref "a.out"
 let option_flonglong = ref false
 let option_fmadd = ref false
+let option_dcil = ref false
 let option_dclight = ref false
 let option_dasm = ref false
 let option_E = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 30d4a6cc..b8186804 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -118,21 +118,26 @@ let compile_c_file sourcename ifile ofile =
   cil.Cil.fileName <- sourcename;
   (* Cleanup in the CIL.file *)
   Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
+  (* Save CIL output if requested *)
+  if !option_dcil then begin
+    let ofile = Filename.chop_suffix sourcename ".c" ^ ".cil.c" in
+    let oc = open_out ofile in
+    Cil.dumpFile Cil.defaultCilPrinter oc ofile cil;
+    close_out oc
+  end;
   (* Conversion to Csyntax *)
   let csyntax =
     try
       Cil2CsyntaxTranslator.convertFile cil
     with
-    | Cil2CsyntaxTranslator.Unsupported msg ->
+    | Cil2Csyntax.Error msg ->
         eprintf "%s\n" msg;
         exit 2
-    | Cil2CsyntaxTranslator.Internal_error msg ->
-        eprintf "%s\nPlease report it.\n" msg;
-        exit 2 in
+  in
   (* Save Csyntax if requested *)
   if !option_dclight then begin
-    let targetname = Filename.chop_suffix sourcename ".c" in
-    let oc = open_out (targetname ^ ".light.c") in
+    let ofile = Filename.chop_suffix sourcename ".c" ^ ".light.c" in
+    let oc = open_out ofile in
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
   end;
@@ -264,6 +269,7 @@ Preprocessing options:
 Compilation options:
   -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
   -fmadd         Use fused multiply-add and multiply-sub instructions
+  -dcil          Save CIL-processed source in <file>.cil.c
   -dclight       Save generated Clight in <file>.light.c
   -dasm          Save generated assembly in <file>.s
 Linking options:
@@ -303,6 +309,10 @@ let rec parse_cmdline i =
       option_fmadd := true;
       parse_cmdline (i + 1)
     end else
+    if s = "-dcil" then begin
+      option_dcil := true;
+      parse_cmdline (i + 1)
+    end else
     if s = "-dclight" then begin
       option_dclight := true;
       parse_cmdline (i + 1)
@@ -348,6 +358,8 @@ let rec parse_cmdline i =
   end
 
 let _ =
+  Cil.initCIL();
+  CPragmas.initialize();
   parse_cmdline 1;
   if not (!option_c || !option_S || !option_E) then begin
     linker !exe_name !linker_options