Project

General

Profile

Download (1.42 KB)

Feature #7467 » job.json

Vitaly Mordan, 08/26/2016 03:10 PM

 
{
"Linux kernel": {
"source": "linux-4.0-rc1",
"configuration": "allmodconfig",
"modules": ["drivers/video/fbdev/broadsheetfb.ko"]
},
"LKVOG strategy": {"name": "separate modules"},
"maximum verification object size": 30000,
"rule specifications DB": "rule specs.json",
"rule specifications": [
"linux:mmc:sdio_func_as",
"linux:usb:coherent",
"linux:usb:dev",
"linux:usb:gadget",
"linux:usb:register",
"linux:usb:urb",
"linux:alloc:irq",
"linux:alloc:spin lock",
"linux:alloc:usb lock",
"linux:chrdev",
"linux:class",
"linux:module",
"linux:mutex",
"linux:netdev",
"linux:rwlock",
"linux:spinlock",
"linux:rtnl",
"linux:sock",
"linux:bitops",
"linux:blk:request",
"linux:blk:queue",
"linux:rculock",
"linux:rculockbh",
"linux:rculocksched",
"linux:srculock",
"linux:completion",
"linux:sysfs",
"linux:iomem",
"linux:idr",
"linux:gendisk"
],
"VTG strategy": {
"name": "sequential combination",
"verifier": {
"name": "CPAchecker"
},
"resource limits": {
"wall time": 1000000,
"CPU time": 900000,
"memory size": 10000000000,
"CPU model": null,
"number of CPU cores": 1,
"result size": 1000000
},
"merge source files": true
}
}

(2-2/3)