// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Function: __dynamic_dev_dbg // with type: int __dynamic_dev_dbg(struct _ddebug *, const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int __dynamic_dev_dbg(struct _ddebug *arg0, const struct device *arg1, const char *arg2, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: __mutex_init // with type: void __mutex_init(struct mutex *, const char *, struct lock_class_key *) // with return type: void void __mutex_init(struct mutex *arg0, const char *arg1, struct lock_class_key *arg2) { // Void type return; } // Function: dev_err // with type: int dev_err(const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int dev_err(const struct device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } extern _Bool __VERIFIER_nondet_bool(void) ; extern void *malloc(size_t) ; __inline static IS_ERR(void const *ptr ) ; extern void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } void *ldv_malloc(size_t size ) { if(__VERIFIER_nondet_bool()) return 0; void *p = malloc(size); assume_abort_if_not(IS_ERR(p) == 0); return p; } // Function: dev_get_drvdata // with type: void *dev_get_drvdata(const struct device *) // with return type: (void)* void *dev_get_drvdata(const struct device *arg0) { // Pointer type return ldv_malloc(0UL); } // Function: dev_set_drvdata // with type: int dev_set_drvdata(struct device *, void *) // with return type: int int __VERIFIER_nondet_int(void); int dev_set_drvdata(struct device *arg0, void *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: dev_warn // with type: int dev_warn(const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int dev_warn(const struct device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: devm_kzalloc // with type: void *devm_kzalloc(struct device *, size_t , gfp_t ) // with return type: (void)* void *devm_kzalloc(struct device *arg0, size_t arg1, gfp_t arg2) { // Pointer type return ldv_malloc(0UL); } // Function: hwmon_device_register // with type: struct device *hwmon_device_register(struct device *) // with return type: (struct device)* struct device *hwmon_device_register(struct device *arg0) { // Pointer type return ldv_malloc(sizeof(struct device)); } // Function: hwmon_device_unregister // with type: void hwmon_device_unregister(struct device *) // with return type: void void hwmon_device_unregister(struct device *arg0) { // Void type return; } // Function: i2c_del_driver // with type: void i2c_del_driver(struct i2c_driver *) // with return type: void void i2c_del_driver(struct i2c_driver *arg0) { // Void type return; } // Function: i2c_new_dummy // with type: struct i2c_client *i2c_new_dummy(struct i2c_adapter *, u16 ) // with return type: (struct i2c_client)* struct i2c_client *i2c_new_dummy(struct i2c_adapter *arg0, u16 arg1) { // Pointer type return ldv_malloc(sizeof(struct i2c_client)); } // Function: i2c_register_driver // with type: int i2c_register_driver(struct module *, struct i2c_driver *) // with return type: int int __VERIFIER_nondet_int(void); int i2c_register_driver(struct module *arg0, struct i2c_driver *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: i2c_smbus_read_byte_data // with type: s32 i2c_smbus_read_byte_data(const struct i2c_client *, u8 ) // with return type: s32 int __VERIFIER_nondet_int(void); s32 i2c_smbus_read_byte_data(const struct i2c_client *arg0, u8 arg1) { // Typedef type // Real type: int // Simple type return __VERIFIER_nondet_int(); } // Function: i2c_smbus_write_byte_data // with type: s32 i2c_smbus_write_byte_data(const struct i2c_client *, u8 , u8 ) // with return type: s32 int __VERIFIER_nondet_int(void); s32 i2c_smbus_write_byte_data(const struct i2c_client *arg0, u8 arg1, u8 arg2) { // Typedef type // Real type: int // Simple type return __VERIFIER_nondet_int(); } // Function: i2c_unregister_device // with type: void i2c_unregister_device(struct i2c_client *) // with return type: void void i2c_unregister_device(struct i2c_client *arg0) { // Void type return; } // Function: kstrtoll // with type: int kstrtoll(const char *, unsigned int, long long *) // with return type: int int __VERIFIER_nondet_int(void); int kstrtoll(const char *arg0, unsigned int arg1, long long *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: kstrtoull // with type: int kstrtoull(const char *, unsigned int, unsigned long long *) // with return type: int int __VERIFIER_nondet_int(void); int kstrtoull(const char *arg0, unsigned int arg1, unsigned long long *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: mutex_lock // with type: void mutex_lock(struct mutex *) // with return type: void void mutex_lock(struct mutex *arg0) { // Void type return; } // Function: mutex_trylock // with type: int mutex_trylock(struct mutex *) // with return type: int int __VERIFIER_nondet_int(void); int mutex_trylock(struct mutex *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: mutex_unlock // with type: void mutex_unlock(struct mutex *) // with return type: void void mutex_unlock(struct mutex *arg0) { // Void type return; } // Skip function: sprintf // Function: strlcpy // with type: size_t strlcpy(char *, const char *, size_t ) // with return type: size_t unsigned long __VERIFIER_nondet_ulong(void); size_t strlcpy(char *arg0, const char *arg1, size_t arg2) { // Typedef type // Real type: __kernel_size_t // Typedef type // Real type: __kernel_ulong_t // Typedef type // Real type: unsigned long // Simple type return __VERIFIER_nondet_ulong(); } // Function: sysfs_create_group // with type: int sysfs_create_group(struct kobject *, const struct attribute_group *) // with return type: int int __VERIFIER_nondet_int(void); int sysfs_create_group(struct kobject *arg0, const struct attribute_group *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: sysfs_remove_group // with type: void sysfs_remove_group(struct kobject *, const struct attribute_group *) // with return type: void void sysfs_remove_group(struct kobject *arg0, const struct attribute_group *arg1) { // Void type return; } // Function: vid_from_reg // with type: int vid_from_reg(int, u8 ) // with return type: int int __VERIFIER_nondet_int(void); int vid_from_reg(int arg0, u8 arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: vid_which_vrm // with type: u8 vid_which_vrm() // with return type: u8 unsigned char __VERIFIER_nondet_uchar(void); u8 vid_which_vrm() { // Typedef type // Real type: unsigned char // Simple type return __VERIFIER_nondet_uchar(); }