Searched refs:proof (Results 1 – 16 of 16) sorted by relevance
| /linux/kernel/bpf/ |
| H A D | diagnostics.h | 70 const char *reg_name, const char *type_name, const char *proof,
|
| H A D | diagnostics.c | 1953 const char *reg_name, const char *type_name, const char *proof, in bpf_diag_mem_bounds() argument
1973 proof, reg_name, type_name, offset_desc, size, mem_size); in bpf_diag_mem_bounds()
|
| H A D | verifier.c | 4338 const char *proof = ""; in check_mem_region_access() local
4362 proof = bpf_diag_fmt( in check_mem_region_access()
4376 proof = bpf_diag_fmt( in check_mem_region_access()
4392 proof = bpf_diag_fmt( in check_mem_region_access()
4406 proof = bpf_diag_fmt( in check_mem_region_access()
4417 reg_arg_name(env, argno), reg_type_str(env, reg->type), proof, in check_mem_region_access()
|
| /linux/rust/zerocopy/src/ |
| H A D | byte_slice.rs | 374 #[kani::proof]
|
| H A D | layout.rs | 2015 #[kani::proof]
2051 #[kani::proof]
2175 #[kani::proof]
2192 #[kani::proof]
|
| H A D | byteorder.rs | 1325 #[cfg_attr(kani, kani::proof)]
1336 #[cfg_attr(kani, kani::proof)]
1347 #[cfg_attr(kani, kani::proof)]
|
| /linux/rust/syn/ |
| H A D | parse.rs | 378 pub(crate) fn advance_step_cursor<'c, 'a>(proof: StepCursor<'c, 'a>, to: Cursor<'c>) -> Cursor<'a> { in advance_step_cursor()
383 let _ = proof; in advance_step_cursor()
|
| /linux/rust/zerocopy/src/util/ |
| H A D | mod.rs | 158 fn proof() { in padding_needed_for() function
242 fn proof() { in round_down_to_next_multiple_of_alignment() function
|
| /linux/Documentation/filesystems/nfs/ |
| H A D | nfs41-server.rst | 228 NFS4ERR_ENCR_ALG_UNSUPP on EXCHANGE_ID, which should be future-proof.
|
| /linux/Documentation/scheduler/ |
| H A D | sched-nice-design.rst | 86 proof, and a buggy SCHED_FIFO app can also lock up the system for good.
|
| /linux/Documentation/power/ |
| H A D | userland-swsusp.rst | 156 SNAPSHOT_ATOMIC_RESTORE will not succeed. Still, this is not a fool-proof
|
| /linux/Documentation/filesystems/ |
| H A D | directory-locking.rst | 236 That concludes the proof, since the set of operations with the
|
| /linux/Documentation/locking/ |
| H A D | lockdep-design.rst | 284 The validator achieves perfect, mathematical 'closure' (proof of locking
|
| /linux/lib/ |
| H A D | Kconfig.debug | 1474 The proof does not depend on how hard and complex a
1477 for it to trigger. The proof also does not depend on
1491 the proof of observed correctness is also maintained for an
|
| /linux/Documentation/ |
| H A D | memory-barriers.txt | 1640 will carry out its proof assuming that the current CPU is the only
1642 compiler's proof will be erroneous. Use READ_ONCE() to tell the
|
| /linux/tools/memory-model/Documentation/ |
| H A D | explanation.txt | 1599 a somewhat lengthy formal proof. Pretty much all you need to know
|