diff options
| author | Kathy Gray | 2015-10-29 13:32:36 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-10-29 18:13:59 +0000 |
| commit | 1601f337e10871cc7468c4b7abc5e4570f8d4411 (patch) | |
| tree | a3eec5bd846da5fc875f62fb8000acb48740ee22 /src/gen_lib | |
| parent | 91a38a0dbcac11574768ff2fa2cb180d8d897487 (diff) | |
Ocaml generation now just needing big int/little int issues resolved (probably) at least for Power.
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index c789ff52..8a1a27c6 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -15,6 +15,11 @@ let to_bool = function | Vone -> true | Vundef -> assert false +let is_one i = + if eq_big_int i unit_big_int + then Vone + else Vzero + let get_barray = function | Vvector(a,_,_) -> a | Vregister(a,_,_,_) -> !a @@ -117,8 +122,8 @@ let set_vector_subrange_vec v n m new_v = done; end in - match v with - | VvectorR(array,start,is_inc) -> + match v, new_v with + | VvectorR(array,start,is_inc),VvectorR(new_v,_,_) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in walker array length offset new_v | _ -> () |
