diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 218f20e7..37f73a1e 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -366,7 +366,7 @@ let rec slice_vector v n1 n2 = match v with | V_vector m inc vs -> if inc - then V_vector 0 inc (from_n_to_n (n1 - m) (n2 - m) vs) + then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) vs) else V_vector (n1 - n2 + 1) inc (from_n_to_n (m - n1) (m - n2) vs) | V_vector_sparse m n inc vs d -> let (slice, still_sparse) = @@ -374,7 +374,7 @@ let rec slice_vector v n1 n2 = then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2 else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in if still_sparse && inc - then V_vector_sparse 0 (n2 - n1) inc slice d + then V_vector_sparse n1 (n2 - n1) inc slice d else if inc then V_vector 0 inc (List.map snd slice) else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) inc slice d else V_vector (n1 - n2 +1) inc (List.map snd slice) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 68076627..049ca92d 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -94,7 +94,7 @@ let rec slice_value bits start stop = Bitvector (Interp.from_n_to_n (if inc then (start - fst) else (fst - start)) (if inc then (stop - fst) else (fst - stop)) bools) inc - (if inc then 0 else ((stop - start) + 1)) + (if inc then start else ((stop - start) + 1)) | Bytevector bytes -> Bytevector (Interp.from_n_to_n start stop bytes) | Unknown -> Unknown diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index 8a047a5b..fe547201 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -54,7 +54,7 @@ let rec slice bitvector (start,stop) = Bitvector ((Interp.from_n_to_n (if inc then (sub_big_int start fst) else (sub_big_int fst start)) (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bools), inc, - (if inc then zero_big_int else (add_big_int (sub_big_int stop start) unit_big_int))) + (if inc then start else (add_big_int (sub_big_int stop start) unit_big_int))) | Bytevector bytes -> Bytevector((Interp.from_n_to_n start stop bytes)) (*This is wrong, need to explode and re-encode, but maybe never happens?*) |