| /kernel/linux/linux-5.10/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/ |
| H A D | assume.h | 7 #define assume(x) \ macro
14 #define assume(x) __CPROVER_assume(x) macro
|
| H A D | simple_sync_srcu.c | 46 assume(try_check_zero(sp, idx, trycount)); in synchronize_srcu()
50 assume(try_check_zero(sp, idx^1, trycount)); in synchronize_srcu()
|
| H A D | preempt.c | 6 #include "assume.h"
66 assume(thread_cpu_id >= 0); in preempt_disable()
67 assume(thread_cpu_id < NR_CPUS); in preempt_disable()
|
| H A D | locks.h | 9 #include "assume.h"
82 * CBMC doesn't support busy waiting, so just assume that the in lock_impl_lock()
85 assume(lock_impl_trylock(lock)); in lock_impl_lock()
194 assume(prev_count); in wait_for_completion()
|
| H A D | misc.h | 4 #include "assume.h"
25 #define udelay(x) assume(0)
|
| /kernel/linux/linux-5.10/arch/m68k/ifpsp060/ |
| H A D | os.S | 152 clr.l %d1 | assume success
187 clr.l %d1 | assume success
223 clr.l %d1 | assume success
245 clr.l %d1 | assume success
267 clr.l %d1 | assume success
291 clr.l %d1 | assume success
306 | below assume that the SFC/DFC have been set previously.
|
| /kernel/linux/linux-6.6/arch/m68k/ifpsp060/ |
| H A D | os.S | 152 clr.l %d1 | assume success
187 clr.l %d1 | assume success
223 clr.l %d1 | assume success
245 clr.l %d1 | assume success
267 clr.l %d1 | assume success
291 clr.l %d1 | assume success
306 | below assume that the SFC/DFC have been set previously.
|
| /kernel/linux/linux-5.10/arch/mips/kernel/ |
| H A D | r2300_fpu.S | 68 li v0, 0 # assume success
102 li v0, 0 # assume success
|
| /kernel/linux/linux-6.6/arch/mips/kernel/ |
| H A D | r2300_fpu.S | 68 li v0, 0 # assume success
102 li v0, 0 # assume success
|
| /kernel/linux/linux-6.6/rust/alloc/ |
| H A D | alloc.rs | 213 intrinsics::assume(new_size >= old_layout.size()); in grow_impl()
304 intrinsics::assume(new_size <= old_layout.size()); in shrink()
|
| H A D | raw_vec.rs | 520 intrinsics::assume(old_layout.align() == new_layout.align()); in finish_grow()
|
| /kernel/linux/linux-5.10/arch/arm/include/debug/ |
| H A D | sa1100.S | 25 @ We assume r1 can be clobbered.
|
| /kernel/linux/linux-6.6/arch/arm/include/debug/ |
| H A D | sa1100.S | 25 @ We assume r1 can be clobbered.
|
| /kernel/linux/linux-5.10/arch/arm/kernel/ |
| H A D | head.S | 559 bne __fixup_smp_on_up @ no, assume UP
567 reteq lr @ yes, assume SMP
572 bne __fixup_smp_on_up @ no, assume UP
|
| /kernel/linux/linux-6.6/arch/xtensa/kernel/ |
| H A D | align.S | 196 addi a7, a7, 2 # increment PC (assume 16-bit insn)
271 addi a7, a7, 2 # increment PC (assume 16-bit insn)
382 addi a7, a7, 2 # incr. PC,assume 16-bit instruction
|
| /kernel/linux/linux-5.10/arch/xtensa/kernel/ |
| H A D | align.S | 247 addi a7, a7, 2 # increment PC (assume 16-bit insn)
349 addi a7, a7, 2 # incr. PC,assume 16-bit instruction
|
| H A D | entry.S | 804 addi a2, a1, -16-PT_SIZE # assume kernel stack
1206 * Note: We assume the stack pointer is EXC_TABLE_KSTK in the fixup handler.
1391 * Note: We assume EXC_TABLE_KSTK contains a valid stack pointer.
|
| /kernel/linux/linux-5.10/arch/sparc/mm/ |
| H A D | viking.S | 95 sethi %hi(MXCC_SRCSTREAM), %o3 ! assume %hi(MXCC_SRCSTREAM) == %hi(MXCC_DESTSTREAM)
|
| /kernel/linux/linux-6.6/arch/sparc/mm/ |
| H A D | viking.S | 95 sethi %hi(MXCC_SRCSTREAM), %o3 ! assume %hi(MXCC_SRCSTREAM) == %hi(MXCC_DESTSTREAM)
|
| /kernel/linux/linux-5.10/arch/m68k/fpsp040/ |
| H A D | round.S | 382 | We get here if ms mant was = 0, and we assume ls mant has bits
|
| /kernel/linux/linux-5.10/arch/x86/crypto/ |
| H A D | sha256-avx-asm.S | 52 ## assume buffers not aligned
|
| H A D | sha256-ssse3-asm.S | 51 ## assume buffers not aligned
|
| /kernel/linux/linux-6.6/arch/m68k/fpsp040/ |
| H A D | round.S | 382 | We get here if ms mant was = 0, and we assume ls mant has bits
|
| /kernel/linux/linux-6.6/arch/x86/crypto/ |
| H A D | sha256-avx-asm.S | 53 ## assume buffers not aligned
|
| H A D | sha256-ssse3-asm.S | 52 ## assume buffers not aligned
|