simplify implementation of owi_char

OCamlPro · Jul 31, 2024 · 11e8630 · 11e8630
1 parent 4857582
commit 11e8630
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 15 deletions.
diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml
@@ -41,18 +41,7 @@ module M :
  in
  (I32 n, Value.pair n sym_expr) )
 
- let symbol_char () : Value.int32 Choice.t =
- Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value ->
- let n =
- match forced_value with
- | None -> Int32.logand 0xFFl (Random.bits32 ())
- | Some (Num (I32 n)) -> n
- | _ -> assert false
- in
- let sym_expr =
- Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.mk_symbol sym))
- in
- (I32 n, Value.pair n sym_expr) )
+ let symbol_char = symbol_i8
 
  let symbol_i64 () : Value.int64 Choice.t =
  Choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value ->

diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
@@ -35,9 +35,7 @@ module M :
  Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
  Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) )
 
- let symbol_char () =
- Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
- Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) )
+ let symbol_char = symbol_i8
 
  let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol