gh0s7/mckernel
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add ACSL annotation

Browse Source
This commit is contained in:
Yoichi Umezawa
2016-03-16 15:42:32 +09:00
parent 8dd9f5ef3f
commit 593cf98015
3 changed files with 54 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

28
arch/x86/kernel/cpu.c
View File

@ -1033,6 +1033,10 @@ static void __x86_wakeup(int apicid, unsigned long ip)
/** IHK Functions **/
/*@
@ assigns \nothing;
@ ensures \interrupt_disabled == 0;
@*/
void cpu_halt(void)
{
asm volatile("hlt");
@ -1335,6 +1339,10 @@ void arch_show_extended_context(void)
}
#endif
/*@
@ requires \valid(reg);
@ assigns \nothing;
@*/
void arch_show_interrupt_context(const void *reg)
{
const struct x86_user_context *uctx = reg;
@ -1423,8 +1431,8 @@ int ihk_mc_interrupt_cpu(int cpu, int vector)
}
/*@
@ requires \valid(proc);
@ ensures proc->fp_regs == NULL;
@ requires \valid(thread);
@ ensures thread->fp_regs == NULL;
@*/
void
release_fp_regs(struct thread *thread)
@ -1439,6 +1447,9 @@ release_fp_regs(struct thread *thread)
thread->fp_regs = NULL;
}
/*@
@ requires \valid(thread);
@*/
void
save_fp_regs(struct thread *thread)
{
@ -1470,6 +1481,10 @@ save_fp_regs(struct thread *thread)
}
}
/*@
@ requires \valid(thread);
@ assigns thread->fp_regs;
@*/
void
restore_fp_regs(struct thread *thread)
{
@ -1518,18 +1533,27 @@ ihk_mc_user_context_t *lookup_user_context(struct thread *thread)
return uctx;
} /* lookup_user_context() */
/*@
@ assigns \nothing;
@*/
void init_tick(void)
{
dkprintf("init_tick():\n");
return;
}
/*@
@ assigns \nothing;
@*/
void init_delay(void)
{
dkprintf("init_delay():\n");
return;
}
/*@
@ assigns \nothing;
@*/
void sync_tick(void)
{
dkprintf("sync_tick():\n");

15
arch/x86/kernel/gencore.c
View File

@ -271,6 +271,17 @@ void fill_note(void *note, struct thread *thread, void *regs)
* should be zero.
*/
/*@
@ requires \valid(thread);
@ requires \valid(regs);
@ requires \valid(coretable);
@ requires \valid(chunks);
@ behavior success:
@ ensures \result == 0;
@ assigns coretable;
@ behavior failure:
@ ensures \result == -1;
@*/
int gencore(struct thread *thread, void *regs,
struct coretable **coretable, int *chunks)
{
@ -510,6 +521,10 @@ int gencore(struct thread *thread, void *regs,
* \param coretable An array of core chunks.
*/
/*@
@ requires \valid(coretable);
@ assigns \nothing;
@*/
void freecore(struct coretable **coretable)
{
struct coretable *ct = *coretable;

13
arch/x86/kernel/local.c
View File

@ -38,6 +38,11 @@ void init_processors_local(int max_id)
kprintf("locals = %p\n", locals);
}
/*@
@ requires \valid(id);
@ ensures \result == locals + (LOCALS_SPAN * id);
@ assigns \nothing;
@*/
struct x86_cpu_local_variables *get_x86_cpu_local_variable(int id)
{
return (struct x86_cpu_local_variables *)
@ -98,6 +103,10 @@ void init_boot_processor_local(void)
}
/** IHK **/
/*@
@ ensures \result == %gs;
@ assigns \nothing;
*/
int ihk_mc_get_processor_id(void)
{
int id;
@ -107,6 +116,10 @@ int ihk_mc_get_processor_id(void)
return id;
}
/*@
@ ensures \result == (locals + (LOCALS_SPAN * %gs))->apic_id;
@ assigns \nothing;
*/
int ihk_mc_get_hardware_processor_id(void)
{
struct x86_cpu_local_variables *v = get_x86_this_cpu_local();