extern void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "drivers--mtd--ar7part.ko_002.17b536c.32_1.cil_true-unreach-call.i", 3, "reach_error"); } /* Generated by CIL v. 1.5.1 */ /* print_CIL_Input is false */ typedef __builtin_va_list __gnuc_va_list; typedef __gnuc_va_list va_list; typedef unsigned int __kernel_mode_t; typedef unsigned long __kernel_size_t; typedef long __kernel_ssize_t; typedef long long __kernel_loff_t; typedef unsigned char __u8; typedef unsigned short __u16; typedef unsigned int __u32; typedef unsigned long long __u64; typedef unsigned char u8; typedef unsigned long long u64; typedef __kernel_mode_t mode_t; typedef __kernel_loff_t loff_t; typedef __kernel_size_t size_t; typedef __kernel_ssize_t ssize_t; typedef unsigned char u_char; typedef unsigned long u_long; typedef __u8 uint8_t; typedef __u32 uint32_t; typedef __u64 uint64_t; typedef unsigned int gfp_t; typedef u64 phys_addr_t; typedef phys_addr_t resource_size_t; struct __anonstruct_atomic_t_7 { int volatile counter ; }; typedef struct __anonstruct_atomic_t_7 atomic_t; struct __anonstruct_atomic64_t_8 { long volatile counter ; }; typedef struct __anonstruct_atomic64_t_8 atomic64_t; struct module; struct bug_entry { int bug_addr_disp ; int file_disp ; unsigned short line ; unsigned short flags ; }; struct page; struct raw_spinlock; struct task_struct; struct kmem_cache; typedef atomic64_t atomic_long_t; struct list_head { struct list_head *next ; struct list_head *prev ; }; struct raw_spinlock { unsigned int slock ; }; typedef struct raw_spinlock raw_spinlock_t; struct __anonstruct_spinlock_t_38 { raw_spinlock_t raw_lock ; unsigned int magic ; unsigned int owner_cpu ; void *owner ; }; typedef struct __anonstruct_spinlock_t_38 spinlock_t; struct notifier_block { int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ; struct notifier_block *next ; int priority ; }; struct kobject; struct attribute { char const *name ; struct module *owner ; mode_t mode ; }; struct sysfs_ops { ssize_t (*show)(struct kobject * , struct attribute * , char * ) ; ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ; }; struct sysfs_dirent; struct kref { atomic_t refcount ; }; struct kset; struct kobj_type; struct kobject { char const *name ; struct list_head entry ; struct kobject *parent ; struct kset *kset ; struct kobj_type *ktype ; struct sysfs_dirent *sd ; struct kref kref ; unsigned int state_initialized : 1 ; unsigned int state_in_sysfs : 1 ; unsigned int state_add_uevent_sent : 1 ; unsigned int state_remove_uevent_sent : 1 ; }; struct kobj_type { void (*release)(struct kobject *kobj ) ; struct sysfs_ops *sysfs_ops ; struct attribute **default_attrs ; }; struct kobj_uevent_env { char *envp[32] ; int envp_idx ; char buf[2048] ; int buflen ; }; struct kset_uevent_ops { int (*filter)(struct kset *kset , struct kobject *kobj ) ; char const *(*name)(struct kset *kset , struct kobject *kobj ) ; int (*uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ; }; struct kset { struct list_head list ; spinlock_t list_lock ; struct kobject kobj ; struct kset_uevent_ops *uevent_ops ; }; enum stat_item { ALLOC_FASTPATH = 0, ALLOC_SLOWPATH = 1, FREE_FASTPATH = 2, FREE_SLOWPATH = 3, FREE_FROZEN = 4, FREE_ADD_PARTIAL = 5, FREE_REMOVE_PARTIAL = 6, ALLOC_FROM_PARTIAL = 7, ALLOC_SLAB = 8, ALLOC_REFILL = 9, FREE_SLAB = 10, CPUSLAB_FLUSH = 11, DEACTIVATE_FULL = 12, DEACTIVATE_EMPTY = 13, DEACTIVATE_TO_HEAD = 14, DEACTIVATE_TO_TAIL = 15, DEACTIVATE_REMOTE_FREES = 16, ORDER_FALLBACK = 17, NR_SLUB_STAT_ITEMS = 18 } ; struct kmem_cache_cpu { void **freelist ; struct page *page ; int node ; unsigned int offset ; unsigned int objsize ; unsigned int stat[NR_SLUB_STAT_ITEMS] ; }; struct kmem_cache_node { spinlock_t list_lock ; unsigned long nr_partial ; unsigned long min_partial ; struct list_head partial ; atomic_long_t nr_slabs ; atomic_long_t total_objects ; struct list_head full ; }; struct kmem_cache_order_objects { unsigned long x ; }; struct kmem_cache { unsigned long flags ; int size ; int objsize ; int offset ; struct kmem_cache_order_objects oo ; struct kmem_cache_node local_node ; struct kmem_cache_order_objects max ; struct kmem_cache_order_objects min ; gfp_t allocflags ; int refcount ; void (*ctor)(void * ) ; int inuse ; int align ; char const *name ; struct list_head list ; struct kobject kobj ; int remote_node_defrag_ratio ; struct kmem_cache_node *node[1 << 9] ; struct kmem_cache_cpu *cpu_slab[4096] ; }; typedef __u64 Elf64_Addr; typedef __u16 Elf64_Half; typedef __u32 Elf64_Word; typedef __u64 Elf64_Xword; struct elf64_sym { Elf64_Word st_name ; unsigned char st_info ; unsigned char st_other ; Elf64_Half st_shndx ; Elf64_Addr st_value ; Elf64_Xword st_size ; }; typedef struct elf64_sym Elf64_Sym; struct marker; typedef void marker_probe_func(void *probe_private , void *call_private , char const *fmt , va_list *args ); struct marker_probe_closure { marker_probe_func *func ; void *probe_private ; }; struct marker { char const *name ; char const *format ; char state ; char ptype ; void (*call)(struct marker const *mdata , void *call_private , ...) ; struct marker_probe_closure single ; struct marker_probe_closure *multi ; char const *tp_name ; void *tp_cb ; } __attribute__((__aligned__(8))) ; struct tracepoint; struct tracepoint { char const *name ; int state ; void **funcs ; } __attribute__((__aligned__(32))) ; struct mod_arch_specific { }; struct kernel_symbol { unsigned long value ; char const *name ; }; struct module_attribute { struct attribute attr ; ssize_t (*show)(struct module_attribute * , struct module * , char * ) ; ssize_t (*store)(struct module_attribute * , struct module * , char const * , size_t count ) ; void (*setup)(struct module * , char const * ) ; int (*test)(struct module * ) ; void (*free)(struct module * ) ; }; struct module_param_attrs; struct module_kobject { struct kobject kobj ; struct module *mod ; struct kobject *drivers_dir ; struct module_param_attrs *mp ; }; struct exception_table_entry; enum module_state { MODULE_STATE_LIVE = 0, MODULE_STATE_COMING = 1, MODULE_STATE_GOING = 2 } ; struct module_sect_attrs; struct module_notes_attrs; struct module { enum module_state state ; struct list_head list ; char name[64UL - sizeof(unsigned long )] ; struct module_kobject mkobj ; struct module_attribute *modinfo_attrs ; char const *version ; char const *srcversion ; struct kobject *holders_dir ; struct kernel_symbol const *syms ; unsigned long const *crcs ; unsigned int num_syms ; unsigned int num_gpl_syms ; struct kernel_symbol const *gpl_syms ; unsigned long const *gpl_crcs ; struct kernel_symbol const *unused_syms ; unsigned long const *unused_crcs ; unsigned int num_unused_syms ; unsigned int num_unused_gpl_syms ; struct kernel_symbol const *unused_gpl_syms ; unsigned long const *unused_gpl_crcs ; struct kernel_symbol const *gpl_future_syms ; unsigned long const *gpl_future_crcs ; unsigned int num_gpl_future_syms ; unsigned int num_exentries ; struct exception_table_entry *extable ; int (*init)(void) ; void *module_init ; void *module_core ; unsigned int init_size ; unsigned int core_size ; unsigned int init_text_size ; unsigned int core_text_size ; struct mod_arch_specific arch ; unsigned int taints ; unsigned int num_bugs ; struct list_head bug_list ; struct bug_entry *bug_table ; Elf64_Sym *symtab ; unsigned int num_symtab ; char *strtab ; struct module_sect_attrs *sect_attrs ; struct module_notes_attrs *notes_attrs ; void *percpu ; char *args ; struct marker *markers ; unsigned int num_markers ; struct tracepoint *tracepoints ; unsigned int num_tracepoints ; struct list_head modules_which_use_me ; struct task_struct *waiter ; void (*exit)(void) ; char *refptr ; }; struct kvec { void *iov_base ; size_t iov_len ; }; struct otp_info { uint32_t start ; uint32_t length ; uint32_t locked ; }; struct nand_oobfree { uint32_t offset ; uint32_t length ; }; struct nand_ecclayout { uint32_t eccbytes ; uint32_t eccpos[64] ; uint32_t oobavail ; struct nand_oobfree oobfree[8] ; }; struct mtd_ecc_stats { uint32_t corrected ; uint32_t failed ; uint32_t badblocks ; uint32_t bbtblocks ; }; struct mtd_info; struct erase_info { struct mtd_info *mtd ; uint64_t addr ; uint64_t len ; uint64_t fail_addr ; u_long time ; u_long retries ; unsigned int dev ; unsigned int cell ; void (*callback)(struct erase_info *self ) ; u_long priv ; u_char state ; struct erase_info *next ; }; struct mtd_erase_region_info { uint64_t offset ; uint32_t erasesize ; uint32_t numblocks ; unsigned long *lockmap ; }; enum __anonenum_mtd_oob_mode_t_102 { MTD_OOB_PLACE = 0, MTD_OOB_AUTO = 1, MTD_OOB_RAW = 2 } ; typedef enum __anonenum_mtd_oob_mode_t_102 mtd_oob_mode_t; struct mtd_oob_ops { mtd_oob_mode_t mode ; size_t len ; size_t retlen ; size_t ooblen ; size_t oobretlen ; uint32_t ooboffs ; uint8_t *datbuf ; uint8_t *oobbuf ; }; struct mtd_info { u_char type ; uint32_t flags ; uint64_t size ; uint32_t erasesize ; uint32_t writesize ; uint32_t oobsize ; uint32_t oobavail ; unsigned int erasesize_shift ; unsigned int writesize_shift ; unsigned int erasesize_mask ; unsigned int writesize_mask ; char const *name ; int index ; struct nand_ecclayout *ecclayout ; int numeraseregions ; struct mtd_erase_region_info *eraseregions ; int (*erase)(struct mtd_info *mtd , struct erase_info *instr ) ; int (*point)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , void **virt , resource_size_t *phys ) ; void (*unpoint)(struct mtd_info *mtd , loff_t from , size_t len ) ; int (*read)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , u_char *buf ) ; int (*write)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen , u_char const *buf ) ; int (*panic_write)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen , u_char const *buf ) ; int (*read_oob)(struct mtd_info *mtd , loff_t from , struct mtd_oob_ops *ops ) ; int (*write_oob)(struct mtd_info *mtd , loff_t to , struct mtd_oob_ops *ops ) ; int (*get_fact_prot_info)(struct mtd_info *mtd , struct otp_info *buf , size_t len ) ; int (*read_fact_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , u_char *buf ) ; int (*get_user_prot_info)(struct mtd_info *mtd , struct otp_info *buf , size_t len ) ; int (*read_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , u_char *buf ) ; int (*write_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , u_char *buf ) ; int (*lock_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len ) ; int (*writev)(struct mtd_info *mtd , struct kvec const *vecs , unsigned long count , loff_t to , size_t *retlen ) ; void (*sync)(struct mtd_info *mtd ) ; int (*lock)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ; int (*unlock)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ; int (*suspend)(struct mtd_info *mtd ) ; void (*resume)(struct mtd_info *mtd ) ; int (*block_isbad)(struct mtd_info *mtd , loff_t ofs ) ; int (*block_markbad)(struct mtd_info *mtd , loff_t ofs ) ; struct notifier_block reboot_notifier ; struct mtd_ecc_stats ecc_stats ; int subpage_sft ; void *priv ; struct module *owner ; int usecount ; int (*get_device)(struct mtd_info *mtd ) ; void (*put_device)(struct mtd_info *mtd ) ; }; struct mtd_partition { char *name ; uint64_t size ; uint64_t offset ; uint32_t mask_flags ; struct nand_ecclayout *ecclayout ; struct mtd_info **mtdp ; }; struct mtd_part_parser { struct list_head list ; struct module *owner ; char const *name ; int (*parse_fn)(struct mtd_info * , struct mtd_partition ** , unsigned long ) ; }; struct ar7_bin_rec { unsigned int checksum ; unsigned int length ; unsigned int address ; }; struct thread_info; struct mutex { atomic_t count ; spinlock_t wait_lock ; struct list_head wait_list ; struct thread_info *owner ; char const *name ; void *magic ; }; extern int ( /* format attribute */ printk)(char const *fmt , ...) ; extern int strncmp(char const * , char const * , __kernel_size_t ) ; extern void *__kmalloc(size_t size , gfp_t flags ) ; __inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size , gfp_t flags ) { void *tmp___2 ; { tmp___2 = __kmalloc(size, flags); return (tmp___2); } } __inline static void *kzalloc(size_t size , gfp_t flags ) { void *tmp ; { tmp = kmalloc(size, flags | 32768U); return (tmp); } } int init_module(void) ; extern struct module __this_module ; extern int register_mtd_parser(struct mtd_part_parser *parser ) ; static int create_mtd_partitions(struct mtd_info *master , struct mtd_partition **pparts , unsigned long origin ) { struct ar7_bin_rec header ; unsigned int offset ; size_t len ; unsigned int pre_size ; unsigned int post_size ; unsigned int root_offset ; int retries ; struct mtd_partition *ar7_parts ; void *tmp ; int tmp___0 ; int tmp___1 ; { pre_size = master->erasesize; post_size = 0; root_offset = 917504; retries = 10; tmp = kzalloc(sizeof(*ar7_parts) * 4UL, (16U | 64U) | 128U); ar7_parts = tmp; if (! ar7_parts) { return (-12); } else { } (ar7_parts + 0)->name = "loader"; (ar7_parts + 0)->offset = 0; (ar7_parts + 0)->size = master->erasesize; (ar7_parts + 0)->mask_flags = 1024; (ar7_parts + 1)->name = "config"; (ar7_parts + 1)->offset = 0; (ar7_parts + 1)->size = master->erasesize; (ar7_parts + 1)->mask_flags = 0; while (1) { offset = pre_size; (*(master->read))(master, offset, sizeof(header), & len, (uint8_t *)(& header)); tmp___0 = strncmp((char *)(& header), "TIENV0.8", 8); if (tmp___0) { } else { (ar7_parts + 1)->offset = pre_size; } if (header.checksum == 4277008962U) { break; } else { } if (header.checksum == 4276949633U) { break; } else { } pre_size = pre_size + master->erasesize; tmp___1 = retries; retries = retries - 1; if (tmp___1) { } else { break; } } pre_size = offset; if (! (ar7_parts + 1)->offset) { (ar7_parts + 1)->offset = master->size - (uint64_t )master->erasesize; post_size = master->erasesize; } else { } switch (header.checksum) { case 4277008962U: while (1) { if (header.length) { } else { break; } offset = (unsigned long )offset + (sizeof(header) + (unsigned long )header.length); (*(master->read))(master, offset, sizeof(header), & len, (uint8_t *)(& header)); } root_offset = ((unsigned long )offset + sizeof(header)) + 4UL; break; case 4276949633U: while (1) { if (header.length) { } else { break; } offset = (unsigned long )offset + (sizeof(header) + (unsigned long )header.length); (*(master->read))(master, offset, sizeof(header), & len, (uint8_t *)(& header)); } root_offset = (((unsigned long )offset + sizeof(header)) + 4UL) + 255UL; root_offset = root_offset & ~ ((uint32_t )255); break; default: printk("<4>Unknown magic: %08x\n", header.checksum); break; } (*(master->read))(master, root_offset, sizeof(header), & len, (u8 *)(& header)); if (header.checksum != 1936814952U) { root_offset = root_offset + (master->erasesize - (uint32_t )1); root_offset = root_offset & ~ (master->erasesize - (uint32_t )1); } else { } (ar7_parts + 2)->name = "linux"; (ar7_parts + 2)->offset = pre_size; (ar7_parts + 2)->size = (master->size - (uint64_t )pre_size) - (uint64_t )post_size; (ar7_parts + 2)->mask_flags = 0; (ar7_parts + 3)->name = "rootfs"; (ar7_parts + 3)->offset = root_offset; (ar7_parts + 3)->size = (master->size - (uint64_t )root_offset) - (uint64_t )post_size; (ar7_parts + 3)->mask_flags = 0; *pparts = ar7_parts; return (4); } } static struct mtd_part_parser ar7_parser = {{0, 0}, & __this_module, "ar7part", & create_mtd_partitions}; static int ar7_parser_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ; static int ar7_parser_init(void) { int tmp ; { tmp = register_mtd_parser(& ar7_parser); return (tmp); } } int init_module(void) { int tmp ; { tmp = ar7_parser_init(); return (tmp); } } static char const __mod_license151[12] __attribute__((__used__, __unused__, __section__(".modinfo"))) = { 'l', 'i', 'c', 'e', 'n', 's', 'e', '=', 'G', 'P', 'L', '\000'}; static char const __mod_author153[72] __attribute__((__used__, __unused__, __section__(".modinfo"))) = { 'a', 'u', 't', 'h', 'o', 'r', '=', 'F', 'e', 'l', 'i', 'x', ' ', 'F', 'i', 'e', 't', 'k', 'a', 'u', ' ', '<', 'n', 'b', 'd', '@', 'o', 'p', 'e', 'n', 'w', 'r', 't', '.', 'o', 'r', 'g', '>', ',', ' ', 'E', 'u', 'g', 'e', 'n', 'e', ' ', 'K', 'o', 'n', 'e', 'v', ' ', '<', 'e', 'j', 'k', 'a', '@', 'o', 'p', 'e', 'n', 'w', 'r', 't', '.', 'o', 'r', 'g', '>', '\000'}; static char const __mod_description154[40] __attribute__((__used__, __unused__, __section__(".modinfo"))) = { 'd', 'e', 's', 'c', 'r', 'i', 'p', 't', 'i', 'o', 'n', '=', 'M', 'T', 'D', ' ', 'p', 'a', 'r', 't', 'i', 't', 'i', 'o', 'n', 'i', 'n', 'g', ' ', 'f', 'o', 'r', ' ', 'T', 'I', ' ', 'A', 'R', '7', '\000'}; void ldv_check_final_state(void) ; extern void ldv_initialize(void) ; extern void ldv_handler_precall(void) ; extern int nondet_int(void) ; int LDV_IN_INTERRUPT ; int main(void) { struct mtd_info *var_group1 ; struct mtd_partition **var_group2 ; unsigned long var_create_mtd_partitions_0_p2 ; int tmp ; int tmp___0 ; int tmp___1 ; { LDV_IN_INTERRUPT = 1; ldv_initialize(); ldv_handler_precall(); tmp = ar7_parser_init(); if (tmp) { goto ldv_module_exit; } else { } while (1) { tmp___1 = nondet_int(); if (tmp___1) { } else { break; } tmp___0 = nondet_int(); switch (tmp___0) { case 0: ldv_handler_precall(); create_mtd_partitions(var_group1, var_group2, var_create_mtd_partitions_0_p2); break; default: break; } } ldv_module_exit: ldv_check_final_state(); return 0; } } long ldv__builtin_expect(long exp , long c ) ; void mutex_lock(struct mutex *lock ) ; int ( __attribute__((__warn_unused_result__)) mutex_lock_interruptible)(struct mutex *lock ) ; int ( __attribute__((__warn_unused_result__)) mutex_lock_killable)(struct mutex *lock ) ; int mutex_trylock(struct mutex *lock ) ; void mutex_unlock(struct mutex *lock ) ; __inline static void ldv_error(void) { { LDV_ERROR: {reach_error();abort();} } } extern int ldv_undef_int(void) ; long ldv__builtin_expect(long exp , long c ) { { return (exp); } } int ldv_mutex = 1; int ( __attribute__((__warn_unused_result__)) mutex_lock_interruptible)(struct mutex *lock ) { int nondetermined ; { if (ldv_mutex == 1) { } else { ldv_error(); } nondetermined = ldv_undef_int(); if (nondetermined) { ldv_mutex = 2; return (0); } else { return (-4); } } } int ( __attribute__((__warn_unused_result__)) mutex_lock_killable)(struct mutex *lock ) { int nondetermined ; { if (ldv_mutex == 1) { } else { ldv_error(); } nondetermined = ldv_undef_int(); if (nondetermined) { ldv_mutex = 2; return (0); } else { return (-4); } } } int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) { int atomic_value_after_dec ; { if (ldv_mutex == 1) { } else { ldv_error(); } atomic_value_after_dec = ldv_undef_int(); if (atomic_value_after_dec == 0) { ldv_mutex = 2; return (1); } else { } return (0); } } void mutex_lock(struct mutex *lock ) { { if (ldv_mutex == 1) { } else { ldv_error(); } ldv_mutex = 2; return; } } int mutex_trylock(struct mutex *lock ) { int nondetermined ; { if (ldv_mutex == 1) { } else { ldv_error(); } nondetermined = ldv_undef_int(); if (nondetermined) { ldv_mutex = 2; return (1); } else { return (0); } } } void mutex_unlock(struct mutex *lock ) { { if (ldv_mutex == 2) { } else { ldv_error(); } ldv_mutex = 1; return; } } void ldv_check_final_state(void) { { if (ldv_mutex == 1) { } else { ldv_error(); } return; } }