diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-12-13 17:40:35 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-12-13 17:40:35 +0100 |
| commit | d2ae46db53df8b5cbdff682451e58e4c3e64b4db (patch) | |
| tree | 2a407ab3032edbb14b0d8b6151dde617aa1bec10 /driver | |
| parent | 6753e8f33cd4b26dbb256ae4886f11d60eb0e370 (diff) | |
| download | compcert-d2ae46db53df8b5cbdff682451e58e4c3e64b4db.tar.gz compcert-d2ae46db53df8b5cbdff682451e58e4c3e64b4db.zip | |
Export configured architecture to JSON (#38)
The architecture which was configured is now exported in a new top-level json field.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 0e01dbb5..21fb0db3 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -50,6 +50,12 @@ let dump_jasm asm sourcename destfile = pp_jobject_end pp in pp_jobject_start pp; pp_jmember ~first:true pp "Version" pp_jstring jdump_magic_number; + let json_arch = + match Configuration.arch, !Clflags.option_mthumb with + | "arm", false -> "arm-arm" + | "arm", true -> "arm-thumb" + | a, _ -> a in + pp_jmember pp "Architecture" pp_jstring json_arch; pp_jmember pp "System" pp_jstring Configuration.system; pp_jmember pp "Compile Info" dump_compile_info (); pp_jmember pp "Compilation Unit" pp_jstring sourcename; |