portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Remove many MODIFIES annotations.

Browse source 
These are redundant for any function which the C-to-Isabelle parser
actually analyses, which is now the vast majority of functions.
This commit is contained in:
Thomas Sewell 2016-12-09 11:32:05 +11:00
parent 117785483a
commit 97bac2345f
16 changed files with 6 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
include/arch/arm/arch/32/mode/fastpath/fastpath.h
View file

@ -30,6 +30,7 @@ compile_assert(SysReplyRecv_Minus2, SysReplyRecv == -2)
#define endpoint_ptr_get_epQueue_tail_fp(ep_ptr) TCB_PTR(endpoint_ptr_get_epQueue_tail(ep_ptr))
#define cap_vtable_cap_get_vspace_root_fp(vtable_cap) PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(vtable_cap))
/** MODIFIES: [*] */
/** DONT_TRANSLATE */
static inline void
clearExMonitor_fp(void)

28
include/arch/arm/arch/32/mode/machine.h
View file

@ -62,8 +62,6 @@ void setNextPC(tcb_t *thread, word_t v);
/* Architecture specific machine operations */
/** MODIFIES: [*] */
static inline word_t getProcessorID(void)
{
word_t processor_id;
@ -107,15 +105,11 @@ static inline void clearExMonitor(void)
asm volatile("strex r0, r1, [%0]" : : "r"(&tmp) : "r0");
}
/** MODIFIES: [*] */
static inline void flushBTAC(void)
{
asm volatile("mcr p15, 0, %0, c7, c5, 6" : : "r"(0));
}
/** MODIFIES: [*] */
static inline void writeContextID(word_t id)
{
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
@ -127,7 +121,6 @@ static inline void writeContextID(word_t id)
}
/* Address space control */
/** MODIFIES: [*] */
static inline void writeTTBR0(paddr_t addr)
{
@ -167,7 +160,6 @@ static inline void setCurrentPD(paddr_t addr)
}
/* TLB control */
/** MODIFIES: [*] */
static inline void invalidateTLB(void)
{
@ -176,7 +168,6 @@ static inline void invalidateTLB(void)
dsb();
isb();
}
/** MODIFIES: [*] */
static inline void invalidateTLB_ASID(hw_asid_t hw_asid)
{
@ -189,7 +180,6 @@ static inline void invalidateTLB_ASID(hw_asid_t hw_asid)
isb();
}
}
/** MODIFIES: [*] */
static inline void invalidateTLB_VAASID(word_t mva_plus_asid)
{
@ -202,10 +192,8 @@ static inline void invalidateTLB_VAASID(word_t mva_plus_asid)
isb();
}
}
/** MODIFIES: [*] */
void lockTLBEntry(vptr_t vaddr);
/** MODIFIES: [*] */
void lockTLBEntry(vptr_t vaddr);
static inline void cleanByVA(vptr_t vaddr, paddr_t paddr)
{
@ -221,8 +209,8 @@ static inline void cleanByVA(vptr_t vaddr, paddr_t paddr)
/* Erratum 586323 - end with DMB to ensure the write goes out. */
dmb();
}
/* D-Cache clean to PoU (L2 cache) (v6/v7 common) */
/** MODIFIES: [*] */
static inline void cleanByVA_PoU(vptr_t vaddr, paddr_t paddr)
{
#ifdef ARM_CORTEX_A8
@ -247,9 +235,8 @@ static inline void cleanByVA_PoU(vptr_t vaddr, paddr_t paddr)
/* Erratum 586323 - end with DMB to ensure the write goes out. */
dmb();
}
/* D-Cache invalidate to PoC (v6/v7 common) */
/** MODIFIES: [*] */
/* D-Cache invalidate to PoC (v6/v7 common) */
static inline void invalidateByVA(vptr_t vaddr, paddr_t paddr)
{
#ifdef ARM_CORTEX_A8
@ -261,7 +248,6 @@ static inline void invalidateByVA(vptr_t vaddr, paddr_t paddr)
#endif
dmb();
}
/** MODIFIES: [*] */
/* I-Cache invalidate to PoU (L2 cache) (v6/v7 common) */
static inline void invalidateByVA_I(vptr_t vaddr, paddr_t paddr)
@ -274,7 +260,6 @@ static inline void invalidateByVA_I(vptr_t vaddr, paddr_t paddr)
#endif
isb();
}
/** MODIFIES: [*] */
/* I-Cache invalidate all to PoU (L2 cache) (v6/v7 common) */
static inline void invalidate_I_PoU(void)
@ -286,7 +271,6 @@ static inline void invalidate_I_PoU(void)
asm volatile("mcr p15, 0, %0, c7, c5, 0" : : "r"(0));
isb();
}
/** MODIFIES: [*] */
/* D-Cache clean & invalidate to PoC (v6/v7 common) */
static inline void cleanInvalByVA(vptr_t vaddr, paddr_t paddr)
@ -302,7 +286,6 @@ static inline void cleanInvalByVA(vptr_t vaddr, paddr_t paddr)
#endif
dsb();
}
/** MODIFIES: [*] */
/* Invalidate branch predictors by VA (v6/v7 common) */
static inline void branchFlush(vptr_t vaddr, paddr_t paddr)
@ -311,7 +294,6 @@ static inline void branchFlush(vptr_t vaddr, paddr_t paddr)
}
/* Fault status */
/** MODIFIES: */
static inline word_t PURE getIFSR(void)
{
@ -319,7 +301,6 @@ static inline word_t PURE getIFSR(void)
asm volatile("mrc p15, 0, %0, c5, c0, 1" : "=r"(IFSR));
return IFSR;
}
/** MODIFIES: */
static inline word_t PURE getDFSR(void)
{
@ -327,7 +308,6 @@ static inline word_t PURE getDFSR(void)
asm volatile("mrc p15, 0, %0, c5, c0, 0" : "=r"(DFSR));
return DFSR;
}
/** MODIFIES: */
static inline word_t PURE getFAR(void)
{
@ -336,7 +316,6 @@ static inline word_t PURE getFAR(void)
return FAR;
}
/** MODIFIES: [*] */
static inline word_t getACTLR(void)
{
word_t ACTLR;
@ -344,7 +323,6 @@ static inline word_t getACTLR(void)
return ACTLR;
}
/** MODIFIES: [*] */
static inline void setACTLR(word_t actlr)
{
asm volatile ("mcr p15, 0, %0, c1, c0, 1" :: "r"(actlr));

16
include/arch/arm/arch/32/mode/machine_pl2.h
View file

@ -16,7 +16,6 @@
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
/** MODIFIES: [*] */
static inline void writeContextIDPL2(word_t id)
{
word_t pd_val, vmid;
@ -25,7 +24,6 @@ static inline void writeContextIDPL2(word_t id)
isb();
}
/** MODIFIES: [*] */
static inline void writeContextIDAndPD(word_t id, word_t pd_val)
{
asm volatile("mcrr p15, 6, %0, %1, c2" : : "r"(pd_val), "r"(id << (48-32)));
@ -33,7 +31,6 @@ static inline void writeContextIDAndPD(word_t id, word_t pd_val)
}
/** MODIFIES: [*] */
static inline void setCurrentPDPL2(paddr_t addr)
{
word_t pd_val, vmid;
@ -43,7 +40,6 @@ static inline void setCurrentPDPL2(paddr_t addr)
isb();
}
/** MODIFIES: [*] */
static inline void setCurrentHypPD(paddr_t addr)
{
word_t zero = 0;
@ -52,7 +48,6 @@ static inline void setCurrentHypPD(paddr_t addr)
isb();
}
/** MODIFIES: [*] */
static inline void setVTCR(word_t r)
{
dsb();
@ -60,7 +55,6 @@ static inline void setVTCR(word_t r)
isb();
}
/** MODIFIES: [*] */
static inline void setHCR(word_t r)
{
dsb();
@ -68,7 +62,6 @@ static inline void setHCR(word_t r)
isb();
}
/** MODIFIES: [*] */
static inline void setHMAIR(word_t hmair0, word_t hmair1)
{
asm volatile("mcr p15, 4, %0, c10, c2, 0" : : "r"(hmair0));
@ -76,7 +69,6 @@ static inline void setHMAIR(word_t hmair0, word_t hmair1)
isb();
}
/** MODIFIES: [*] */
static inline void setMAIR(word_t hmair0, word_t hmair1)
{
asm volatile("mcr p15, 0, %0, c10, c2, 0" : : "r"(hmair0));
@ -84,7 +76,6 @@ static inline void setMAIR(word_t hmair0, word_t hmair1)
isb();
}
/** MODIFIES: [*] */
static inline void invalidateHypTLB(void)
{
dsb();
@ -93,7 +84,6 @@ static inline void invalidateHypTLB(void)
isb();
}
/** MODIFIES: [*] */
static inline paddr_t PURE addressTranslateS1CPR(vptr_t vaddr)
{
uint64_t ipa;
@ -104,7 +94,6 @@ static inline paddr_t PURE addressTranslateS1CPR(vptr_t vaddr)
return ipa;
}
/** MODIFIES: [*] */
static inline word_t PURE getHSR(void)
{
word_t HSR;
@ -112,7 +101,6 @@ static inline word_t PURE getHSR(void)
return HSR;
}
/** MODIFIES: [*] */
static inline word_t PURE getHDFAR(void)
{
word_t HDFAR;
@ -120,7 +108,6 @@ static inline word_t PURE getHDFAR(void)
return HDFAR;
}
/** MODIFIES: [*] */
static inline word_t PURE getHIFAR(void)
{
word_t HIFAR;
@ -128,7 +115,6 @@ static inline word_t PURE getHIFAR(void)
return HIFAR;
}
/** MODIFIES: [*] */
static inline word_t PURE getHPFAR(void)
{
word_t HPFAR;
@ -136,7 +122,6 @@ static inline word_t PURE getHPFAR(void)
return HPFAR;
}
/** MODIFIES: [*] */
static inline word_t getSCTLR(void)
{
word_t SCTLR;
@ -144,7 +129,6 @@ static inline word_t getSCTLR(void)
return SCTLR;
}
/** MODIFIES: [*] */
static inline void setSCTLR(word_t sctlr)
{
asm volatile ("mcr p15, 0, %0, c1, c0, 0" :: "r"(sctlr));

15
include/arch/arm/arch/machine.h
View file

@ -24,40 +24,25 @@ int get_num_dev_p_regs(void);
p_region_t get_dev_p_reg(word_t i);
void map_kernel_devices(void);
/** MODIFIES: [*] */
void initL2Cache(void);
void initIRQController(void);
/** MODIFIES: [*] */
static inline void plat_cleanL2Range(paddr_t start, paddr_t end);
/** MODIFIES: [*] */
static inline void plat_invalidateL2Range(paddr_t start, paddr_t end);
/** MODIFIES: [*] */
static inline void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end);
/** MODIFIES: [*] */
static inline void plat_cleanInvalidateCache(void);
/** MODIFIES: [*] */
void cleanInvalidateCacheRange_RAM(word_t start, word_t end, paddr_t pstart);
/** MODIFIES: [*] */
void cleanCacheRange_RAM(word_t start, word_t end, paddr_t pstart);
/** MODIFIES: [*] */
void cleanCacheRange_PoU(word_t start, word_t end, paddr_t pstart);
/** MODIFIES: [*] */
void invalidateCacheRange_RAM(word_t start, word_t end, paddr_t pstart);
/** MODIFIES: [*] */
void invalidateCacheRange_I(word_t start, word_t end, paddr_t pstart);
/** MODIFIES: [*] */
void branchFlushRange(word_t start, word_t end, paddr_t pstart);
/** MODIFIES: [*] */
void clean_D_PoU(void);
/** MODIFIES: [*] */
void cleanInvalidate_D_PoC(void);
/** MODIFIES: [*] */
void cleanCaches_PoU(void);
/** MODIFIES: [*] */
void cleanInvalidateL1Caches(void);
/* Cleaning memory before user-level access */

1
include/arch/arm/arch/machine/gic_pl390.h
View file

@ -211,7 +211,6 @@ handleSpuriousIRQ(void)
{
}
/** MODIFIES: [*] */
void initIRQController(void);
#endif /* !__ARCH_MACHINE_GICPL390_H */

6
include/arch/arm/arch/machine/l2c_310.h
View file

@ -18,18 +18,12 @@
#include <arch/types.h>
/** MODIFIES: [*] */
void initL2Cache(void);
/** MODIFIES: [*] */
void plat_cleanInvalidateCache(void);
/** MODIFIES: [*] */
void plat_cleanCache(void);
/** MODIFIES: [*] */
void plat_cleanL2Range(paddr_t start, paddr_t end);
/** MODIFIES: [*] */
void plat_invalidateL2Range(paddr_t start, paddr_t end);
/** MODIFIES: [*] */
void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end);
#endif /* !__ARCH_MACHINE_L2C_310_H */

