From 801ed5afd5e5f97818e73c06102510bfcf7170c5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 27 Apr 2015 17:02:07 +0200 Subject: Added the first version of the sdump export to json. --- driver/Driver.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index d225ec4f..5a89d4d4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -155,6 +155,15 @@ let dump_asm asm destfile = output_value oc C2C.decl_atom; close_out oc +let jdump_magic_number = "CompCertJDUMP" ^ Configuration.version + +let dump_jasm asm destfile = + let oc = open_out_bin destfile in + fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a,\n\"C Declaration\":%t}" + jdump_magic_number AsmToJSON.p_program asm C2CToJSON.print_decl_atom; + close_out oc + + (* From CompCert C AST to asm *) let compile_c_ast sourcename csyntax ofile debug = @@ -176,9 +185,12 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> print_error stderr msg; exit 2 in - (* Dump Asm in binary format *) + (* Dump Asm in binary and JSON format *) if !option_sdump then - dump_asm asm (output_filename sourcename ".c" ".sdump"); + begin + dump_asm asm (output_filename sourcename ".c" ".sdump"); + dump_jasm asm (output_filename sourcename ".c" ".json") + end; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; -- cgit From 4705c24a336d831dd5afb02288fda17c0093c438 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 6 May 2015 15:10:39 +0200 Subject: Moved the information needed from the atoms to the ASM printer and removed unused information from the json dump. --- driver/Driver.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 5a89d4d4..04dec9db 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -159,8 +159,8 @@ let jdump_magic_number = "CompCertJDUMP" ^ Configuration.version let dump_jasm asm destfile = let oc = open_out_bin destfile in - fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a,\n\"C Declaration\":%t}" - jdump_magic_number AsmToJSON.p_program asm C2CToJSON.print_decl_atom; + fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a}" + jdump_magic_number AsmToJSON.p_program asm; close_out oc -- cgit From 50ed2827867238a98f2036f799d4d6f354a2581c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 19 May 2015 18:07:08 +0200 Subject: Added flag for the renaming of static functions. --- driver/Driver.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 04dec9db..90badb85 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -435,6 +435,7 @@ Language support options (use -fno- to turn off -f) : -fnone Turn off all language support options above Debugging options: -g Generate debugging information + -frename-static Rename static functions and declarations Optimization options: (use -fno- to turn off -f) -O Optimize the compiled code [on by default] -O0 Do not optimize the compiled code @@ -528,6 +529,7 @@ let cmdline_actions = Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true); + Exact "-frename-static", Self (fun s -> option_rename_static:= true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); -- cgit From b59b2b182a6832e1b6ebf3cf7ba4fd1943843b74 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 1 Jul 2015 17:25:44 +0200 Subject: Removed the version from the compcert.ini file and add it again in a separate file. --- driver/Driver.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 805d5405..402bdb65 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -145,7 +145,7 @@ let parse_c_file sourcename ifile = (* Dump Asm code in binary format for the validator *) -let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version +let sdump_magic_number = "CompCertSDUMP" ^ Version.version let dump_asm asm destfile = let oc = open_out_bin destfile in @@ -387,7 +387,10 @@ let explode_comma_option s = | hd :: tl -> tl let version_string = - "The CompCert C verified compiler, version "^ Configuration.version ^ "\n" + if Version.buildnr <> "" && Version.tag <> "" then + sprintf "The CompCert verified compiler, %s,%s,%s\n" Version.version Version.buildnr Version.tag + else + "The CompCert C verified compiler, version "^ Version.version ^ "\n" let usage_string = version_string ^ -- cgit From fae1b5c4c2c38133da8caa87ee66abb411ca4af4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 1 Jul 2015 17:59:05 +0200 Subject: Added Build, Tag, etc in version string and driver/Version.ml should be ignored --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 402bdb65..30315fd0 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -388,7 +388,7 @@ let explode_comma_option s = let version_string = if Version.buildnr <> "" && Version.tag <> "" then - sprintf "The CompCert verified compiler, %s,%s,%s\n" Version.version Version.buildnr Version.tag + sprintf "The CompCert verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -- cgit From a28cb16aeb266fd41c0ce2ddbe0a0d8d2cbf20de Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 7 Jul 2015 17:50:55 +0200 Subject: Diab defines w_char to be unsigned short. --- driver/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 1b58fe61..1dce08ac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -661,7 +661,9 @@ let _ = Printexc.record_backtrace true; Machine.config := begin match Configuration.arch with - | "powerpc" -> Machine.ppc_32_bigendian + | "powerpc" -> if Configuration.system = "linux" + then Machine.ppc_32_bigendian + else Machine.ppc_32_diab_bigendian | "arm" -> Machine.arm_littleendian | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx -- cgit