Eric Patrizio

Instrumentation and preprocessing

3

Hello, It seems that the instrumentation is launched before the preprocessor, generating errors in some cases. Here is a minimalistic example with sedlex preprocessing : ``` shell-session $ git clone...

Fixes issue #255

add a flag to print the solver statistics

9

fixes #184

symbolic instruction error: extend_i32/64

2

symbolic_value: I32 and I64 modules ```ocaml (* FIXME: This is probably wrong? *) let extend_s n x = cvtop ty (ExtS (32 - n)) (make (Extract (x, n / 8,...

symbolic instruction Encoding error: trunc_f32/64

6

symbolic_value: I32 and I64 modules ```ocaml let trunc_f32_s x = cvtop ty TruncSF32 x let trunc_f32_u x = cvtop ty TruncUF32 x let trunc_f64_s x = cvtop ty TruncSF64 x...

symbolic_value: I32 and I64 modules ```ocaml let trunc_sat_f32_s _ = assert false let trunc_sat_f32_u _ = assert false let trunc_sat_f64_s _ = assert false let trunc_sat_f64_u _ = assert false...

symbolic_value: I32 and I64 modules ```ocaml let popcnt _ = assert false ```

https://github.com/OCamlPro/owi/blob/d3650d2a50bfa852b8ec8ef41cdd679fb0749d66/src/symbolic_memory.ml#L45

https://github.com/OCamlPro/owi/blob/d3650d2a50bfa852b8ec8ef41cdd679fb0749d66/src/symbolic_memory.ml#L43