|
# 1 "/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.aspect"
|
|
# 1 "<built-in>"
|
|
# 1 "<command-line>"
|
|
# 1 "/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.aspect"
|
|
|
|
info: expand(module_init(arg)){
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","init: '%s'\n",$arg_val1>
|
|
}
|
|
|
|
info: expand(module_exit(arg)){
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","exit: '%s'\n",$arg_val1>
|
|
}
|
|
|
|
info: expand(EXPORT_SYMBOL_GPL(arg)){
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","gpl_function: '%s'\n",$arg_val1>
|
|
}
|
|
|
|
info: expand(EXPORT_SYMBOL(arg)){
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","export_symbol_function: '%s'\n",$arg_val1>
|
|
}
|
|
|
|
info: init_global($ struct $ $){
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","Structure variable name is '%s'\n",$var_name>
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","Structure variable type name is '%s'\n",$var_type_name>
|
|
$fprintf_var_init_list<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer">
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","Structure description end\n">
|
|
}
|
|
|
|
before: call ($ request_irq(unsigned int, irqreturn_t (*handler)(int, void *), $, $, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq request: '%s', arg2='%s'\n",$func_name,$arg_value2>
|
|
}
|
|
|
|
before: call ($ request_any_context_irq(unsigned int, irqreturn_t (*handler)(int, void *), $, $, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq request_any_context_irq: '%s', arg2='%s'\n",$func_name,$arg_value2>
|
|
}
|
|
|
|
before: call ($ request_percpu_irq(unsigned int, irqreturn_t (*handler)(int, void *), $, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq request_any_context_irq: '%s', arg2='%s'\n",$func_name,$arg_value2>
|
|
}
|
|
|
|
|
|
before: call ($ request_threaded_irq(unsigned int, irqreturn_t (*handler)(int, void *), irqreturn_t (*thread_fn)(int, void *), $, $, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq request_threaded_irq: '%s', arg2='%s', arg3='%s'\n",$func_name,$arg_value2,$arg_value3>
|
|
}
|
|
|
|
before: call ($ devm_request_threaded_irq(struct device *, unsigned int, irqreturn_t (*handler)(int, void *), irqreturn_t (*thread_fn)(int, void *), $, $, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq devm_request_threaded_irq: '%s', arg3='%s', arg4='%s'\n",$func_name,$arg_value3,$arg_value4>
|
|
}
|
|
|
|
before: call (void free_irq(unsigned int, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq free_irq: '%s'\n",$func_name>
|
|
}
|
|
|
|
before: call (void devm_free_irq(struct device *, unsigned int, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq devm_free_irq: '%s'\n",$func_name>
|
|
}
|
|
|
|
before: call (void free_percpu_irq(unsigned int, void *)) {
|
|
$fprintf<"/work/zakharov/bench-tests/cpa/work/current--X--drivers/net/usb/cdc-phonet.ko--X--deg2_cpalinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/12/deg/analysis/first_request.answer","irq free_percpu_irq: '%s'\n",$func_name>
|
|
}
|