1 /* SPDX-License-Identifier: GPL-2.0+ */
6 * Texas Instruments Incorporated, <www.ti.com>
12 #include <asm/arch/hardware.h>
38 void msmc_share_all_segments(int priv_id);
39 void msmc_get_ses_mpax(int priv_id, int ses_pair, u32 *mpax);
40 void msmc_set_ses_mpax(int priv_id, int ses_pair, u32 *mpax);
41 void msmc_map_ses_segment(int priv_id, int ses_pair,
42 u32 src_pfn, u32 dst_pfn, enum mpax_seg_size size);