diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-10-19 13:08:13 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-19 13:08:13 +0200 |
| commit | 6a010b47b216c5a6b6e85abcfbba5339bab15dd6 (patch) | |
| tree | 4c7f8bacd081f023cfd3220b0aac0e186567d051 /powerpc/AsmToJSON.ml | |
| parent | a0f238a3d270edd7042d9852d43e3ec5b9602af2 (diff) | |
| download | compcert-kvx-6a010b47b216c5a6b6e85abcfbba5339bab15dd6.tar.gz compcert-kvx-6a010b47b216c5a6b6e85abcfbba5339bab15dd6.zip | |
New support for inserting ais-annotations.
The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.
The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.
Diffstat (limited to 'powerpc/AsmToJSON.ml')
| -rw-r--r-- | powerpc/AsmToJSON.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index b542d7a7..a3e57e51 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -367,7 +367,7 @@ let pp_instructions pp ic = | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" - | EF_annot (txt,targs) -> + | EF_annot (kind,txt,targs) -> let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in let len = String.length annot_string in let buf = Buffer.create len in @@ -376,7 +376,11 @@ let pp_instructions pp ic = | _ -> () end; Buffer.add_char buf c) annot_string; let annot_string = Buffer.contents buf in - instruction pp "Pannot" [String annot_string] + let kind = match P.to_int kind with + | 1 -> "normal" + | 2 -> "ais" + | _ -> assert false in + instruction pp "Pannot" [String kind;String annot_string] | EF_annot_val _ | EF_builtin _ | EF_debug _ @@ -423,7 +427,8 @@ let pp_section pp sec = | Section_debug_line _ | Section_debug_loc | Section_debug_ranges - | Section_debug_str -> () (* There should be no info in the debug sections *) + | Section_debug_str + | Section_ais_annotation -> () (* There should be no info in the debug sections *) let pp_int_opt pp = function | None -> fprintf pp "0" |