./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/linux-4.2-rc1.tar.xz-08_1a-drivers--net--team--team.ko-entry_point.cil.out.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/linux-4.2-rc1.tar.xz-08_1a-drivers--net--team--team.ko-entry_point.cil.out.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--net--team--team.ko-entry_point.cil.out.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-free) ) -> enabling soundness analyses "base, useAfterFree"[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-deref) ) -> enabling soundness analyses "base, memOutOfBounds"[0;0;00m
[0;34m[Info] Setting "ana.arrayoob" to true[0;0;00m
[0;34m[Info] Setting "cil.addNestedScopeAttr" to true[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-memtrack) ) -> enabling soundness analyses "memLeak"[0;0;00m
[0;34m[Info] Setting "ana.malloc.unique_address_count" to 5[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
[Error][Imprecise][Unsound] Function definition missing for __cmpxchg_wrong_size
[Error][Imprecise][Unsound] Function definition missing for __bad_percpu_size
[Error][Imprecise][Unsound] Function definition missing for __bad_size_call_parameter
[Info][Witness] couldn't parse entry: find uuid

[Info] runtime: 00:00:10.477
[Info] vars: 11143, evals: 11442

[Info] |called|=38

Memory statistics: total=22052.96MB, max=132.00MB, minor=22048.01MB, major=298.63MB, promoted=293.67MB
    minor collections=10522  major collections=19 compactions=0


[Info] runtime: 00:00:20.558
[Info] vars: 19404, evals: 18221

[Info] |called|=40

Memory statistics: total=41053.78MB, max=265.50MB, minor=41047.71MB, major=674.56MB, promoted=668.49MB
    minor collections=19584  major collections=24 compactions=0


[Info] runtime: 00:00:30.659
[Info] vars: 27832, evals: 25229

[Info] |called|=45

Memory statistics: total=59491.94MB, max=403.80MB, minor=59485.35MB, major=1028.98MB, promoted=1022.40MB
    minor collections=28378  major collections=28 compactions=0


[Info] runtime: 00:00:40.734
[Info] vars: 36131, evals: 32260

[Info] |called|=43

Memory statistics: total=78326.05MB, max=534.03MB, minor=78317.70MB, major=1398.23MB, promoted=1389.87MB
    minor collections=37359  major collections=30 compactions=0


[Info] runtime: 00:00:50.845
[Info] vars: 44351, evals: 39686

[Info] |called|=42

Memory statistics: total=96785.72MB, max=706.25MB, minor=96777.13MB, major=1751.84MB, promoted=1743.25MB
    minor collections=46163  major collections=32 compactions=0

