summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorPeter Sewell2014-11-23 16:59:20 +0000
committerPeter Sewell2014-11-23 16:59:20 +0000
commit9d61b77442d75685c533e2c0e4c8a75bc219b792 (patch)
tree1703333cfed501231c5e6b563385b98117aa6bac /src
parentadb18ab321740919fa66967bae4705996f602525 (diff)
wib
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_interface.lem12
-rw-r--r--src/lem_interp/printing_functions.ml8
2 files changed, 10 insertions, 10 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index f01a51cb..34d31ad2 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -496,15 +496,15 @@ let byte_of_byte_lifted bl =
val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*)
let rec bytes_of_bits bits = match bits with
| [] -> []
- | b1::b2::b3::b4::b5::b6::b7::b8::bits ->
- (Byte [b1;b2;b3;b4;b5;b6;b7;b8])::(bytes_of_bits bits)
+ | b0::b1::b2::b3::b4::b5::b6::b7::bits ->
+ (Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits)
end
val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*)
let rec byte_lifteds_of_bit_lifteds bits = match bits with
| [] -> []
- | b1::b2::b3::b4::b5::b6::b7::b8::bits ->
- (Byte_lifted [b1;b2;b3;b4;b5;b6;b7;b8])::(byte_lifteds_of_bit_lifteds bits)
+ | b0::b1::b2::b3::b4::b5::b6::b7::bits ->
+ (Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits)
end
@@ -527,7 +527,7 @@ let integer_of_bit_list b =
val bit_list_of_integer : int -> integer -> list bit
let bit_list_of_integer len b =
List.map (fun b -> if b then Bitc_one else Bitc_zero)
- (reverse (boolListFrombitSeq (natFromInt len) (bitSeqFromInteger Nothing b))) (* PS really? that reverse seemed to make it worse... *)
+ (reverse (boolListFrombitSeq (natFromInt len) (bitSeqFromInteger Nothing b)))
val integer_of_byte_list : list byte -> integer
let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
@@ -557,7 +557,7 @@ let rec integerFromIntListAux (acc: integer) (is: list int) =
| (i :: is') -> integerFromIntListAux ((acc * 256) + integerFromInt i) is'
end
let integer_address_of_int_list (is: list int) =
- integerFromIntListAux 0 (List.reverse is)
+ integerFromIntListAux 0 is
val address_of_byte_list : list byte -> address
let address_of_byte_list bs =
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index a8eebf97..46c7d227 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -90,7 +90,7 @@ let hex_int_to_string i =
let bytes_lifted_homogenous_to_string = function
| Bitslh_concrete bs ->
- let i = Big_int.int_of_big_int (Interp_interface.integer_of_bit_list (List.rev bs)) in
+ let i = Big_int.int_of_big_int (Interp_interface.integer_of_bit_list bs) in
hex_int_to_string i
| Bitslh_undef -> "uu"
| Bitslh_unknown -> "??"
@@ -116,7 +116,7 @@ let bit_lifteds_to_string (bls: bit_lifted list) (starto : int option) =
| None -> (* print as bitvector after all *)
simple_bit_lifteds_to_string bls starto
| Some (byteslhs: bits_lifted_homogenous list) ->
- let s = String.concat "" (List.map bytes_lifted_homogenous_to_string (List.rev byteslhs)) in
+ let s = String.concat "" (List.map bytes_lifted_homogenous_to_string byteslhs) in
match starto with
| None -> "0x" ^ s
| Some start -> "0x" ^ "_" ^string_of_int start ^"'" ^ s
@@ -397,8 +397,8 @@ let rec instr_parms_to_string ps =
let pad n s = if String.length s < n then s ^ String.make (n-String.length s) ' ' else s
let instruction_to_string (name, parms, base_effects) =
- raise (Failure "TODO instruction_to_string")
-(* (pad 5 (String.lowercase name)) ^ " " ^ instr_parms_to_string parms *)
+(* "TODO instruction_to_string"*)
+ (pad 5 (String.lowercase name)) ^ " " ^ instr_parms_to_string parms
let print_backtrace_compact printer stack = List.iter (fun (e,(env,mem)) -> print_exp printer env e) (compact_stack stack)
let print_continuation printer stack = let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env e