1- use crate :: { ir :: ModuleSpec , HashMap , HashSet } ;
1+ use crate :: { HashMap , HashSet , ir :: ModuleSpec } ;
22use std:: sync:: Arc ;
33
44use crate :: concolic:: MemoryAccessKind ;
@@ -8,9 +8,9 @@ use super::{BinaryOp, ConcolicEvent, SolverBackendError, SymVal, SymValRef, Symv
88
99use smtlib:: Logic ;
1010use smtlib:: {
11+ BitVec , Bool , SatResult ,
1112 prelude:: * ,
1213 terms:: { Const , Dynamic } ,
13- BitVec , Bool , SatResult ,
1414} ;
1515
1616#[ derive( Clone , Debug ) ]
@@ -134,12 +134,10 @@ impl<'ctx> SolverInstance<'ctx> {
134134 }
135135
136136 fn get_inp_bv ( & mut self , i : u16 ) -> Const < ' ctx , BitVec < ' ctx , 8 > > {
137- * self . inp_vals
138- . entry ( i)
139- . or_insert_with ( || {
140- let symbol = format ! ( "inp-{i}" ) ;
141- BitVec :: new_const ( self . storage , & symbol)
142- } )
137+ * self . inp_vals . entry ( i) . or_insert_with ( || {
138+ let symbol = format ! ( "inp-{i}" ) ;
139+ BitVec :: new_const ( self . storage , & symbol)
140+ } )
143141 }
144142
145143 fn new_prop ( & mut self ) -> Const < ' ctx , Bool < ' ctx > > {
@@ -193,7 +191,7 @@ impl<'ctx> SolverInstance<'ctx> {
193191 SymVal :: ConstI32 ( v) => BitVec :: < 32 > :: new ( self . storage , v as i64 ) . into ( ) ,
194192 SymVal :: ConstI64 ( v) => BitVec :: < 64 > :: new ( self . storage , v as i64 ) . into ( ) ,
195193 SymVal :: ConstF32 ( _) | SymVal :: ConstF64 ( _) => {
196- return Err ( SolverBackendError :: UnsupportedFloatingpointOperation )
194+ return Err ( SolverBackendError :: UnsupportedFloatingpointOperation ) ;
197195 }
198196 SymVal :: Unary ( op, bv) => {
199197 let val = self . get_symval ( bv, context) ?;
@@ -268,7 +266,7 @@ impl<'ctx> SolverInstance<'ctx> {
268266 MemoryAccessKind :: I64AsS32 => combine_32 ( & bytes) . sext :: < 32 , 64 > ( ) . into ( ) ,
269267 MemoryAccessKind :: I64AsU32 => combine_32 ( & bytes) . uext :: < 32 , 64 > ( ) . into ( ) ,
270268 MemoryAccessKind :: F32 | MemoryAccessKind :: F64 => {
271- return Err ( SolverBackendError :: UnsupportedFloatingpointOperation )
269+ return Err ( SolverBackendError :: UnsupportedFloatingpointOperation ) ;
272270 }
273271 }
274272 // zero-width bvs are not allowed :(
0 commit comments