aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/AsmToJSON.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-09-22 15:01:34 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2017-09-22 15:01:34 +0200
commit0f210f622a4609811959f4450f770c61f5eb6532 (patch)
tree847efeee3b28cfb44acd551743164858cb4e1902 /powerpc/AsmToJSON.ml
parent45aeaf195645a870b54e606c3407f5c65188ad98 (diff)
downloadcompcert-kvx-0f210f622a4609811959f4450f770c61f5eb6532.tar.gz
compcert-kvx-0f210f622a4609811959f4450f770c61f5eb6532.zip
Disallow usage of default pattern for AsmToJSON.
In order to ensure that no new instruction is added without adding it to the Json export we enforce warning 4 for the instruction printer and removed all default pattern matchings. Bug 22239
Diffstat (limited to 'powerpc/AsmToJSON.ml')
-rw-r--r--powerpc/AsmToJSON.ml13
1 files changed, 11 insertions, 2 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index e84746a8..2017d3e3 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -128,7 +128,7 @@ let pp_instructions pp ic =
pp_jmember ~first:true pp "Instruction Name" pp_jstring n;
pp_jmember pp "Args" (pp_jarray pp_arg) args;
pp_jobject_end pp in
- let instruction pp = function
+ let [@ocaml.warning "+4"] instruction pp = function
| Padd (ir1,ir2,ir3)
| Padd64 (ir1,ir2,ir3) -> instruction pp "Padd" [Ireg ir1; Ireg ir2; Ireg ir3]
| Paddc (ir1,ir2,ir3) -> instruction pp "Paddc" [Ireg ir1; Ireg ir2; Ireg ir3]
@@ -353,7 +353,16 @@ let pp_instructions pp ic =
Buffer.add_char buf c) annot_string;
let annot_string = Buffer.contents buf in
instruction pp "Pannot" [String annot_string]
- | _ -> assert false
+ | EF_annot_val _
+ | EF_builtin _
+ | EF_debug _
+ | EF_external _
+ | EF_free
+ | EF_malloc
+ | EF_memcpy _
+ | EF_runtime _
+ | EF_vload _
+ | EF_vstore _ -> assert false
end
| Pcfi_adjust _ (* Only debug relevant *)
| Pcfi_rel_offset _ -> assert false in (* Only debug relevant *)