bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--char--agp--amd64-agp.ko-entry_point_true-unreach-call.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 66 66 544 2633
Removed infinite loop in amd64_insert_memory
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.144358873367
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'pcibios_resource_to_bus' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'agp_put_bridge' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'agp_remove_bridge' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_set_power_state as symbolic
Removed calls to 'amd_flush_garts' (function is undefined)
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function __phys_addr as symbolic
Defining function pci_get_slot as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Defining function pci_find_capability as symbolic
Defining function agp_alloc_bridge as symbolic
Defining function agp_add_bridge as symbolic
Defining function amd_cache_northbridges as symbolic
Defining function __request_region as symbolic
Defining function printk as symbolic
Defining function e820_any_mapped as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function agp_generic_mask_memory as symbolic
Defining function agp_generic_create_gatt_table as symbolic
Defining function agp_generic_free_gatt_table as symbolic
Removed calls to 'global_cache_flush' (function is undefined)
Defining function agp_generic_remove_memory as symbolic
Defining function agp_generic_alloc_by_type as symbolic
Defining function agp_generic_alloc_page as symbolic
Defining function agp_generic_alloc_pages as symbolic
Defining function agp_generic_type_to_mask_type as symbolic
Defining function agp_num_entries as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function pci_dev_present as symbolic
Defining function driver_attach as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'agp_generic_free_by_type' (function is undefined)
Removed calls to 'agp_generic_enable' (function is undefined)
Removed calls to 'agp_generic_destroy_page' (function is undefined)
Removed calls to 'agp_generic_destroy_pages' (function is undefined)
Defining function ldv_suspend_late_1 as symbolic
Defining function ldv_resume_early_1 as symbolic
Defining function ldv_shutdown_1 as symbolic
Defining function release_resource as symbolic
Linked our definitions to these undefined functions:
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.21607208252
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 107 78 304 1636
INFO: Starting verification
KLEE: WARNING ONCE: function "agp_amd64_probe" has inline asm
KLEE: WARNING ONCE: function "amd64_insert_memory" has inline asm
KLEE: WARNING: undefined reference to function: agp_generic_destroy_page
KLEE: WARNING: undefined reference to function: agp_generic_destroy_pages
KLEE: WARNING: undefined reference to function: agp_generic_enable
KLEE: WARNING: undefined reference to function: agp_generic_free_by_type
KLEE: WARNING: undefined reference to function: global_cache_flush
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5dbe58fe-ceb5-4be6-bdaa-9977923e5635/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 10176 states (over memory cap)
KLEE: WARNING: killing 9485 states (over memory cap)
KLEE: WARNING: killing 9804 states (over memory cap)
KLEE: WARNING: killing 10124 states (over memory cap)
KLEE: WARNING: killing 10257 states (over memory cap)
KLEE: WARNING: killing 10216 states (over memory cap)
KLEE: WARNING: killing 10711 states (over memory cap)
KLEE: WARNING: killing 11036 states (over memory cap)
KLEE: WARNING: killing 11444 states (over memory cap)
KLEE: WARNING: killing 11229 states (over memory cap)
KLEE: WARNING: killing 11369 states (over memory cap)
KLEE: WARNING: killing 11597 states (over memory cap)
KLEE: WARNING: killing 11301 states (over memory cap)
KLEE: WARNING: killing 11881 states (over memory cap)
KLEE: WARNING: killing 12027 states (over memory cap)
KLEE: WARNING: killing 11989 states (over memory cap)
KLEE: WARNING: killing 11950 states (over memory cap)
KLEE: WARNING: killing 8805 states (over memory cap)
KLEE: WARNING: killing 12426 states (over memory cap)
KLEE: WARNING: killing 8681 states (over memory cap)
KLEE: WARNING: killing 12195 states (over memory cap)
KLEE: WARNING: killing 8899 states (over memory cap)
KLEE: WARNING: killing 8627 states (over memory cap)
KLEE: WARNING: killing 8871 states (over memory cap)
KLEE: WARNING: killing 8598 states (over memory cap)
KLEE: WARNING: killing 8752 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 8717 states (over memory cap)
KLEE: WARNING: killing 8700 states (over memory cap)
KLEE: WARNING: killing 8682 states (over memory cap)
KLEE: WARNING: killing 9176 states (over memory cap)
KLEE: WARNING: killing 8901 states (over memory cap)
KLEE: WARNING: killing 8798 states (over memory cap)
KLEE: WARNING: killing 8699 states (over memory cap)
KLEE: WARNING: killing 9016 states (over memory cap)
KLEE: WARNING: killing 8917 states (over memory cap)
KLEE: WARNING: killing 9232 states (over memory cap)
KLEE: WARNING: killing 9133 states (over memory cap)
KLEE: WARNING: killing 9113 states (over memory cap)
KLEE: WARNING: killing 9180 states (over memory cap)
KLEE: WARNING: killing 8997 states (over memory cap)
KLEE: WARNING: killing 8893 states (over memory cap)
KLEE: WARNING: killing 9370 states (over memory cap)
KLEE: WARNING: killing 9350 states (over memory cap)
KLEE: WARNING: killing 9248 states (over memory cap)
KLEE: WARNING: killing 9314 states (over memory cap)
KLEE: WARNING: killing 9212 states (over memory cap)
KLEE: WARNING: killing 9110 states (over memory cap)
KLEE: WARNING: killing 9259 states (over memory cap)
KLEE: WARNING: killing 9074 states (over memory cap)
KLEE: WARNING: killing 9299 states (over memory cap)
KLEE: WARNING: killing 9445 states (over memory cap)
KLEE: WARNING: killing 9341 states (over memory cap)
KLEE: WARNING: killing 9325 states (over memory cap)
KLEE: WARNING: killing 9470 states (over memory cap)
KLEE: WARNING: killing 9129 states (over memory cap)
KLEE: WARNING: killing 9271 states (over memory cap)
KLEE: WARNING: killing 9418 states (over memory cap)
KLEE: WARNING: killing 9399 states (over memory cap)
KLEE: WARNING: killing 9306 states (over memory cap)
KLEE: WARNING: killing 9205 states (over memory cap)
KLEE: WARNING: killing 9426 states (over memory cap)
KLEE: WARNING: killing 9490 states (over memory cap)
KLEE: WARNING: killing 9470 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 9438 states (over memory cap)
KLEE: WARNING: killing 9499 states (over memory cap)
KLEE: WARNING: killing 9165 states (over memory cap)
KLEE: WARNING: killing 9220 states (over memory cap)
KLEE: WARNING: killing 9280 states (over memory cap)
KLEE: WARNING: killing 9183 states (over memory cap)
KLEE: WARNING: killing 9561 states (over memory cap)
KLEE: WARNING: killing 9387 states (over memory cap)
KLEE: WARNING: killing 9366 states (over memory cap)
KLEE: WARNING: killing 9506 states (over memory cap)
KLEE: WARNING: killing 9573 states (over memory cap)
KLEE: WARNING: killing 9792 states (over memory cap)
KLEE: WARNING: killing 9930 states (over memory cap)
KLEE: WARNING: killing 9605 states (over memory cap)
KLEE: WARNING: killing 9357 states (over memory cap)
KLEE: WARNING: killing 9493 states (over memory cap)
KLEE: WARNING: killing 9629 states (over memory cap)
KLEE: WARNING: killing 9382 states (over memory cap)
KLEE: WARNING: killing 9362 states (over memory cap)
KLEE: WARNING: killing 9498 states (over memory cap)
KLEE: WARNING: killing 9556 states (over memory cap)
KLEE: WARNING: killing 9457 states (over memory cap)
KLEE: WARNING: killing 9215 states (over memory cap)
KLEE: WARNING: killing 9426 states (over memory cap)
KLEE: WARNING: killing 9562 states (over memory cap)
KLEE: WARNING: killing 9397 states (over memory cap)
KLEE: WARNING: killing 9612 states (over memory cap)
KLEE: WARNING: killing 9290 states (over memory cap)
KLEE: WARNING: killing 9577 states (over memory cap)
KLEE: WARNING: killing 9631 states (over memory cap)
KLEE: WARNING: killing 9242 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 9507 states (over memory cap)
KLEE: WARNING: killing 9719 states (over memory cap)
KLEE: WARNING: killing 9474 states (over memory cap)
KLEE: WARNING: killing 9315 states (over memory cap)
KLEE: WARNING: killing 9298 states (over memory cap)
KLEE: WARNING: killing 9360 states (over memory cap)
KLEE: WARNING: killing 9569 states (over memory cap)
KLEE: WARNING: killing 9399 states (over memory cap)
KLEE: WARNING: killing 9308 states (over memory cap)
KLEE: WARNING: killing 9596 states (over memory cap)
KLEE: WARNING: killing 9360 states (over memory cap)
