frama-c -cpp-command "gcc -E -C -D_EM_WSIZE=4 -D_EM_PSIZE=4 -nostdinc -I/home/virtualbox/Desktop/RSS/Minix/include -I/home/virtualbox/Desktop/RSS/Minix/kernel/arch/i386/include -I." -jessie -jessie-atp alt-ergo -jessie-debug 10 system.c [kernel] preprocessing with "gcc -E -C -D_EM_WSIZE=4 -D_EM_PSIZE=4 -nostdinc -I/home/virtualbox/Desktop/RSS/Minix/include -I/home/virtualbox/Desktop/RSS/Minix/kernel/arch/i386/include -I. -dD system.c" system.c:678:[kernel] warning: Body of function vmrestart_check falls-through. Adding a return statement [jessie] Starting Jessie translation [jessie] Adding default behavior to all functions [kernel] No code for function do_getinfo, default assigns generated [kernel] No code for function kprintf, default assigns generated [kernel] No code for function do_iopenable, default assigns generated [kernel] No code for function do_privctl, default assigns generated [kernel] No code for function do_vmctl, default assigns generated [kernel] No code for function util_stacktrace, default assigns generated [kernel] No code for function minix_panic, default assigns generated [kernel] No code for function isokendpt_f, default assigns generated [kernel] No code for function do_segctl, default assigns generated [kernel] No code for function do_setgrant, default assigns generated [kernel] No code for function do_irqctl, default assigns generated [kernel] No code for function do_readbios, default assigns generated [kernel] No code for function do_unused, default assigns generated [kernel] No code for function do_devio, default assigns generated [kernel] No code for function do_mapdma, default assigns generated [kernel] No code for function do_exec, default assigns generated [kernel] No code for function do_vdevio, default assigns generated [kernel] No code for function do_sprofile, default assigns generated [kernel] No code for function do_fork, default assigns generated [kernel] No code for function sys_call_restart, default assigns generated [kernel] No code for function do_int86, default assigns generated [kernel] No code for function proc_stacktrace, default assigns generated [kernel] No code for function do_cprofile, default assigns generated [kernel] No code for function _receive, default assigns generated [kernel] No code for function do_newmap, default assigns generated [kernel] No code for function do_sdevio, default assigns generated [kernel] No code for function do_profbuf, default assigns generated [kernel] No code for function lock_notify, default assigns generated [kernel] No code for function do_exit, default assigns generated [kernel] No code for function do_kill, default assigns generated [kernel] No code for function data_copy, default assigns generated [kernel] No code for function do_trace, default assigns generated [kernel] No code for function soft_notify, default assigns generated [kernel] No code for function do_getksig, default assigns generated [kernel] No code for function add64u, default assigns generated [kernel] No code for function do_nice, default assigns generated [kernel] No code for function do_endksig, default assigns generated [kernel] No code for function lock_send, default assigns generated [kernel] No code for function do_copy, default assigns generated [kernel] No code for function do_sigsend, default assigns generated [kernel] No code for function lock_enqueue, default assigns generated [kernel] No code for function sigaddset, default assigns generated [kernel] No code for function do_vcopy, default assigns generated [kernel] No code for function do_sigreturn, default assigns generated [kernel] No code for function umap_virtual, default assigns generated [kernel] No code for function verify_grant, default assigns generated [kernel] No code for function lock_dequeue, default assigns generated [kernel] No code for function do_umap, default assigns generated [kernel] No code for function do_times, default assigns generated [kernel] No code for function memcpy, default assigns generated [kernel] No code for function do_memset, default assigns generated [kernel] No code for function do_setalarm, default assigns generated [kernel] No code for function do_vm_setbuf, default assigns generated [kernel] No code for function do_stime, default assigns generated [kernel] No code for function do_sysctl, default assigns generated [kernel] No code for function do_safecopy, default assigns generated [kernel] No code for function do_abort, default assigns generated [kernel] No code for function sigismember, default assigns generated [kernel] No code for function do_vsafecopy, default assigns generated [jessie] Rename entities [jessie] Fill offset/size information in fields [jessie] Replace addrof array with startof [jessie] Replace string constants by global variables [jessie] Put all global initializations in the [globinit] file [jessie] Rewrite type void* and (un)signed char* into char* [jessie] Annotate code with overflow checks /* Generated by Frama-C */ char __string_fell_out_of_switch[19] ; char __string_strange_restart_type[21] ; char __string_SYSTEM__delayed_msgcopy_failed[31] ; char __string_SYSTEM__restart_sys_call_[26] ; char __string_call_number_out_of_range[25] ; char __string_SYSTEM__ignoring_call__d_from_dead__d_[39] ; char __string_SYSTEM__vmrestart_source_doesn_t_match[39] ; char __string_SYSTEM__VMREQUEST_not_set_for_process_on_vmrestart_queue[57] ; char __string_SYSTEM__VMREQUEST_set_for_empty_process[40] ; char __string_softnotify_but_no_p_softnotified[33] ; char __string_dying_proc_was_on_next_soft_notify[35] ; char __string_endpoint__d____s_send_to_dying_dst_ep__d___s__[47] ; char __string_endpoint__d____s_receiving_from_dead_src_ep__d____s_[53] ; char __string_endpoint__d____s_removed_from_queue_at__d_[43] ; char __string_clear_endpoint__clearing_s_asynsize_of__s____d_[48] ; char __string_clear_proc__system_process_died[32] ; char __string_kernel_trace__[15] ; char __string_process__s____d_died__stack__[30] ; char __string_clear_proc__empty_process[26] ; char __string_SYSTEM_umap_grant_umap_virtual_failed__grant__s__d_____s__vir__x_lx_[69] ; char __string_SYSTEM__umap_grant__isokendpt_failed_[38] ; char __string_SYSTEM__umap_grant__verify_grant_failed_[41] ; char __string_Warning__error_in_umap_bios__virtual_address__x_x_[51] ; char __string_cause_sig__PM_gets_signal[26] ; char __string_send_sig_to_empty_process[26] ; char __string_SYS_MAPDMA[11] ; char __string_SYS_SDEVIO[11] ; char __string_SYS_IOPENABLE[14] ; char __string_SYS_READBIOS[13] ; char __string_SYS_INT86[10] ; char __string_SYS_PROFBUF[12] ; char __string_SYS_CPROF[10] ; char __string_SYS_SPROF[10] ; char __string_SYS_SYSCTL[11] ; char __string_SYS_GETINFO[12] ; char __string_SYS_ABORT[10] ; char __string_SYS_STIME[10] ; char __string_SYS_SETALARM[13] ; char __string_SYS_TIMES[10] ; char __string_SYS_VSAFECOPY[14] ; char __string_SYS_SAFECOPYTO[15] ; char __string_SYS_SAFECOPYFROM[17] ; char __string_SYS_PHYSVCOPY[14] ; char __string_SYS_VIRVCOPY[13] ; char __string_SYS_PHYSCOPY[13] ; char __string_SYS_VIRCOPY[12] ; char __string_SYS_UMAP[9] ; char __string_SYS_VMCTL[10] ; char __string_SYS_VM_SETBUF[14] ; char __string_SYS_MEMSET[11] ; char __string_SYS_SEGCTL[11] ; char __string_SYS_NEWMAP[11] ; char __string_SYS_VDEVIO[11] ; char __string_SYS_DEVIO[10] ; char __string_SYS_IRQCTL[11] ; char __string_SYS_SIGRETURN[14] ; char __string_SYS_SIGSEND[12] ; char __string_SYS_ENDKSIG[12] ; char __string_SYS_GETKSIG[12] ; char __string_SYS_KILL[9] ; char __string_SYS_SETGRANT[13] ; char __string_SYS_TRACE[10] ; char __string_SYS_PRIVCTL[12] ; char __string_SYS_NICE[9] ; char __string_SYS_EXIT[9] ; char __string_SYS_EXEC[9] ; char __string_SYS_FORK[9] ; char __string_unused[7] ; char __string_SYSTEM__reply_to__d_failed___d_[32] ; char __string_SYSTEM__not_replying_to__d__not_ready_[39] ; char __string_SYSTEM__illegal_request__d_from__d__[37] ; char __string_sys_task__no_debug_output_for_a_while_[39] ; char __string_SYSTEM__request__d_from__d_denied__[36] ; char __string_system_c[9] ; char __string_softnotify_non_NULL_after_receive[34] ; char __string_receive___failed[17] ; char __string_softnotify_non_NULL_before_receive__2_[39] ; char __string_softnotify_non_NULL_before_receive__1_[39] ; /*@ behavior default: assigns \nothing; */ void free(char *ptr ) ; /*@ behavior default: assigns \nothing; */ char *malloc(unsigned int size ) ; typedef unsigned int size_t; typedef long clock_t; typedef unsigned long sigset_t; typedef unsigned short bitchunk_t; typedef unsigned char u8_t; typedef unsigned short u16_t; typedef unsigned long u32_t; typedef long i32_t; struct __anonstruct_u64_t_1 { u32_t [2] ; }; typedef struct __anonstruct_u64_t_1 u64_t; typedef unsigned int vir_clicks; typedef unsigned long phys_bytes; typedef unsigned int phys_clicks; typedef int endpoint_t; typedef unsigned long vir_bytes; struct mem_map { vir_clicks mem_vir ; phys_clicks mem_phys ; vir_clicks mem_len ; }; struct far_mem { int in_use ; phys_clicks mem_phys_0 ; vir_clicks mem_len_0 ; }; struct io_range { unsigned int ior_base ; unsigned int ior_limit ; }; struct mem_range { phys_bytes mr_base ; phys_bytes mr_limit ; }; struct __anonstruct_mess_1_4 { int m1i1 ; int m1i2 ; int m1i3 ; char *m1p1 ; char *m1p2 ; char *m1p3 ; }; typedef struct __anonstruct_mess_1_4 mess_1; struct __anonstruct_mess_2_5 { int m2i1 ; int m2i2 ; int m2i3 ; long m2l1 ; long m2l2 ; char *m2p1 ; short m2s1 ; }; typedef struct __anonstruct_mess_2_5 mess_2; struct __anonstruct_mess_3_6 { int m3i1 ; int m3i2 ; char *m3p1 ; char m3ca1[14] ; }; typedef struct __anonstruct_mess_3_6 mess_3; struct __anonstruct_mess_4_7 { long m4l1 ; long m4l2 ; long m4l3 ; long m4l4 ; long m4l5 ; }; typedef struct __anonstruct_mess_4_7 mess_4; struct __anonstruct_mess_5_8 { short m5c1 ; short m5c2 ; int m5i1 ; int m5i2 ; long m5l1 ; long m5l2 ; long m5l3 ; }; typedef struct __anonstruct_mess_5_8 mess_5; struct __anonstruct_mess_6_9 { long m6l1 ; long m6l2 ; long m6l3 ; short m6s1 ; short m6s2 ; short m6s3 ; char m6c1 ; char m6c2 ; char *m6p1 ; char *m6p2 ; }; typedef struct __anonstruct_mess_6_9 mess_6; struct __anonstruct_mess_7_10 { int m7i1 ; int m7i2 ; int m7i3 ; int m7i4 ; char *m7p1 ; char *m7p2 ; }; typedef struct __anonstruct_mess_7_10 mess_7; struct __anonstruct_mess_8_11 { int m8i1 ; int m8i2 ; char *m8p1 ; char *m8p2 ; char *m8p3 ; char *m8p4 ; }; typedef struct __anonstruct_mess_8_11 mess_8; struct __anonstruct_mess_9_12 { long m9l1 ; long m9l2 ; long m9l3 ; long m9l4 ; long m9l5 ; short m9s1 ; short m9s2 ; short m9s3 ; char m9c1 ; char m9c2 ; }; typedef struct __anonstruct_mess_9_12 mess_9; union __anonunion_m_u_14 { mess_1 m_m1 ; mess_2 m_m2 ; mess_3 m_m3 ; mess_4 m_m4 ; mess_5 m_m5 ; mess_7 m_m7 ; mess_8 m_m8 ; mess_6 m_m6 ; mess_9 m_m9 ; }; struct __anonstruct_message_13 { endpoint_t m_source ; int m_type ; union __anonunion_m_u_14 m_u ; }; typedef struct __anonstruct_message_13 message; struct timer; union __anonunion_tmr_arg_t_15 { int ta_int ; long ta_long ; char *ta_ptr ; }; typedef union __anonunion_tmr_arg_t_15 tmr_arg_t; struct timer { struct timer *tmr_next ; clock_t tmr_exp_time ; void (*tmr_func)(struct timer *tp ) ; tmr_arg_t tmr_arg ; }; typedef struct timer timer_t; typedef int proc_nr_t; typedef short sys_id_t; struct __anonstruct_sys_map_t_16 { bitchunk_t chunk[2U] ; }; typedef struct __anonstruct_sys_map_t_16 sys_map_t; typedef unsigned long irq_policy_t; typedef unsigned long irq_id_t; struct irq_hook { struct irq_hook *next ; int (*handler)(struct irq_hook * ) ; int irq ; int id_1 ; int proc_nr_e ; irq_id_t notify_id ; irq_policy_t policy ; }; typedef struct irq_hook irq_hook_t; typedef i32_t int32_t; typedef int32_t cp_grant_id_t; typedef unsigned int reg_t; struct stackframe_s { u16_t gs ; u16_t fs ; u16_t es ; u16_t ds ; reg_t di ; reg_t si ; reg_t fp ; reg_t st ; reg_t bx ; reg_t dx ; reg_t cx ; reg_t retreg ; reg_t retadr ; reg_t pc ; reg_t cs ; reg_t psw ; reg_t sp ; reg_t ss ; }; struct segdesc_s { u16_t limit_low ; u16_t base_low ; u8_t base_middle ; u8_t access ; u8_t granularity ; u8_t base_high ; }; struct segframe { reg_t p_ldt_sel ; reg_t p_cr3 ; struct segdesc_s p_ldt[5] ; }; struct pagefault { u32_t pf_virtual ; u32_t pf_flags ; }; struct proc_1; struct system_stats { unsigned long bad_req ; unsigned long not_allowed ; u64_t total ; }; struct sprof_info_s { int mem_used ; int total_samples ; int idle_samples ; int system_samples ; int user_samples ; }; struct __anonstruct_sprof_sample_22 { char name[8] ; int pc_0 ; }; struct cprof_info_s { int mem_used_0 ; int err ; }; struct cprof_ctl_s { int reset ; int slots_used ; int err_0 ; }; struct cprof_tbl_s { struct cprof_tbl_s *next_0 ; char cpath[256] ; int calls ; u64_t cycles ; }; struct priv_0 { proc_nr_t s_proc_nr ; sys_id_t s_id ; short s_flags ; vir_bytes s_asyntab ; size_t s_asynsize ; short s_trap_mask ; sys_map_t s_ipc_to ; bitchunk_t s_k_call_mask[3U] ; sys_map_t s_notify_pending ; irq_id_t s_int_pending ; sigset_t s_sig_pending ; timer_t s_alarm_timer ; struct far_mem s_farmem[3] ; reg_t *s_stack_guard ; int s_nr_io_range ; struct io_range s_io_tab[32] ; int s_nr_mem_range ; struct mem_range s_mem_tab[10] ; int s_nr_irq ; int s_irq_tab[4] ; vir_bytes s_grant_table ; int s_grant_entries ; }; struct __anonstruct_sys_call_25 { int call_nr ; message *m_ptr_40 ; int src_dst_e ; long bit_map ; }; struct __anonstruct_msgcopy_26 { struct proc_1 *dst_2 ; vir_bytes dst_v ; message msgbuf ; }; union __anonunion_saved_24 { message reqmsg ; struct __anonstruct_sys_call_25 sys_call ; struct __anonstruct_msgcopy_26 msgcopy ; }; struct __anonstruct_p_vmrequest_23 { struct proc_1 *nextrestart ; struct proc_1 *nextrequestor ; int type_0 ; union __anonunion_saved_24 saved ; vir_bytes start ; vir_bytes length ; u8_t writeflag ; endpoint_t who ; int vmresult ; struct proc_1 *requestor ; }; struct proc_1 { struct stackframe_s p_reg ; struct segframe p_seg ; proc_nr_t p_nr ; struct priv_0 *p_priv ; short p_rts_flags ; short p_misc_flags ; char p_priority ; char p_max_priority ; char p_ticks_left ; char p_quantum_size ; struct mem_map p_memmap[3] ; struct pagefault p_pagefault ; struct proc_1 *p_nextpagefault ; clock_t p_user_time ; clock_t p_sys_time ; struct proc_1 *p_nextready ; struct proc_1 *p_caller_q ; struct proc_1 *p_q_link ; message *p_messbuf ; int p_getfrom_e ; int p_sendto_e ; sigset_t p_pending ; char p_name[8] ; endpoint_t p_endpoint ; struct __anonstruct_p_vmrequest_23 p_vmrequest ; struct proc_1 *next_soft_notify ; int p_softnotified ; }; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_16, src; assigns *m_ptr_16 \from *m_ptr_16, src; */ extern int _receive(endpoint_t src , message *m_ptr_16 ) ; /*@ behavior default: assigns \at(\result,Post) \from *fmt; */ extern int kprintf(char const *fmt , ...) ; /*@ behavior default: assigns *s \from *s, n; */ extern void minix_panic(char *s , int n ) ; /*@ behavior default: assigns *caller \from *caller; */ extern void sys_call_restart(struct proc_1 *caller ) ; /*@ behavior default: assigns \at(\result,Post) \from src_0, dst; */ extern int lock_notify(int src_0 , int dst ) ; /*@ behavior default: assigns \at(\result,Post) \from dst_0; */ extern int soft_notify(int dst_0 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_26, dst_1; assigns *m_ptr_26 \from *m_ptr_26, dst_1; */ extern int lock_send(int dst_1 , message *m_ptr_26 ) ; /*@ behavior default: assigns *rp_1 \from *rp_1; */ extern void lock_enqueue(struct proc_1 *rp_1 ) ; /*@ behavior default: assigns *rp_4 \from *rp_4; */ extern void lock_dequeue(struct proc_1 *rp_4 ) ; /*@ behavior default: assigns \at(\result,Post) \from *file, *p, line, e, f; assigns *file \from *file, *p, line, e, f; assigns *p \from *file, *p, line, e, f; */ extern int isokendpt_f(char *file , int line , endpoint_t e , int *p , int f ) ; int get_priv(struct proc_1 *rc_0 , int proc_type ) ; void set_sendto_bit(struct proc_1 *rp_0 , int id ) ; void unset_sendto_bit(struct proc_1 *rp_2 , int id_0 ) ; void send_sig(int proc_nr , int sig_nr ) ; void cause_sig(int proc_nr_0 , int sig_nr_0 ) ; void sys_task(void) ; phys_bytes umap_grant(struct proc_1 *rp , cp_grant_id_t grant , vir_bytes bytes ) ; void clear_endpoint(struct proc_1 *rc ) ; phys_bytes umap_bios(vir_bytes vir_addr , vir_bytes bytes_1 ) ; phys_bytes umap_verify_grant(struct proc_1 *rp_5 , endpoint_t grantee , cp_grant_id_t grant_0 , vir_bytes offset , vir_bytes bytes_3 , int access_0 ) ; /*@ behavior default: assigns \at(\result,Post) \from \nothing; */ extern int verify_grant(endpoint_t , endpoint_t , cp_grant_id_t , vir_bytes , int , vir_bytes , vir_bytes * , endpoint_t * ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_0_0; assigns *m_0_0 \from *m_0_0; */ extern int do_sysctl(message *m_0_0 ) ; /*@ behavior default: assigns \at(\result,Post) \from from, from_addr, to, to_addr, bytes_0; */ extern int data_copy(endpoint_t from , vir_bytes from_addr , endpoint_t to , vir_bytes to_addr , size_t bytes_0 ) ; /*@ behavior default: assigns \at(\result,Post) \from *rp_3, seg, vir_addr_0, bytes_2; assigns *rp_3 \from *rp_3, seg, vir_addr_0, bytes_2; */ extern phys_bytes umap_virtual(struct proc_1 *rp_3 , int seg , vir_bytes vir_addr_0 , vir_bytes bytes_2 ) ; /*@ behavior default: assigns *proc_0 \from *proc_0; */ extern void proc_stacktrace(struct proc_1 *proc_0 ) ; /*@ behavior default: assigns \nothing; */ extern void util_stacktrace(void) ; extern struct proc_1 *vmrestart ; extern struct proc_1 *softnotify ; extern irq_hook_t irq_hooks[16] ; extern endpoint_t ipc_stats_target ; extern struct system_stats sys_stats ; extern endpoint_t who_e ; extern int who_p ; extern int sys_call_code ; struct sprof_info_s sprof_info_inst ; struct __anonstruct_sprof_sample_22 sprof_sample ; struct cprof_info_s cprof_info_inst ; struct cprof_ctl_s cprof_ctl_inst ; struct cprof_tbl_s cprof_tbl_inst ; extern struct priv_0 priv[32] ; extern struct priv_0 *ppriv_addr[32] ; extern struct proc_1 proc[104] ; extern struct proc_1 *pproc_addr[104] ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_7; assigns *m_ptr_7 \from *m_ptr_7; */ extern int do_unused(message *m_ptr_7 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_10; assigns *m_ptr_10 \from *m_ptr_10; */ extern int do_exec(message *m_ptr_10 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_13; assigns *m_ptr_13 \from *m_ptr_13; */ extern int do_fork(message *m_ptr_13 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_17; assigns *m_ptr_17 \from *m_ptr_17; */ extern int do_newmap(message *m_ptr_17 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_20; assigns *m_ptr_20 \from *m_ptr_20; */ extern int do_exit(message *m_ptr_20 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_22; assigns *m_ptr_22 \from *m_ptr_22; */ extern int do_trace(message *m_ptr_22 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_24; assigns *m_ptr_24 \from *m_ptr_24; */ extern int do_nice(message *m_ptr_24 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_27; assigns *m_ptr_27 \from *m_ptr_27; */ extern int do_copy(message *m_ptr_27 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_29; assigns *m_ptr_29 \from *m_ptr_29; */ extern int do_vcopy(message *m_ptr_29 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_31; assigns *m_ptr_31 \from *m_ptr_31; */ extern int do_umap(message *m_ptr_31 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_33; assigns *m_ptr_33 \from *m_ptr_33; */ extern int do_memset(message *m_ptr_33 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_35; assigns *m_ptr_35 \from *m_ptr_35; */ extern int do_vm_setbuf(message *m_ptr_35 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_38; assigns *m_ptr_38 \from *m_ptr_38; */ extern int do_abort(message *m_ptr_38 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr; assigns *m_ptr \from *m_ptr; */ extern int do_getinfo(message *m_ptr ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_1; assigns *m_ptr_1 \from *m_ptr_1; */ extern int do_privctl(message *m_ptr_1 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_3; assigns *m_ptr_3 \from *m_ptr_3; */ extern int do_segctl(message *m_ptr_3 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_5; assigns *m_ptr_5 \from *m_ptr_5; */ extern int do_irqctl(message *m_ptr_5 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_8; assigns *m_ptr_8 \from *m_ptr_8; */ extern int do_devio(message *m_ptr_8 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_11; assigns *m_ptr_11 \from *m_ptr_11; */ extern int do_vdevio(message *m_ptr_11 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_14; assigns *m_ptr_14 \from *m_ptr_14; */ extern int do_int86(message *m_ptr_14 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_18; assigns *m_ptr_18 \from *m_ptr_18; */ extern int do_sdevio(message *m_ptr_18 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_21; assigns *m_ptr_21 \from *m_ptr_21; */ extern int do_kill(message *m_ptr_21 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_23; assigns *m_ptr_23 \from *m_ptr_23; */ extern int do_getksig(message *m_ptr_23 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_25; assigns *m_ptr_25 \from *m_ptr_25; */ extern int do_endksig(message *m_ptr_25 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_28; assigns *m_ptr_28 \from *m_ptr_28; */ extern int do_sigsend(message *m_ptr_28 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_30; assigns *m_ptr_30 \from *m_ptr_30; */ extern int do_sigreturn(message *m_ptr_30 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_32; assigns *m_ptr_32 \from *m_ptr_32; */ extern int do_times(message *m_ptr_32 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_34; assigns *m_ptr_34 \from *m_ptr_34; */ extern int do_setalarm(message *m_ptr_34 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_36; assigns *m_ptr_36 \from *m_ptr_36; */ extern int do_stime(message *m_ptr_36 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_37; assigns *m_ptr_37 \from *m_ptr_37; */ extern int do_safecopy(message *m_ptr_37 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_39; assigns *m_ptr_39 \from *m_ptr_39; */ extern int do_vsafecopy(message *m_ptr_39 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_0; assigns *m_ptr_0 \from *m_ptr_0; */ extern int do_iopenable(message *m_ptr_0 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_2; assigns *m_ptr_2 \from *m_ptr_2; */ extern int do_vmctl(message *m_ptr_2 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_4; assigns *m_ptr_4 \from *m_ptr_4; */ extern int do_setgrant(message *m_ptr_4 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_6; assigns *m_ptr_6 \from *m_ptr_6; */ extern int do_readbios(message *m_ptr_6 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_9; assigns *m_ptr_9 \from *m_ptr_9; */ extern int do_mapdma(message *m_ptr_9 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_12; assigns *m_ptr_12 \from *m_ptr_12; */ extern int do_sprofile(message *m_ptr_12 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_15; assigns *m_ptr_15 \from *m_ptr_15; */ extern int do_cprofile(message *m_ptr_15 ) ; /*@ behavior default: assigns \at(\result,Post) \from *m_ptr_19; assigns *m_ptr_19 \from *m_ptr_19; */ extern int do_profbuf(message *m_ptr_19 ) ; /*@ behavior default: assigns \at(\result,Post) \from *_set, _sig; assigns *_set \from *_set, _sig; */ extern int sigaddset(sigset_t *_set , int _sig ) ; /*@ behavior default: assigns \at(\result,Post) \from *_set_0, _sig_0; */ extern int sigismember(sigset_t const *_set_0 , int _sig_0 ) ; /*@ behavior default: assigns \at(\result,Post) \from _n; */ extern char *memcpy(char *_s1 , char *_s2 , size_t _n ) ; /*@ behavior default: assigns \at(\result,Post) \from i, j; */ extern u64_t add64u(u64_t i , unsigned int j ) ; int (*call_vec[45])(message *m_ptr ) ; char *callnames[45] ; static void initialize(void) ; static void softnotify_check(void) ; static struct proc_1 *vmrestart_check(message *m_0 ) ; static message m ; static int curr ; static int limit ; static int extra ; /*@ behavior default: */ void sys_task(void) { register int result ; register struct proc_1 *caller_ptr ; int s_0 ; int call_nr_0 ; int n_0 ; struct proc_1 *restarting ; int r ; int rts ; n_0 = 0; initialize(); while (1) { restarting = vmrestart_check(& m); softnotify_check(); if (softnotify) { minix_panic((char *)(__string_softnotify_non_NULL_before_receive__1_), 32768); } if (! restarting) { if (softnotify) { minix_panic((char *)(__string_softnotify_non_NULL_before_receive__2_), 32768); } r = _receive(31438,& m); if (r != 0) { minix_panic((char *)(__string_receive___failed),r); } if (m.m_source == -2) { goto __Cont; } if (softnotify) { minix_panic((char *)(__string_softnotify_non_NULL_after_receive), 32768); } } sys_call_code = (int )((unsigned int )m.m_type); call_nr_0 = sys_call_code - 1536; who_e = m.m_source; isokendpt_f((char *)(__string_system_c),104,who_e,& who_p,1); caller_ptr = *((pproc_addr + 4) + who_p); if (caller_ptr->p_endpoint == ipc_stats_target) { sys_stats.total = add64u(sys_stats.total,1U); } if (call_nr_0 < 0) { goto _LOR; } else { if (call_nr_0 >= 45) { goto _LOR; } else { /*@ assert ((unsigned int )call_nr_0%16U ≥ 0); // synthesized assert ((unsigned int )call_nr_0%16U < 32); // synthesized assert (1 ≤ 2147483647>>(unsigned int )call_nr_0%16U); // synthesized */ if (! ((int )(caller_ptr->p_priv)->s_k_call_mask[(unsigned int )call_nr_0 / 16U] & ( 1 << (unsigned int )call_nr_0 % 16U))) { if (curr < limit + extra) { kprintf(__string_SYSTEM__request__d_from__d_denied__,call_nr_0, m.m_source); } else { if (curr == limit + extra) { kprintf(__string_sys_task__no_debug_output_for_a_while_); } else { if (curr == 2 * limit - 1) { limit *= 2; } } } curr ++; if (caller_ptr->p_endpoint == ipc_stats_target) { (sys_stats.not_allowed) ++; } result = -104; } else { result = (*(call_vec[call_nr_0]))(& m); } } } goto _LOR_0; _LOR: /* internal */ kprintf(__string_SYSTEM__illegal_request__d_from__d__, call_nr_0,m.m_source); if (caller_ptr->p_endpoint == ipc_stats_target) { (sys_stats.bad_req) ++; } result = -107; _LOR_0: /* internal */ ; if (result == -996) { memcpy((char *)(& caller_ptr->p_vmrequest.saved.reqmsg),(char *)(& m), 36U); caller_ptr->p_vmrequest.type_0 = 1; } else { if (result != -201) { if (restarting) { while (1) { rts = (int )restarting->p_rts_flags; restarting->p_rts_flags = (short )((int )restarting->p_rts_flags & -2049); if (rts) { if (! restarting->p_rts_flags) { lock_enqueue(restarting); } } goto while_1_break; } while_1_break: /* internal */ ; } m.m_type = result; if (((int )caller_ptr->p_rts_flags & 8) == 8) { if (! (((int )caller_ptr->p_rts_flags & 4) == 4)) { if (caller_ptr->p_getfrom_e == 31438) { goto _LOR_1; } else { if (caller_ptr->p_getfrom_e == -2) { goto _LOR_1; } else { kprintf(__string_SYSTEM__not_replying_to__d__not_ready_, caller_ptr->p_endpoint); } } goto _LOR_2; _LOR_1: /* internal */ s_0 = lock_send(m.m_source,& m); if (0 != s_0) { kprintf(__string_SYSTEM__reply_to__d_failed___d_,m.m_source, s_0); } _LOR_2: /* internal */ ; } else { kprintf(__string_SYSTEM__not_replying_to__d__not_ready_, caller_ptr->p_endpoint); } } else { kprintf(__string_SYSTEM__not_replying_to__d__not_ready_, caller_ptr->p_endpoint); } } } __Cont: /* internal */ ; } return; } /*@ behavior default: */ static void initialize(void) { register struct priv_0 *sp_0 ; int i_0 ; i_0 = 0; while (1) { if (! (i_0 < 16)) { goto while_2_break; } irq_hooks[i_0].proc_nr_e = 27342; i_0 ++; } while_2_break: /* internal */ ; sp_0 = priv; while (1) { if (! (sp_0 < & priv[32])) { goto while_3_break; } sp_0->s_alarm_timer.tmr_exp_time = 2147483647L; sp_0->s_alarm_timer.tmr_next = (struct timer *)((char *)0); sp_0 ++; } while_3_break: /* internal */ ; i_0 = 0; while (1) { if (! (i_0 < 45)) { goto while_4_break; } call_vec[i_0] = & do_unused; callnames[i_0] = (char *)(__string_unused); i_0 ++; } while_4_break: /* internal */ ; callnames[0] = (char *)(__string_SYS_FORK); call_vec[0] = & do_fork; callnames[1] = (char *)(__string_SYS_EXEC); call_vec[1] = & do_exec; callnames[2] = (char *)(__string_SYS_EXIT); call_vec[2] = & do_exit; callnames[3] = (char *)(__string_SYS_NICE); call_vec[3] = & do_nice; callnames[4] = (char *)(__string_SYS_PRIVCTL); call_vec[4] = & do_privctl; callnames[5] = (char *)(__string_SYS_TRACE); call_vec[5] = & do_trace; callnames[34] = (char *)(__string_SYS_SETGRANT); call_vec[34] = & do_setgrant; callnames[6] = (char *)(__string_SYS_KILL); call_vec[6] = & do_kill; callnames[7] = (char *)(__string_SYS_GETKSIG); call_vec[7] = & do_getksig; callnames[8] = (char *)(__string_SYS_ENDKSIG); call_vec[8] = & do_endksig; callnames[9] = (char *)(__string_SYS_SIGSEND); call_vec[9] = & do_sigsend; callnames[10] = (char *)(__string_SYS_SIGRETURN); call_vec[10] = & do_sigreturn; callnames[19] = (char *)(__string_SYS_IRQCTL); call_vec[19] = & do_irqctl; callnames[21] = (char *)(__string_SYS_DEVIO); call_vec[21] = & do_devio; callnames[23] = (char *)(__string_SYS_VDEVIO); call_vec[23] = & do_vdevio; callnames[11] = (char *)(__string_SYS_NEWMAP); call_vec[11] = & do_newmap; callnames[12] = (char *)(__string_SYS_SEGCTL); call_vec[12] = & do_segctl; callnames[13] = (char *)(__string_SYS_MEMSET); call_vec[13] = & do_memset; callnames[29] = (char *)(__string_SYS_VM_SETBUF); call_vec[29] = & do_vm_setbuf; callnames[43] = (char *)(__string_SYS_VMCTL); call_vec[43] = & do_vmctl; callnames[14] = (char *)(__string_SYS_UMAP); call_vec[14] = & do_umap; callnames[15] = (char *)(__string_SYS_VIRCOPY); call_vec[15] = & do_copy; callnames[16] = (char *)(__string_SYS_PHYSCOPY); call_vec[16] = & do_copy; callnames[17] = (char *)(__string_SYS_VIRVCOPY); call_vec[17] = & do_vcopy; callnames[18] = (char *)(__string_SYS_PHYSVCOPY); call_vec[18] = & do_vcopy; callnames[31] = (char *)(__string_SYS_SAFECOPYFROM); call_vec[31] = & do_safecopy; callnames[32] = (char *)(__string_SYS_SAFECOPYTO); call_vec[32] = & do_safecopy; callnames[33] = (char *)(__string_SYS_VSAFECOPY); call_vec[33] = & do_vsafecopy; callnames[25] = (char *)(__string_SYS_TIMES); call_vec[25] = & do_times; callnames[24] = (char *)(__string_SYS_SETALARM); call_vec[24] = & do_setalarm; callnames[39] = (char *)(__string_SYS_STIME); call_vec[39] = & do_stime; callnames[27] = (char *)(__string_SYS_ABORT); call_vec[27] = & do_abort; callnames[26] = (char *)(__string_SYS_GETINFO); call_vec[26] = & do_getinfo; callnames[44] = (char *)(__string_SYS_SYSCTL); call_vec[44] = & do_sysctl; callnames[36] = (char *)(__string_SYS_SPROF); call_vec[36] = & do_sprofile; callnames[37] = (char *)(__string_SYS_CPROF); call_vec[37] = & do_cprofile; callnames[38] = (char *)(__string_SYS_PROFBUF); call_vec[38] = & do_profbuf; callnames[20] = (char *)(__string_SYS_INT86); call_vec[20] = & do_int86; callnames[35] = (char *)(__string_SYS_READBIOS); call_vec[35] = & do_readbios; callnames[28] = (char *)(__string_SYS_IOPENABLE); call_vec[28] = & do_iopenable; callnames[22] = (char *)(__string_SYS_SDEVIO); call_vec[22] = & do_sdevio; callnames[42] = (char *)(__string_SYS_MAPDMA); call_vec[42] = & do_mapdma; return; } /*@ behavior default: */ int get_priv(struct proc_1 *rc_0 , int proc_type ) { register struct priv_0 *sp_1 ; int __retres ; if (proc_type == 16) { sp_1 = priv; while (1) { if (! (sp_1 < & priv[32])) { goto while_5_break; } if (sp_1->s_proc_nr == 27342) { if ((int )sp_1->s_id != 0) { goto while_5_break; } } sp_1 ++; } while_5_break: /* internal */ ; if (sp_1 >= & priv[32]) { __retres = -28; goto return_label; } rc_0->p_priv = sp_1; (rc_0->p_priv)->s_proc_nr = rc_0->p_nr; (rc_0->p_priv)->s_flags = (short)16; sp_1->s_asyntab = 4294967295UL; sp_1->s_asynsize = 0U; } else { rc_0->p_priv = priv; (rc_0->p_priv)->s_proc_nr = 9; } __retres = 0; return_label: /* internal */ return (__retres); } /*@ behavior default: */ void set_sendto_bit(struct proc_1 *rp_0 , int id ) { struct proc_1 *rrp ; if ((ppriv_addr[id])->s_proc_nr == 27342) { goto return_label; } else { if ((int )(rp_0->p_priv)->s_id == id) { goto return_label; } } /*@ assert ((unsigned int )id%16U ≥ 0); // synthesized assert ((unsigned int )id%16U < 32); // synthesized assert (1 ≤ 2147483647>>(unsigned int )id%16U); // synthesized */ (rp_0->p_priv)->s_ipc_to.chunk[(unsigned int )id / 16U] = (unsigned short )( (int )(rp_0->p_priv)->s_ipc_to.chunk[(unsigned int )id / 16U] | (1 << (unsigned int )id % 16U)); rrp = *((pproc_addr + 4) + (ppriv_addr[id])->s_proc_nr); if (! (rrp->p_nr < 0)) { /*@ assert ((unsigned int )(rp_0->p_priv)->s_id%16U ≥ 0); // synthesized assert ((unsigned int )(rp_0->p_priv)->s_id%16U < 32); // synthesized assert (1 ≤ 2147483647>>(unsigned int )(rp_0->p_priv)->s_id%16U); // synthesized */ (rrp->p_priv)->s_ipc_to.chunk[(unsigned int )(rp_0->p_priv)->s_id / 16U] = (unsigned short )( (int )(rrp->p_priv)->s_ipc_to.chunk[(unsigned int )(rp_0->p_priv)->s_id / 16U] | ( 1 << (unsigned int )(rp_0->p_priv)->s_id % 16U)); } return_label: /* internal */ return; } /*@ behavior default: */ void unset_sendto_bit(struct proc_1 *rp_2 , int id_0 ) { /*@ assert ((unsigned int )id_0%16U ≥ 0); // synthesized assert ((unsigned int )id_0%16U < 32); // synthesized assert (1 ≤ 2147483647>>(unsigned int )id_0%16U); // synthesized */ (rp_2->p_priv)->s_ipc_to.chunk[(unsigned int )id_0 / 16U] = (unsigned short )( (int )(rp_2->p_priv)->s_ipc_to.chunk[(unsigned int )id_0 / 16U] & ~ ( 1 << (unsigned int )id_0 % 16U)); /*@ assert ((unsigned int )(rp_2->p_priv)->s_id%16U ≥ 0); // synthesized assert ((unsigned int )(rp_2->p_priv)->s_id%16U < 32); // synthesized assert (1 ≤ 2147483647>>(unsigned int )(rp_2->p_priv)->s_id%16U); // synthesized */ (ppriv_addr[id_0])->s_ipc_to.chunk[(unsigned int )(rp_2->p_priv)->s_id / 16U] = (unsigned short )( (int )(ppriv_addr[id_0])->s_ipc_to.chunk[(unsigned int )(rp_2->p_priv)->s_id / 16U] & ~ ( 1 << (unsigned int )(rp_2->p_priv)->s_id % 16U)); return; } /*@ behavior default: */ void send_sig(int proc_nr , int sig_nr ) { register struct proc_1 *rp_6 ; if (! ((unsigned int )(proc_nr + 4) < 104U)) { minix_panic((char *)(__string_send_sig_to_empty_process),proc_nr); } else { if ((int )(*((pproc_addr + 4) + proc_nr))->p_rts_flags == 1) { minix_panic((char *)(__string_send_sig_to_empty_process),proc_nr); } } rp_6 = *((pproc_addr + 4) + proc_nr); sigaddset(& (rp_6->p_priv)->s_sig_pending,sig_nr); soft_notify(rp_6->p_endpoint); return; } /*@ behavior default: */ void cause_sig(int proc_nr_0 , int sig_nr_0 ) { register struct proc_1 *rp_7 ; int tmp ; if (proc_nr_0 == 0) { minix_panic((char *)(__string_cause_sig__PM_gets_signal),32768); } rp_7 = *((pproc_addr + 4) + proc_nr_0); tmp = sigismember((sigset_t const *)(& rp_7->p_pending),sig_nr_0); if (! tmp) { sigaddset(& rp_7->p_pending,sig_nr_0); if (! (((int )rp_7->p_rts_flags & 16) == 16)) { while (1) { if (! rp_7->p_rts_flags) { lock_dequeue(rp_7); } rp_7->p_rts_flags = (short )((int )rp_7->p_rts_flags | 48); goto while_6_break; } while_6_break: /* internal */ ; send_sig(0,30); } } return; } /*@ behavior default: */ phys_bytes umap_bios(vir_bytes vir_addr , vir_bytes bytes_1 ) { phys_bytes __retres_0 ; if (vir_addr >= 0UL) { if (vir_addr + bytes_1 <= 1279UL) { __retres_0 = vir_addr; goto return_label; } else { goto _LAND; } } else { goto _LAND; } goto _LAND_0; _LAND: /* internal */ ; if (vir_addr >= 589824UL) { if (vir_addr + bytes_1 <= 1048575UL) { __retres_0 = vir_addr; goto return_label; } } _LAND_0: /* internal */ ; kprintf(__string_Warning__error_in_umap_bios__virtual_address__x_x_, vir_addr); __retres_0 = 0UL; return_label: /* internal */ return (__retres_0); } /*@ behavior default: */ phys_bytes umap_grant(struct proc_1 *rp , cp_grant_id_t grant , vir_bytes bytes ) { int proc_nr_1 ; vir_bytes offset_0 ; vir_bytes ret ; endpoint_t granter ; int tmp_0 ; int tmp_0_0 ; phys_bytes __retres_1 ; tmp_0 = verify_grant(rp->p_endpoint,31438,grant,bytes,0,0UL,& offset_0, & granter); if (tmp_0 != 0) { kprintf(__string_SYSTEM__umap_grant__verify_grant_failed_); __retres_1 = 0UL; goto return_label; } tmp_0_0 = isokendpt_f((char *)(__string_system_c),442,granter,& proc_nr_1, 0); if (! tmp_0_0) { kprintf(__string_SYSTEM__umap_grant__isokendpt_failed_); __retres_1 = 0UL; goto return_label; } ret = umap_virtual(*((pproc_addr + 4) + proc_nr_1),1,offset_0,bytes); if (! ret) { kprintf(__string_SYSTEM_umap_grant_umap_virtual_failed__grant__s__d_____s__vir__x_lx_, rp->p_name,grant,(*((pproc_addr + 4) + proc_nr_1))->p_name, offset_0); } __retres_1 = ret; return_label: /* internal */ return (__retres_1); } /*@ behavior default: */ void clear_endpoint(struct proc_1 *rc ) { register struct proc_1 *rp_8 ; register struct proc_1 **xpp ; struct proc_1 *np ; int target_proc ; int rts_0 ; int rts_0_0 ; if ((int )rc->p_rts_flags == 1) { minix_panic((char *)(__string_clear_proc__empty_process),rc->p_endpoint); } if (rc->p_endpoint == 0) { kprintf(__string_process__s____d_died__stack__,rc->p_name,rc->p_endpoint); proc_stacktrace(rc); kprintf(__string_kernel_trace__); util_stacktrace(); minix_panic((char *)(__string_clear_proc__system_process_died), rc->p_endpoint); } else { if (rc->p_endpoint == 1) { kprintf(__string_process__s____d_died__stack__,rc->p_name, rc->p_endpoint); proc_stacktrace(rc); kprintf(__string_kernel_trace__); util_stacktrace(); minix_panic((char *)(__string_clear_proc__system_process_died), rc->p_endpoint); } } while (1) { if (! rc->p_rts_flags) { lock_dequeue(rc); } rc->p_rts_flags = (short )((int )rc->p_rts_flags | 256); goto while_7_break; } while_7_break: /* internal */ ; if ((int )(rc->p_priv)->s_flags & 16) { if ((rc->p_priv)->s_asynsize) { kprintf(__string_clear_endpoint__clearing_s_asynsize_of__s____d_, rc->p_name,rc->p_endpoint); proc_stacktrace(rc); } (rc->p_priv)->s_asynsize = 0U; } if (((int )rc->p_rts_flags & 4) == 4) { isokendpt_f((char *)(__string_system_c),498,rc->p_sendto_e,& target_proc, 1); xpp = & (*((pproc_addr + 4) + target_proc))->p_caller_q; while (1) { if (! (*xpp != (struct proc_1 *)0)) { goto while_8_break; } if (*xpp == rc) { *xpp = (*xpp)->p_q_link; kprintf(__string_endpoint__d____s_removed_from_queue_at__d_, rc->p_endpoint,rc->p_name,rc->p_sendto_e); goto while_8_break; } xpp = & (*xpp)->p_q_link; } while_8_break: /* internal */ ; rc->p_rts_flags = (short )((int )rc->p_rts_flags & -5); } rc->p_rts_flags = (short )((int )rc->p_rts_flags & -9); rp_8 = proc; while (1) { if (! (rp_8 < & proc[104])) { goto while_9_break; } if ((int )rp_8->p_rts_flags == 1) { goto __Cont; } /*@ assert ((unsigned int )(rc->p_priv)->s_id%16U ≥ 0); // synthesized assert ((unsigned int )(rc->p_priv)->s_id%16U < 32); // synthesized assert (1 ≤ 2147483647>>(unsigned int )(rc->p_priv)->s_id%16U); // synthesized */ (rp_8->p_priv)->s_notify_pending.chunk[(unsigned int )(rc->p_priv)->s_id / 16U] = (unsigned short )( (int )(rp_8->p_priv)->s_notify_pending.chunk[(unsigned int )(rc->p_priv)->s_id / 16U] & ~ ( 1 << (unsigned int )(rc->p_priv)->s_id % 16U)); if (((int )rp_8->p_rts_flags & 8) == 8) { if (rp_8->p_getfrom_e == rc->p_endpoint) { rp_8->p_reg.retreg = 4294967188U; while (1) { rts_0 = (int )rp_8->p_rts_flags; rp_8->p_rts_flags = (short )((int )rp_8->p_rts_flags & -9); if (rts_0) { if (! rp_8->p_rts_flags) { lock_enqueue(rp_8); } } goto while_10_break; } while_10_break: /* internal */ ; kprintf(__string_endpoint__d____s_receiving_from_dead_src_ep__d____s_, rp_8->p_endpoint,rp_8->p_name,rc->p_endpoint,rc->p_name); } } if (((int )rp_8->p_rts_flags & 4) == 4) { if (rp_8->p_sendto_e == rc->p_endpoint) { rp_8->p_reg.retreg = 4294967187U; while (1) { rts_0_0 = (int )rp_8->p_rts_flags; rp_8->p_rts_flags = (short )((int )rp_8->p_rts_flags & -5); if (rts_0_0) { if (! rp_8->p_rts_flags) { lock_enqueue(rp_8); } } goto while_11_break; } while_11_break: /* internal */ ; kprintf(__string_endpoint__d____s_send_to_dying_dst_ep__d___s__, rp_8->p_endpoint,rp_8->p_name,rc->p_endpoint,rc->p_name); } } __Cont: /* internal */ ; rp_8 ++; } while_9_break: /* internal */ ; np = softnotify; while (1) { if (! np) { goto while_12_break; } if (np == rc) { minix_panic((char *)(__string_dying_proc_was_on_next_soft_notify), np->p_endpoint); } np = np->next_soft_notify; } while_12_break: /* internal */ ; return; } /*@ behavior default: */ phys_bytes umap_verify_grant(struct proc_1 *rp_5 , endpoint_t grantee , cp_grant_id_t grant_0 , vir_bytes offset , vir_bytes bytes_3 , int access_0 ) { int proc_nr_2 ; vir_bytes v_offset ; endpoint_t granter_0 ; int tmp_1 ; int tmp_0_1 ; phys_bytes tmp_1_0 ; phys_bytes __retres_2 ; tmp_1 = verify_grant(rp_5->p_endpoint,grantee,grant_0,bytes_3,access_0, offset,& v_offset,& granter_0); if (tmp_1 != 0) { __retres_2 = 0UL; goto return_label; } else { tmp_0_1 = isokendpt_f((char *)(__string_system_c),577,granter_0, & proc_nr_2,0); if (! tmp_0_1) { __retres_2 = 0UL; goto return_label; } } tmp_1_0 = umap_virtual(*((pproc_addr + 4) + proc_nr_2),1,v_offset,bytes_3); __retres_2 = tmp_1_0; return_label: /* internal */ return (__retres_2); } /*@ behavior default: */ static void softnotify_check(void) { struct proc_1 *np_0 ; struct proc_1 *nextnp ; if (! softnotify) { goto return_label; } np_0 = softnotify; while (1) { if (! np_0) { goto while_13_break; } if (! np_0->p_softnotified) { minix_panic((char *)(__string_softnotify_but_no_p_softnotified),32768); } lock_notify(-2,np_0->p_endpoint); nextnp = np_0->next_soft_notify; np_0->next_soft_notify = (struct proc_1 *)((char *)0); np_0->p_softnotified = 0; np_0 = nextnp; } while_13_break: /* internal */ ; softnotify = (struct proc_1 *)((char *)0); return_label: /* internal */ return; } /*@ behavior default: */ static struct proc_1 *vmrestart_check(message *m_0 ) { int type_1 ; int r_0 ; struct proc_1 *restarting_0 ; int tmp_2 ; int i_1 ; int rts_1 ; struct proc_1 *__retres_3 ; restarting_0 = vmrestart; if (! restarting_0) { __retres_3 = (struct proc_1 *)((char *)0); goto return_label; } if ((int )restarting_0->p_rts_flags & 1) { minix_panic((char *)(__string_SYSTEM__VMREQUEST_set_for_empty_process), 32768); } type_1 = restarting_0->p_vmrequest.type_0; restarting_0->p_vmrequest.type_0 = 0; vmrestart = restarting_0->p_vmrequest.nextrestart; if (! (((int )restarting_0->p_rts_flags & 2048) == 2048)) { minix_panic((char *)(__string_SYSTEM__VMREQUEST_not_set_for_process_on_vmrestart_queue), restarting_0->p_endpoint); } switch (type_1) { case 1: ; memcpy((char *)m_0,(char *)(& restarting_0->p_vmrequest.saved.reqmsg), 36U); if (m_0->m_source != restarting_0->p_endpoint) { minix_panic((char *)(__string_SYSTEM__vmrestart_source_doesn_t_match), 32768); } tmp_2 = isokendpt_f((char *)(__string_system_c),638,m_0->m_source, & who_p,0); if (! tmp_2) { kprintf(__string_SYSTEM__ignoring_call__d_from_dead__d_,m_0->m_type, m_0->m_source); __retres_3 = (struct proc_1 *)((char *)0); goto return_label; } i_1 = m_0->m_type - 1536; if (i_1 >= 0) { if (! (i_1 < 45)) { minix_panic((char *)(__string_call_number_out_of_range),i_1); } } else { minix_panic((char *)(__string_call_number_out_of_range),i_1); } __retres_3 = restarting_0; goto return_label; case 2: ; kprintf(__string_SYSTEM__restart_sys_call_); sys_call_restart(restarting_0); __retres_3 = (struct proc_1 *)((char *)0); goto return_label; case 3: r_0 = data_copy(-2, (unsigned long )(& restarting_0->p_vmrequest.saved.msgcopy.msgbuf), (restarting_0->p_vmrequest.saved.msgcopy.dst_2)->p_endpoint, restarting_0->p_vmrequest.saved.msgcopy.dst_v, 36U); if (r_0 != 0) { minix_panic((char *)(__string_SYSTEM__delayed_msgcopy_failed),r_0); } while (1) { rts_1 = (int )restarting_0->p_rts_flags; restarting_0->p_rts_flags = (short )((int )restarting_0->p_rts_flags & -2049); if (rts_1) { if (! restarting_0->p_rts_flags) { lock_enqueue(restarting_0); } } goto while_15_break; } while_15_break: /* internal */ ; __retres_3 = (struct proc_1 *)((char *)0); goto return_label; default: ; minix_panic((char *)(__string_strange_restart_type),type_1); } minix_panic((char *)(__string_fell_out_of_switch),32768); __retres_3 = (struct proc_1 *)0; return_label: /* internal */ return (__retres_3); } /*@ behavior default: */ void __globinit_whole_program(void) { } [jessie] Retype variables of array type [jessie] Retype logic functions/predicates [jessie] Expand structure copying [jessie] Retype variables of structure type [jessie] Retype variables and fields whose address is taken system.c:196:[jessie] failure: Unexpected failure. Please submit bug report (Ref. "norm.ml:1105:8"). [kernel] Plugin jessie aborted because of an internal error. Please report with 'crash' at http://bts.frama-c.com