Patch VeriFast proofs

btj · btj · commit feee4345b1d5 · 2025-08-06T08:40:50.000+02:00
diff --git a/verifast-proofs/alloc/raw_vec/mod.rs/original/raw_vec.rs b/verifast-proofs/alloc/raw_vec/mod.rs/original/raw_vec.rs
@@ -761,7 +761,7 @@ impl<A: Allocator> RawVecInner<A> {
 }
 
 // not marked inline(never) since we want optimizers to be able to observe the specifics of this
-// function, see tests/codegen/vec-reserve-extend.rs.
+// function, see tests/codegen-llvm/vec-reserve-extend.rs.
 #[cold]
 fn finish_grow<A>(
     new_layout: Layout,
diff --git a/verifast-proofs/alloc/raw_vec/mod.rs/verified/raw_vec.rs b/verifast-proofs/alloc/raw_vec/mod.rs/verified/raw_vec.rs
@@ -1978,7 +1978,7 @@ impl<A: Allocator> RawVecInner<A> {
 }
 
 // not marked inline(never) since we want optimizers to be able to observe the specifics of this
-// function, see tests/codegen/vec-reserve-extend.rs.
+// function, see tests/codegen-llvm/vec-reserve-extend.rs.
 #[cold]
 fn finish_grow<A>(
     new_layout: Layout,
diff --git a/verifast-proofs/alloc/raw_vec/mod.rs/with-directives/raw_vec.rs b/verifast-proofs/alloc/raw_vec/mod.rs/with-directives/raw_vec.rs
@@ -761,7 +761,7 @@ impl<A: Allocator> RawVecInner<A> {
 }
 
 // not marked inline(never) since we want optimizers to be able to observe the specifics of this
-// function, see tests/codegen/vec-reserve-extend.rs.
+// function, see tests/codegen-llvm/vec-reserve-extend.rs.
 #[cold]
 fn finish_grow<A>(
     new_layout: Layout,

Original file line number	Diff line number	Diff line change
`@@ -761,7 +761,7 @@ impl<A: Allocator> RawVecInner<A> {`
`761`	`761`	`}`
`762`	`762`
`763`	`763`	`// not marked inline(never) since we want optimizers to be able to observe the specifics of this`
`764`		`-// function, see tests/codegen/vec-reserve-extend.rs.`
	`764`	`+// function, see tests/codegen-llvm/vec-reserve-extend.rs.`
`765`	`765`	`#[cold]`
`766`	`766`	`fn finish_grow<A>(`
`767`	`767`	`new_layout: Layout,`
Original file line number	Diff line number	Diff line change
`@@ -1978,7 +1978,7 @@ impl<A: Allocator> RawVecInner<A> {`
`1978`	`1978`	`}`
`1979`	`1979`
`1980`	`1980`	`// not marked inline(never) since we want optimizers to be able to observe the specifics of this`
`1981`		`-// function, see tests/codegen/vec-reserve-extend.rs.`
	`1981`	`+// function, see tests/codegen-llvm/vec-reserve-extend.rs.`
`1982`	`1982`	`#[cold]`
`1983`	`1983`	`fn finish_grow<A>(`
`1984`	`1984`	`new_layout: Layout,`