diff options
| author |  varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-04 11:59:35 +0000 |
|---|---|---|
| committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-04 11:59:35 +0000 |
| commit | d892ae294cb2cec3fcf9445555f884420e90c346 (patch) | |
| tree | 1619234a7f95f2fd874328c3238cfbbc314d0614 /checklink/PPC_parsers.ml | |
| parent | 9f841d3335cfb9c0bd6f560b9c429c3c527eabe3 (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.ml | 4 |
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) |