coreboot
coreboot is an Open Source project aimed at replacing the proprietary BIOS found in most computers.
stack.h
Go to the documentation of this file.
1 /* SPDX-License-Identifier: GPL-2.0-only */
2 
3 #ifndef _COMMON_STACK_H_
4 #define _COMMON_STACK_H_
5 
6 #include <stdint.h>
7 
8 static inline void *stack_push32(void *stack, uint32_t value)
9 {
10  uint32_t *stack32 = stack;
11 
12  stack32 = &stack32[-1];
13  *stack32 = value;
14  return stack32;
15 }
16 
17 #endif /* _COMMON_STACK_H_ */
value
pte_t value
Definition: mmu.c:91
stack_push32
static void * stack_push32(void *stack, uint32_t value)
Definition: stack.h:8
uint32_t
unsigned int uint32_t
Definition: stdint.h:14