aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--driver/Driver.ml68
-rw-r--r--driver/Optionsprinter.ml143
-rw-r--r--lib/Json.ml42
-rw-r--r--powerpc/AsmToJSON.ml153
4 files changed, 299 insertions, 107 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 78d141c1..81f28309 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -20,6 +20,8 @@ open Timing
let stdlib_path = ref Configuration.stdlib_path
+let dump_options = ref false
+
(* Optional sdump suffix *)
let sdump_suffix = ref ".json"
@@ -282,37 +284,37 @@ let process_c_file sourcename =
preprocess sourcename (output_filename_default "-");
""
end else begin
- let preproname = if !option_dprepro then
+ let preproname = if !option_dprepro then
output_filename sourcename ".c" ".i"
else
Filename.temp_file "compcert" ".i" in
preprocess sourcename preproname;
- if !option_interp then begin
- Machine.config := Machine.compcert_interpreter !Machine.config;
- let csyntax,_ = parse_c_file sourcename preproname in
- if not !option_dprepro then
- safe_remove preproname;
- Interp.execute csyntax;
- ""
- end else if !option_S then begin
- compile_c_file sourcename preproname
- (output_filename ~final:true sourcename ".c" ".s");
- if not !option_dprepro then
- safe_remove preproname;
- ""
- end else begin
- let asmname =
- if !option_dasm
- then output_filename sourcename ".c" ".s"
- else Filename.temp_file "compcert" ".s" in
- compile_c_file sourcename preproname asmname;
- if not !option_dprepro then
- safe_remove preproname;
- let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
- assemble asmname objname;
- if not !option_dasm then safe_remove asmname;
- objname
- end
+ let name =
+ if !option_interp then begin
+ Machine.config := Machine.compcert_interpreter !Machine.config;
+ let csyntax,_ = parse_c_file sourcename preproname in
+ Interp.execute csyntax;
+ ""
+ end else if !option_S then begin
+ compile_c_file sourcename preproname
+ (output_filename ~final:true sourcename ".c" ".s");
+ ""
+ end else begin
+ let asmname =
+ if !option_dasm
+ then output_filename sourcename ".c" ".s"
+ else Filename.temp_file "compcert" ".s" in
+ compile_c_file sourcename preproname asmname;
+ let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
+ assemble asmname objname;
+ if not !option_dasm then safe_remove asmname;
+ objname
+ end in
+ if not !option_dprepro then
+ safe_remove preproname;
+ if !dump_options then
+ Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path;
+ name
end
(* Processing of a .i / .p file (preprocessed C) *)
@@ -324,7 +326,9 @@ let process_i_file sourcename =
""
end else if !option_S then begin
compile_c_file sourcename sourcename
- (output_filename ~final:true sourcename ".c" ".s");
+ (output_filename ~final:true sourcename ".c" ".s");
+ if !dump_options then
+ Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path;
""
end else begin
let asmname =
@@ -335,6 +339,8 @@ let process_i_file sourcename =
let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
assemble asmname objname;
if not !option_dasm then safe_remove asmname;
+ if !dump_options then
+ Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path;
objname
end
@@ -354,6 +360,8 @@ let process_cminor_file sourcename =
let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in
assemble asmname objname;
if not !option_dasm then safe_remove asmname;
+ if !dump_options then
+ Optionsprinter.print (output_filename sourcename ".cm" ".opt.json") !stdlib_path;
objname
end
@@ -496,6 +504,7 @@ Tracing options:
-dmach Save generated Mach code in <file>.mach
-dasm Save generated assembly in <file>.s
-sdump Save info for post-linking validation in <file>.json
+ -doptions Save the compiler configurations in <file>.opt.json
General options:
-stdlib <dir> Set the path of the Compcert run-time library
-v Print external commands before invoking them
@@ -621,6 +630,7 @@ let cmdline_actions =
Exact "-dasm", Set option_dasm;
Exact "-sdump", Set option_sdump;
Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s);
+ Exact "-doptions", Set dump_options;
(* General options *)
Exact "-v", Set option_v;
Exact "-stdlib", String(fun s -> stdlib_path := s);
@@ -712,6 +722,6 @@ let _ =
let linker_args = time "Total compilation time" perform_actions () in
if (not nolink) && linker_args <> [] then begin
linker (output_filename_default "a.out") linker_args
- end
+ end;
with Sys_error msg ->
eprintf "I/O error: %s.\n" msg; exit 2
diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml
new file mode 100644
index 00000000..f046b40a
--- /dev/null
+++ b/driver/Optionsprinter.ml
@@ -0,0 +1,143 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
+(* is distributed under the terms of the INRIA Non-Commercial *)
+(* License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+open Clflags
+open Json
+open Machine
+open Printf
+
+let print_list oc name l =
+ p_jmember oc name (p_jarray p_jstring) l
+
+let print_clflags oc =
+ fprintf oc "{";
+ print_list oc "prepro_options" !prepro_options;
+ print_list oc "linker_options" !linker_options;
+ print_list oc "assembler_options" !assembler_options;
+ p_jmember oc "flongdouble" p_jbool !option_flongdouble;
+ p_jmember oc "fstruct_passing" p_jbool !option_fstruct_passing;
+ p_jmember oc "fbitfields" p_jbool !option_fbitfields;
+ p_jmember oc "fvarag_calls" p_jbool !option_fvararg_calls;
+ p_jmember oc "funprototyped" p_jbool !option_funprototyped;
+ p_jmember oc "fpacked_structs" p_jbool !option_fpacked_structs;
+ p_jmember oc "ffpu" p_jbool !option_ffpu;
+ p_jmember oc "ffloatconstprop" p_jint !option_ffloatconstprop;
+ p_jmember oc "ftailcalls" p_jbool !option_ftailcalls;
+ p_jmember oc "fconstprop" p_jbool !option_fconstprop;
+ p_jmember oc "fcse" p_jbool !option_fcse;
+ p_jmember oc "fredundance" p_jbool !option_fredundancy;
+ p_jmember oc "falignfunctions" (p_jopt p_jint) !option_falignfunctions;
+ p_jmember oc "falignbranchtargets" p_jint !option_falignbranchtargets;
+ p_jmember oc "faligncondbranchs" p_jint !option_faligncondbranchs;
+ p_jmember oc "finline_asm" p_jbool !option_finline_asm;
+ p_jmember oc "mthumb" p_jbool !option_mthumb;
+ p_jmember oc "Osize" p_jbool !option_Osize;
+ p_jmember oc "dprepro" p_jbool !option_dprepro;
+ p_jmember oc "dparse" p_jbool !option_dparse;
+ p_jmember oc "dcmedium" p_jbool !option_dcmedium;
+ p_jmember oc "dclight" p_jbool !option_dclight;
+ p_jmember oc "dcminor" p_jbool !option_dcminor;
+ p_jmember oc "drtl" p_jbool !option_drtl;
+ p_jmember oc "dltl" p_jbool !option_dltl;
+ p_jmember oc "dalloctrace" p_jbool !option_dalloctrace;
+ p_jmember oc "dmach" p_jbool !option_dmach;
+ p_jmember oc "dasm" p_jbool !option_dasm;
+ p_jmember oc "sdump" p_jbool !option_sdump;
+ p_jmember oc "g" p_jbool !option_g;
+ p_jmember oc "gdwarf" p_jint !option_gdwarf;
+ p_jmember oc "gdepth" p_jint !option_gdepth;
+ p_jmember oc "o" (p_jopt p_jstring) !option_o;
+ p_jmember oc "E" p_jbool !option_E;
+ p_jmember oc "S" p_jbool !option_S;
+ p_jmember oc "c" p_jbool !option_c;
+ p_jmember oc "v" p_jbool !option_v;
+ p_jmember oc "interp" p_jbool !option_interp;
+ p_jmember oc "small_data" p_jint !option_small_data;
+ p_jmember oc "small_data" p_jint !option_small_const;
+ p_jmember oc "timings" p_jbool !option_timings;
+ p_jmember oc "rename_static" p_jbool !option_rename_static;
+ fprintf oc "\n}"
+
+let print_struct_passing_style oc = function
+ | Configuration.SP_ref_callee -> p_jstring oc "SP_ref_callee"
+ | Configuration.SP_ref_caller -> p_jstring oc "SP_ref_caller"
+ | Configuration.SP_split_args -> p_jstring oc "SP_split_args"
+
+let print_struct_return_style oc = function
+ | Configuration.SR_int1248 -> p_jstring oc "SR_int1248"
+ | Configuration.SR_int1to4 -> p_jstring oc "SR_int1to4"
+ | Configuration.SR_int1to8 -> p_jstring oc "SR_int1to8"
+ | Configuration.SR_ref -> p_jstring oc "SR_ref"
+
+let print_configurations oc lib_path =
+ fprintf oc "{";
+ p_jmember oc "arch" p_jstring Configuration.arch;
+ p_jmember oc "model" p_jstring Configuration.model;
+ p_jmember oc "abi" p_jstring Configuration.abi;
+ p_jmember oc "system" p_jstring Configuration.abi;
+ print_list oc "prepro" Configuration.prepro;
+ print_list oc "asm" Configuration.asm;
+ print_list oc "linker" Configuration.linker;
+ p_jmember oc "asm_supports_cfi" p_jbool Configuration.asm_supports_cfi;
+ p_jmember oc "stdlib_path" p_jstring lib_path;
+ p_jmember oc "has_runtime_lib" p_jbool Configuration.has_runtime_lib;
+ p_jmember oc "has_standard_headers" p_jbool Configuration.has_standard_headers;
+ p_jmember oc "advanced_debug" p_jbool Configuration.advanced_debug;
+ p_jmember oc "struct_passing_style" print_struct_passing_style Configuration.struct_passing_style;
+ p_jmember oc "struct_return_style" print_struct_return_style Configuration.struct_return_style;
+ fprintf oc "\n}"
+
+let print_machine oc =
+ fprintf oc "{";
+ p_jmember oc "name" p_jstring !config.name;
+ p_jmember oc "char_signed" p_jbool !config.char_signed;
+ p_jmember oc "sizeof_ptr" p_jint !config.sizeof_ptr;
+ p_jmember oc "sizeof_short" p_jint !config.sizeof_short;
+ p_jmember oc "sizeof_int" p_jint !config.sizeof_int;
+ p_jmember oc "sizeof_long" p_jint !config.sizeof_long;
+ p_jmember oc "sizeof_longlong" p_jint !config.sizeof_longlong;
+ p_jmember oc "sizeof_float" p_jint !config.sizeof_float;
+ p_jmember oc "sizeof_double" p_jint !config.sizeof_double;
+ p_jmember oc "sizeof_longdouble" p_jint !config.sizeof_longdouble;
+ p_jmember oc "sizeof_void" (p_jopt p_jint) !config.sizeof_void;
+ p_jmember oc "sizeof_fun" (p_jopt p_jint) !config.sizeof_fun;
+ p_jmember oc "sizeof_wchar" p_jint !config.sizeof_wchar;
+ p_jmember oc "wchar_signed" p_jbool !config.wchar_signed;
+ p_jmember oc "sizeof_size_t" p_jint !config.sizeof_size_t;
+ p_jmember oc "sizeof_ptrdiff_t" p_jint !config.sizeof_ptrdiff_t;
+ p_jmember oc "alignof_ptr" p_jint !config.alignof_ptr;
+ p_jmember oc "alignof_short" p_jint !config.alignof_short;
+ p_jmember oc "alignof_int" p_jint !config.alignof_int;
+ p_jmember oc "alignof_long" p_jint !config.alignof_long;
+ p_jmember oc "alignof_longlong" p_jint !config.alignof_longlong;
+ p_jmember oc "alignof_float" p_jint !config.alignof_float;
+ p_jmember oc "alignof_double" p_jint !config.alignof_double;
+ p_jmember oc "alignof_longdouble" p_jint !config.alignof_longdouble;
+ p_jmember oc "alignof_void" (p_jopt p_jint) !config.alignof_void;
+ p_jmember oc "alignof_fun" (p_jopt p_jint) !config.alignof_fun;
+ p_jmember oc "bigendian" p_jbool !config.bigendian;
+ p_jmember oc "bitfields_msb_first" p_jbool !config.bitfields_msb_first;
+ p_jmember oc "supports_unaligned_accesses" p_jbool !config.supports_unaligned_accesses;
+ fprintf oc "\n}"
+
+let print file stdlib =
+ let oc = open_out file in
+ fprintf oc "{";
+ p_jmember oc "Version" p_jstring Version.version;
+ p_jmember oc "Buildnr" p_jstring Version.buildnr;
+ p_jmember oc "Tag" p_jstring Version.tag;
+ p_jmember oc "Cwd" p_jstring (Sys.getcwd ());
+ fprintf oc "%a:%t" p_jstring "Clflags" print_clflags;
+ p_jmember oc "Configurations" print_configurations stdlib;
+ fprintf oc "%a:%t" p_jstring "Machine" print_machine;
+ fprintf oc "}";
+ close_out oc
diff --git a/lib/Json.ml b/lib/Json.ml
new file mode 100644
index 00000000..4aa91e95
--- /dev/null
+++ b/lib/Json.ml
@@ -0,0 +1,42 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
+(* is distributed under the terms of the INRIA Non-Commercial *)
+(* License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+open Printf
+
+(* Simple functions for JSON printing *)
+
+(* Print a string as json string *)
+let p_jstring oc s = fprintf oc "\"%s\"" s
+
+(* Print a list as json array *)
+let p_jarray elem oc l =
+ match l with
+ | [] -> fprintf oc "[]"
+ | hd::tail ->
+ output_string oc "["; elem oc hd;
+ List.iter (fprintf oc ",%a" elem) tail;
+ output_string oc "]"
+
+(* Print a bool as json bool *)
+let p_jbool oc = fprintf oc "%B"
+
+(* Print a int as json int *)
+let p_jint oc = fprintf oc "%d"
+
+(* Print a member *)
+let p_jmember oc name p_mem mem =
+ fprintf oc "\n%a:%a" p_jstring name p_mem mem
+
+(* Print optional value *)
+let p_jopt p_elem oc = function
+ | None -> output_string oc "null"
+ | Some i -> p_elem oc i
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 42ad4f97..4f6a1864 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -17,78 +17,81 @@ open AST
open BinNums
open C2C
open Camlcoq
+open Json
open Printf
open Sections
-let p_jstring oc s = fprintf oc "\"%s\"" s
+let p_ireg oc reg =
+ let num = match reg with
+ | GPR0 -> 0
+ | GPR1 -> 1
+ | GPR2 -> 2
+ | GPR3 -> 3
+ | GPR4 -> 4
+ | GPR5 -> 5
+ | GPR6 -> 6
+ | GPR7 -> 7
+ | GPR8 -> 8
+ | GPR9 -> 9
+ | GPR10 -> 10
+ | GPR11 -> 11
+ | GPR12 -> 12
+ | GPR13 -> 13
+ | GPR14 -> 14
+ | GPR15 -> 15
+ | GPR16 -> 16
+ | GPR17 -> 17
+ | GPR18 -> 18
+ | GPR19 -> 19
+ | GPR20 -> 20
+ | GPR21 -> 21
+ | GPR22 -> 22
+ | GPR23 -> 23
+ | GPR24 -> 24
+ | GPR25 -> 25
+ | GPR26 -> 26
+ | GPR27 -> 27
+ | GPR28 -> 28
+ | GPR29 -> 29
+ | GPR30 -> 30
+ | GPR31 -> 31
+ in p_jmember oc "Register" (fun oc -> fprintf oc "r%d") num
-let p_ireg oc = function
- | GPR0 -> fprintf oc "{\"Register\":\"r0\"}"
- | GPR1 -> fprintf oc "{\"Register\":\"r1\"}"
- | GPR2 -> fprintf oc "{\"Register\":\"r2\"}"
- | GPR3 -> fprintf oc "{\"Register\":\"r3\"}"
- | GPR4 -> fprintf oc "{\"Register\":\"r4\"}"
- | GPR5 -> fprintf oc "{\"Register\":\"r5\"}"
- | GPR6 -> fprintf oc "{\"Register\":\"r6\"}"
- | GPR7 -> fprintf oc "{\"Register\":\"r7\"}"
- | GPR8 -> fprintf oc "{\"Register\":\"r8\"}"
- | GPR9 -> fprintf oc "{\"Register\":\"r9\"}"
- | GPR10 -> fprintf oc "{\"Register\":\"r10\"}"
- | GPR11 -> fprintf oc "{\"Register\":\"r11\"}"
- | GPR12 -> fprintf oc "{\"Register\":\"r12\"}"
- | GPR13 -> fprintf oc "{\"Register\":\"r13\"}"
- | GPR14 -> fprintf oc "{\"Register\":\"r14\"}"
- | GPR15 -> fprintf oc "{\"Register\":\"r15\"}"
- | GPR16 -> fprintf oc "{\"Register\":\"r16\"}"
- | GPR17 -> fprintf oc "{\"Register\":\"r17\"}"
- | GPR18 -> fprintf oc "{\"Register\":\"r18\"}"
- | GPR19 -> fprintf oc "{\"Register\":\"r19\"}"
- | GPR20 -> fprintf oc "{\"Register\":\"r20\"}"
- | GPR21 -> fprintf oc "{\"Register\":\"r21\"}"
- | GPR22 -> fprintf oc "{\"Register\":\"r22\"}"
- | GPR23 -> fprintf oc "{\"Register\":\"r23\"}"
- | GPR24 -> fprintf oc "{\"Register\":\"r24\"}"
- | GPR25 -> fprintf oc "{\"Register\":\"r25\"}"
- | GPR26 -> fprintf oc "{\"Register\":\"r26\"}"
- | GPR27 -> fprintf oc "{\"Register\":\"r27\"}"
- | GPR28 -> fprintf oc "{\"Register\":\"r28\"}"
- | GPR29 -> fprintf oc "{\"Register\":\"r29\"}"
- | GPR30 -> fprintf oc "{\"Register\":\"r30\"}"
- | GPR31 -> fprintf oc "{\"Register\":\"r31\"}"
-
-let p_freg oc = function
- | FPR0 -> fprintf oc "{\"Register\":\"f0\"}"
- | FPR1 -> fprintf oc "{\"Register\":\"f1\"}"
- | FPR2 -> fprintf oc "{\"Register\":\"f2\"}"
- | FPR3 -> fprintf oc "{\"Register\":\"f3\"}"
- | FPR4 -> fprintf oc "{\"Register\":\"f4\"}"
- | FPR5 -> fprintf oc "{\"Register\":\"f5\"}"
- | FPR6 -> fprintf oc "{\"Register\":\"f6\"}"
- | FPR7 -> fprintf oc "{\"Register\":\"f7\"}"
- | FPR8 -> fprintf oc "{\"Register\":\"f8\"}"
- | FPR9 -> fprintf oc "{\"Register\":\"f9\"}"
- | FPR10 -> fprintf oc "{\"Register\":\"f10\"}"
- | FPR11 -> fprintf oc "{\"Register\":\"f11\"}"
- | FPR12 -> fprintf oc "{\"Register\":\"f12\"}"
- | FPR13 -> fprintf oc "{\"Register\":\"f13\"}"
- | FPR14 -> fprintf oc "{\"Register\":\"f14\"}"
- | FPR15 -> fprintf oc "{\"Register\":\"f15\"}"
- | FPR16 -> fprintf oc "{\"Register\":\"f16\"}"
- | FPR17 -> fprintf oc "{\"Register\":\"f17\"}"
- | FPR18 -> fprintf oc "{\"Register\":\"f18\"}"
- | FPR19 -> fprintf oc "{\"Register\":\"f19\"}"
- | FPR20 -> fprintf oc "{\"Register\":\"f20\"}"
- | FPR21 -> fprintf oc "{\"Register\":\"f21\"}"
- | FPR22 -> fprintf oc "{\"Register\":\"f22\"}"
- | FPR23 -> fprintf oc "{\"Register\":\"f23\"}"
- | FPR24 -> fprintf oc "{\"Register\":\"f24\"}"
- | FPR25 -> fprintf oc "{\"Register\":\"f25\"}"
- | FPR26 -> fprintf oc "{\"Register\":\"f26\"}"
- | FPR27 -> fprintf oc "{\"Register\":\"f27\"}"
- | FPR28 -> fprintf oc "{\"Register\":\"f28\"}"
- | FPR29 -> fprintf oc "{\"Register\":\"f29\"}"
- | FPR30 -> fprintf oc "{\"Register\":\"f30\"}"
- | FPR31 -> fprintf oc "{\"Register\":\"f31\"}"
+let p_freg oc reg =
+ let num = match reg with
+ | FPR0 -> 0
+ | FPR1 -> 1
+ | FPR2 -> 2
+ | FPR3 -> 3
+ | FPR4 -> 4
+ | FPR5 -> 5
+ | FPR6 -> 6
+ | FPR7 -> 7
+ | FPR8 -> 8
+ | FPR9 -> 9
+ | FPR10 -> 10
+ | FPR11 -> 11
+ | FPR12 -> 12
+ | FPR13 -> 13
+ | FPR14 -> 14
+ | FPR15 -> 15
+ | FPR16 -> 16
+ | FPR17 -> 17
+ | FPR18 -> 18
+ | FPR19 -> 19
+ | FPR20 -> 20
+ | FPR21 -> 21
+ | FPR22 -> 22
+ | FPR23 -> 23
+ | FPR24 -> 24
+ | FPR25 -> 25
+ | FPR26 -> 26
+ | FPR27 -> 27
+ | FPR28 -> 28
+ | FPR29 -> 29
+ | FPR30 -> 30
+ | FPR31 -> 31
+ in p_jmember oc "Register" (fun oc -> fprintf oc "f%d") num
let p_preg oc = function
| IR ir -> p_ireg oc ir
@@ -129,12 +132,6 @@ let p_crbit oc c =
let p_label oc l = fprintf oc "{\"Label\":%ld}" (P.to_int32 l)
-let p_list elem oc l =
- match l with
- | [] -> fprintf oc "[]"
- | hd::tail ->
- output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]"
-
type instruction_arg =
| Ireg of ireg
| Freg of freg
@@ -156,7 +153,7 @@ let p_arg oc = function
| Atom a -> p_atom_constant oc a
let p_instruction oc ic =
- let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_list p_arg) l
+ let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_jarray p_arg) l
and inst_name oc s = fprintf oc"%a:%a" p_jstring "Instruction Name" p_jstring s in
let first = ref true in
let sep oc = if !first then first := false else output_string oc ", " in
@@ -385,7 +382,7 @@ let p_vardef oc (name,v) =
fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n"
p_atom name v.gvar_readonly v.gvar_volatile
p_storage static p_int_opt alignment p_section section
- (p_list p_init_data) v.gvar_init
+ (p_jarray p_init_data) v.gvar_init
let p_program oc prog =
let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
@@ -394,5 +391,5 @@ let p_program oc prog =
| Gvar v -> (ident,v)::vars,funs
| _ -> vars,funs) ([],[]) prog.prog_defs in
fprintf oc "{\"Global Variables\":%a,\n\"Functions\":%a}"
- (p_list p_vardef) prog_vars
- (p_list p_fundef) prog_funs
+ (p_jarray p_vardef) prog_vars
+ (p_jarray p_fundef) prog_funs