1
include/arch/arm/armv/armv6/armv/context_switch.h
View file

@ -14,7 +14,6 @@
#include <arch/api/types.h>
#include <mode/model/statedata.h>
/** MODIFIES: [*] */
static inline void setHardwareASID(hw_asid_t hw_asid)
{
dsb();

7
include/arch/arm/armv/armv6/armv/machine.h
View file

@ -11,8 +11,6 @@
#ifndef __ARCH_ARMV6_MACHINE_H
#define __ARCH_ARMV6_MACHINE_H
/** MODIFIES: [*] */
static inline void wfi(void)
{
/*
@ -29,21 +27,16 @@ static inline void wfi(void)
#endif
}
/** MODIFIES: [*] */
static inline void dsb(void)
{
asm volatile("mcr p15, 0, %0, c7, c10, 4" : : "r"(0) : "memory");
}
/** MODIFIES: [*] */
static inline void dmb(void)
{
asm volatile("mcr p15, 0, %0, c7, c10, 5" : : "r"(0) : "memory");
}
/** MODIFIES: [*] */
static inline void isb(void)
{
asm volatile("mcr p15, 0, %0, c7, c5, 4" : : "r"(0) : "memory");

1
include/arch/arm/armv/armv7-a/armv/context_switch.h
View file

@ -15,7 +15,6 @@
#include <arch/api/types.h>
#include <mode/model/statedata.h>
/** MODIFIES: [*] */
static inline void setHardwareASID(hw_asid_t hw_asid)
{
#if defined(CONFIG_ARM_ERRATA_430973)

4
include/arch/arm/armv/armv7-a/armv/machine.h
View file

@ -11,25 +11,21 @@
#ifndef __ARCH_ARMV7A_MACHINE_H
#define __ARCH_ARMV7A_MACHINE_H
/** MODIFIES: [*] */
static inline void wfi(void)
{
asm volatile("wfi" ::: "memory");
}
/** MODIFIES: [*] */
static inline void dsb(void)
{
asm volatile("dsb" ::: "memory");
}
/** MODIFIES: [*] */
static inline void dmb(void)
{
asm volatile("dmb" ::: "memory");
}
/** MODIFIES: [*] */
static inline void isb(void)
{
asm volatile("isb" ::: "memory");

2
include/machine/timer.h
View file

@ -10,9 +10,7 @@
#ifndef __TIMER_H
#define __TIMER_H
/** MODIFIES: [*] */
void resetTimer(void);
/** MODIFIES: [*] */
void initTimer(void);
#endif

4
include/plat/bcm2837/plat/machine.h
View file

@ -146,15 +146,12 @@ handleReservedIRQ(irq_t irq)
}
}
/** MODIFIES: [*] */
interrupt_t
getActiveIRQ(void);
/** MODIFIES: [*] */
void
maskInterrupt(bool_t disable, interrupt_t irq);
/** MODIFIES: [*] */
static inline bool_t
isIRQPending(void)
{
@ -166,7 +163,6 @@ isIRQPending(void)
return pending != 0;
}
/** MODIFIES: [*] */
static inline void
ackInterrupt(UNUSED irq_t irq)
{

4
include/plat/bcm2837/plat/machine/hardware.h
View file

@ -62,14 +62,10 @@ const p_region_t BOOT_RODATA dev_p_regs[] = {
{ /* .start */ TIMER_PADDR , /* .end */ TIMER_PADDR + (1u << PAGE_BITS) },
};
/** MODIFIES: [*] */
void initL2Cache(void);
/** MODIFIES: [*] */
static inline void plat_cleanL2Range(paddr_t start, paddr_t end) {}
/** MODIFIES: [*] */
static inline void plat_invalidateL2Range(paddr_t start, paddr_t end) {}
/** MODIFIES: [*] */
static inline void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
static inline void plat_cleanInvalidateCache(void) {}

3
include/plat/tk1/plat/machine/smmu.h
View file

@ -155,13 +155,10 @@ plat_smmu_get_asid_by_module_id(uint32_t mid)
}
/** MODIFIES: [*] */
int plat_smmu_init(void);
/** MODIFIES: [*] */
void plat_smmu_tlb_flush_all(void);
/** MODIFIES: [*] */
void plat_smmu_ptc_flush_all(void);
iopde_t *plat_smmu_lookup_iopd_by_asid(uint32_t asid);

5
src/arch/arm/armv/armv7-a/cache.c
View file

@ -10,17 +10,16 @@
#include <arch/machine/hardware.h>
/** MODIFIES: [*] */
static inline void invalidateByWSL(word_t wsl)
{
asm volatile("mcr p15, 0, %0, c7, c6, 2" : : "r"(wsl));
}
/** MODIFIES: [*] */
static inline void cleanByWSL(word_t wsl)
{
asm volatile("mcr p15, 0, %0, c7, c10, 2" : : "r"(wsl));
}
/** MODIFIES: [*] */
static inline void cleanInvalidateByWSL(word_t wsl)
{
asm volatile("mcr p15, 0, %0, c7, c14, 2" : : "r"(wsl));

2
src/plat/bcm2837/machine/intc.c
View file

@ -29,7 +29,6 @@ initIRQController(void)
/** MODIFIES: [*] */
interrupt_t
getActiveIRQ(void)
{
@ -74,7 +73,6 @@ getActiveIRQ(void)
return irqInvalid;
}
/** MODIFIES: [*] */
void
maskInterrupt(bool_t disable, interrupt_t irq)
{