diff options
Diffstat (limited to 'src/lem_interp/interp.lem')
| -rw-r--r-- | src/lem_interp/interp.lem | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index f2fbcec2..efb1db7a 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -417,11 +417,11 @@ let detaint value = | v -> v end -let binary_taint thunk vall valr = +let rec binary_taint thunk vall valr = match (vall,valr) with - | (V_track vl rl,V_track vr rr) -> taint (thunk vl vr) (rl++rr) - | (V_track vl rl,vr) -> taint (thunk vl vr) rl - | (vl,V_track vr rr) -> taint (thunk vl vr) rr + | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl++rr) + | (V_track vl rl,vr) -> taint (binary_taint thunk vl vr) rl + | (vl,V_track vr rr) -> taint (binary_taint thunk vl vr) rr | (vl,vr) -> thunk vl vr end @@ -1237,7 +1237,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let (by_e,env) = to_exp mode le by_val_whole in match by_val with | V_lit (L_aux (L_num by_num) bl) -> - if (from_num = to_num) + if ((is_inc && (from_num >= to_num)) || (from_num <= to_num)) then (Value(V_lit (L_aux L_unit l)),lm,le) else let (ftyp,ttyp,btyp) = (val_typ from_val,val_typ to_val,val_typ by_val) in @@ -1458,7 +1458,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let inc = n1 < n2 in V_vector n1 inc (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown) - | _ -> Assert_extra.failwith "Vector slice of non-vector" end) end) in + | _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end) in (Value (binary_taint take_slice slice vvec), lm,le)) (fun a -> let rebuild v env = let (ie1,env) = to_exp mode env i1v in |