summaryrefslogtreecommitdiff
path: root/checklink/PPC_parsers.ml
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-04-04 11:59:35 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-04-04 11:59:35 +0000
commitd892ae294cb2cec3fcf9445555f884420e90c346 (patch)
tree1619234a7f95f2fd874328c3238cfbbc314d0614 /checklink/PPC_parsers.ml
parent9f841d3335cfb9c0bd6f560b9c429c3c527eabe3 (diff)
Cleaning up checklink
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1865 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/PPC_parsers.ml')
-rw-r--r--checklink/PPC_parsers.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/checklink/PPC_parsers.ml b/checklink/PPC_parsers.ml
index ffbbc2f..192c14a 100644
--- a/checklink/PPC_parsers.ml
+++ b/checklink/PPC_parsers.ml
@@ -382,8 +382,6 @@ let parse_instr bs =
| { bits:32:bitstring }
-> UNKNOWN(bits)
-exception Wrong_code_size
-
let rec parse_code_as_list bs =
bitmatch bs with
| { instr:32:bitstring; rest:-1:bitstring } ->
@@ -391,7 +389,7 @@ let rec parse_code_as_list bs =
| { rest:-1:bitstring } ->
if Bitstring.bitstring_length rest = 0
then []
- else raise Wrong_code_size
+ else assert false
let parse_nth_instr bs n = parse_instr (Bitstring.subbitstring bs (n * 32) 32)