@@ -245,43 +245,6 @@ impl<'tcx> GotocHook<'tcx> for Panic {
245
245
}
246
246
}
247
247
248
- struct PtrRead ;
249
-
250
- impl < ' tcx > GotocHook < ' tcx > for PtrRead {
251
- fn hook_applies ( & self , tcx : TyCtxt < ' tcx > , instance : Instance < ' tcx > ) -> bool {
252
- let name = with_no_trimmed_paths ! ( tcx. def_path_str( instance. def_id( ) ) ) ;
253
- name == "core::ptr::read"
254
- || name == "core::ptr::read_unaligned"
255
- || name == "core::ptr::read_volatile"
256
- || name == "std::ptr::read"
257
- || name == "std::ptr::read_unaligned"
258
- || name == "std::ptr::read_volatile"
259
- }
260
-
261
- fn handle (
262
- & self ,
263
- tcx : & mut GotocCtx < ' tcx > ,
264
- _instance : Instance < ' tcx > ,
265
- mut fargs : Vec < Expr > ,
266
- assign_to : Place < ' tcx > ,
267
- target : Option < BasicBlock > ,
268
- span : Option < Span > ,
269
- ) -> Stmt {
270
- let loc = tcx. codegen_span_option ( span) ;
271
- let target = target. unwrap ( ) ;
272
- let src = fargs. remove ( 0 ) ;
273
- Stmt :: block (
274
- vec ! [
275
- unwrap_or_return_codegen_unimplemented_stmt!( tcx, tcx. codegen_place( & assign_to) )
276
- . goto_expr
277
- . assign( src. dereference( ) . with_location( loc) , loc) ,
278
- Stmt :: goto( tcx. current_fn( ) . find_label( & target) , loc) ,
279
- ] ,
280
- loc,
281
- )
282
- }
283
- }
284
-
285
248
struct RustAlloc ;
286
249
// Removing this hook causes regression failures.
287
250
// https://github.com/model-checking/kani/issues/1170
@@ -362,7 +325,6 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
362
325
Rc :: new( Assert ) ,
363
326
Rc :: new( ExpectFail ) ,
364
327
Rc :: new( Nondet ) ,
365
- Rc :: new( PtrRead ) ,
366
328
Rc :: new( RustAlloc ) ,
367
329
Rc :: new( SliceFromRawPart ) ,
368
330
] ,
0 commit comments