2022-03-09 11:27:02 /home/simmo/dev/goblint/sv-comp/analyzer/goblint --conf /home/simmo/dev/goblint/sv-comp/goblint-bench/index/conf/td3.json -v --disable dbg.compare_runs.glob --enable solverdiffs --compare_runs original increment knot_comb.c Custom include dirs: 1. /home/simmo/dev/goblint/sv-comp/goblint/includes (exists=true) Preprocessing files. Preprocessor cpp: is_bad=false 'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' '/home/simmo/dev/goblint/sv-comp/goblint/includes/stdlib.c' '-o' '.goblint/preprocessed/stdlib.i' 'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' '/home/simmo/dev/goblint/sv-comp/goblint/includes/pthread.c' '-o' '.goblint/preprocessed/pthread.i' 'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' 'knot_comb.c' '-o' '.goblint/preprocessed/knot_comb.i' Parsing files. Frontc is parsing .goblint/preprocessed/stdlib.i Converting CABS->CIL Frontc is parsing .goblint/preprocessed/pthread.i Converting CABS->CIL Frontc is parsing .goblint/preprocessed/knot_comb.i Converting CABS->CIL Pre-merging (0) .goblint/preprocessed/stdlib.i Pre-merging (1) .goblint/preprocessed/pthread.i Pre-merging (2) .goblint/preprocessed/knot_comb.i :-1: Warning: Incompatible declaration for pthread_mutex_init (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:781 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic Failed assumption that union __anonunion_pthread_mutex_t_335460617 and union __anonunion_pthread_mutex_t_5 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 8 != 6.) union __anonunion_pthread_mutex_t_335460617 { struct __pthread_mutex_s __data ; char __size[40] ; long __align ; }; union __anonunion_pthread_mutex_t_5 { struct __pthread_mutex_s __data ; char __size[24] ; long __align ; }; :-1: Warning: Incompatible declaration for pthread_mutex_destroy (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:786 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic Failed assumption that union __anonunion_pthread_mutex_t_335460617 and union __anonunion_pthread_mutex_t_5 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 8 != 6.) union __anonunion_pthread_mutex_t_335460617 { struct __pthread_mutex_s __data ; char __size[40] ; long __align ; }; union __anonunion_pthread_mutex_t_5 { struct __pthread_mutex_s __data ; char __size[24] ; long __align ; }; :-1: Warning: Incompatible declaration for pthread_mutex_lock (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:794 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic Failed assumption that union __anonunion_pthread_mutex_t_335460617 and union __anonunion_pthread_mutex_t_5 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 8 != 6.) union __anonunion_pthread_mutex_t_335460617 { struct __pthread_mutex_s __data ; char __size[40] ; long __align ; }; union __anonunion_pthread_mutex_t_5 { struct __pthread_mutex_s __data ; char __size[24] ; long __align ; }; :-1: Warning: Incompatible declaration for pthread_mutex_unlock (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:835 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic Failed assumption that union __anonunion_pthread_mutex_t_335460617 and union __anonunion_pthread_mutex_t_5 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 8 != 6.) union __anonunion_pthread_mutex_t_335460617 { struct __pthread_mutex_s __data ; char __size[40] ; long __align ; }; union __anonunion_pthread_mutex_t_5 { struct __pthread_mutex_s __data ; char __size[24] ; long __align ; }; :-1: Warning: Incompatible declaration for pthread_create (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:202 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic Failed assumption that union pthread_attr_t and union __anonunion_pthread_attr_t_4 are isomorphic (different array sizes) union pthread_attr_t { char __size[56] ; long __align ; }; union __anonunion_pthread_attr_t_4 { char __size[36] ; long __align ; }; :-1: Warning: Incompatible declaration for pthread_attr_init (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:285 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic Failed assumption that union pthread_attr_t and union __anonunion_pthread_attr_t_4 are isomorphic (different array sizes) union pthread_attr_t { char __size[56] ; long __align ; }; union __anonunion_pthread_attr_t_4 { char __size[36] ; long __align ; }; :-1: Warning: Incompatible declaration for pthread_attr_setdetachstate (from .goblint/preprocessed/knot_comb.i(2)). Previous was at /usr/include/pthread.h:297 (from .goblint/preprocessed/pthread.i (1)) Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic Failed assumption that union pthread_attr_t and union __anonunion_pthread_attr_t_4 are isomorphic (different array sizes) union pthread_attr_t { char __size[56] ; long __align ; }; union __anonunion_pthread_attr_t_4 { char __size[36] ; long __align ; }; Final merging phase (0): .goblint/preprocessed/stdlib.i Final merging phase (1): .goblint/preprocessed/pthread.i Final merging phase (2): .goblint/preprocessed/knot_comb.i Constructors: read_config, init_cycle_clock, init_debug Adding constructors to: main And now... the Goblin! Startfuns: [main] Exitfuns: [] Otherfuns: [] Using new format for phases! Activated analyses for phase 0: expRelation, base, threadid, threadflag, threadreturn, escape, mutex, access, mallocWrapper Activated transformations for phase 0: Generating the control flow graph. Initializing 44 globals. Executing 53 assigns. Unmarshalling original/solver.marshalled... If type of content changed, this will result in a segmentation fault! Unmarshalling increment/solver.marshalled... If type of content changed, this will result in a segmentation fault! Comparing precision of original (left) with increment (right) as EqConstrSys: node 291 "! done" on knot_comb.c:586:3-651:3: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: line = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} Map: tmp = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}. node 291 "! done" on knot_comb.c:586:3-651:3: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: line = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} Map: tmp = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}. node 359 "return (result);" on knot_comb.c:652:3-652:18: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: line = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} Map: tmp = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}. node 359 "return (result);" on knot_comb.c:652:3-652:18: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{(alloc@sid:788)}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{(alloc@sid:788)}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{(alloc@sid:788)}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{(alloc@sid:788)}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main], {thread_process_client}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: line = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} Map: tmp = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}. node 359 "return (result);" on knot_comb.c:652:3-652:18: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main], {thread_process_client, thread_main}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main], {thread_process_client, thread_main}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main], {thread_process_client, thread_main}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main], {thread_process_client, thread_main}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Not {0}([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: line = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} Map: tmp = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}. node 294 "tmp = input_get_line(& state);" on knot_comb.c:587:5-587:34: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (0,[0,0]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (0,[0,0]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (0,[0,0]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main, thread_process_client], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (0,[0,0]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: line = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} Map: tmp = HoarePO: {state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}. node 291 "! done" on knot_comb.c:586:3-651:3: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} diff: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, thread_main_autospawn], {thread_process_client}, bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { result -> (Unknown int([-31,31]),[0,2147483647]) done -> (Unknown int([0,7]),[0,1]) state -> mapping { buf -> (Array: (Unknown int([-7,7]),[-128,127]), (512,[512,512])) socket -> (Unknown int([-31,31]),[0,2147483647]) used -> (Unknown int([-31,31]),[-2147483648,2147483647]) valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) } line -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} tmp -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} method -> {&state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} url -> {NULL, ?} protocol -> {NULL, ?} version -> Unknown valid -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___0 -> {NULL, ?} tmp___1 -> {NULL, ?} tmp___2 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___3 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___4 -> (Unknown int([-31,31]),[-2147483648,2147483647]) tmp___5 -> (Unknown int([0,32]),[0,4294967295]) request -> mapping { closed -> (Unknown int([0,7]),[0,2147483647]) socket -> (Unknown int([-31,31]),[0,2147483647]) url -> (Array: (Unknown int([-7,7]),[-128,127]), (80,[80,80])) version -> (Unknown int([0,7]),[0,4294967295]) } } Parameter { request -> {&request} } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, Comparison summary: original less precise than increment (more precise: 0, less precise: 32, total: 4008) [Warning][Deadcode] Function "fstat" will never be called: 2LoC (knot_comb.c:245:1-252:1) [Warning][Deadcode] Function "cache_new" will never be called: 46LoC (knot_comb.c:278:1-351:1) [Warning][Deadcode] Function "cache_add" will never be called: 18LoC (knot_comb.c:352:1-381:1) [Warning][Deadcode] Function "cache_remove" will never be called: 22LoC (knot_comb.c:382:1-419:1) [Warning][Deadcode] Function "cache_evict" will never be called: 7LoC (knot_comb.c:420:1-434:1) [Warning][Deadcode] Function "cache_find" will never be called: 2LoC (knot_comb.c:435:1-442:1) [Warning][Deadcode] Function "cache_use" will never be called: 4LoC (knot_comb.c:443:1-453:1) [Warning][Deadcode] Function "cache_finish_get" will never be called: 4LoC (knot_comb.c:454:1-463:1) [Warning][Deadcode] Function "cache_get" will never be called: 16LoC (knot_comb.c:476:1-501:1) [Warning][Deadcode] Function "cache_entry_addref" will never be called: 5LoC (knot_comb.c:502:1-513:1) [Warning][Deadcode] Function "cache_entry_release" will never be called: 13LoC (knot_comb.c:514:1-534:1) [Warning][Deadcode] Function "get_request_entry" will never be called: 6LoC (knot_comb.c:925:1-939:1) [Warning][Deadcode] Function "process_client_cache" will never be called: 39LoC (knot_comb.c:940:1-1006:1) [Warning][Deadcode] Function "real_toutput" will never be called: 6LoC (knot_comb.c:1384:1-1397:1) [Warning][Deadcode] Function "real_debug" will never be called: 6LoC (knot_comb.c:1398:1-1411:1) [Warning][Deadcode] Function "warning" will never be called: 4LoC (knot_comb.c:1422:1-1431:1) [Warning][Deadcode] Function "DefaultAllocEntry" will never be called: 2LoC (knot_comb.c:1596:1-1603:1) [Warning][Deadcode] Function "DefaultFreeEntry" will never be called: 3LoC (knot_comb.c:1604:1-1613:1) [Warning][Deadcode] Function "PL_HashTableDestroy" will never be called: 14LoC (knot_comb.c:1663:1-1689:1) [Warning][Deadcode] Function "PL_HashTableRawLookup" will never be called: 18LoC (knot_comb.c:1690:1-1722:1) [Warning][Deadcode] Function "PL_HashTableRawLookupConst" will never be called: 13LoC (knot_comb.c:1723:1-1749:1) [Warning][Deadcode] Function "PL_HashTableRawAdd" will never be called: 35LoC (knot_comb.c:1750:1-1803:1) [Warning][Deadcode] Function "PL_HashTableAdd" will never be called: 13LoC (knot_comb.c:1804:1-1829:1) [Warning][Deadcode] Function "PL_HashTableRawRemove" will never be called: 31LoC (knot_comb.c:1830:1-1879:1) [Warning][Deadcode] Function "PL_HashTableRemove" will never be called: 7LoC (knot_comb.c:1880:1-1895:1) [Warning][Deadcode] Function "PL_HashTableLookup" will never be called: 6LoC (knot_comb.c:1896:1-1910:1) [Warning][Deadcode] Function "PL_HashTableLookupConst" will never be called: 6LoC (knot_comb.c:1911:1-1925:1) [Warning][Deadcode] Function "PL_HashTableEnumerateEntries" will never be called: 28LoC (knot_comb.c:1926:1-1976:1) [Warning][Deadcode] Function "PL_HashTableDump" will never be called: 2LoC (knot_comb.c:1977:1-1985:1) [Warning][Deadcode] Function "PL_HashString" will never be called: 6LoC (knot_comb.c:1986:1-1999:1) [Warning][Deadcode] Function "PL_CompareStrings" will never be called: 2LoC (knot_comb.c:2000:1-2007:1) [Warning][Deadcode] Function "PL_CompareValues" will never be called: 1LoC (knot_comb.c:2008:1-2014:1) [Warning][Unknown] Calculated state for undefined function: unexpected node Statement g_conn_active --; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement tmp___0 = pthread_create((pthread_t * __restrict )(& thread), (pthread_attr_t___0 const * __restrict )(& attr), & thread_process_client, (void * __restrict )((void *)c)); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement if (rv != 0) { { assert_failed("knot.c", 472U, (char const *)"accept_loop", "rv == 0"); } } [Warning][Unknown] Calculated state for undefined function: unexpected node Statement perror((char const *)"setsockopt"); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement g_conn_active ++; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement c = 0; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement pthread_attr_init(& attr); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement assert_failed("knot.c", 472U, (char const *)"accept_loop", "rv == 0"); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement if (! attr_init_done) { { pthread_attr_init(& attr); rv = pthread_attr_setdetachstate(& attr, 1); } if (rv != 0) { { assert_failed("knot.c", 472U, (char const *)"accept_loop", "rv == 0"); } } { attr_init_done = 1; } } [Warning][Unknown] Calculated state for undefined function: unexpected node Statement close(c); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement if (tmp___0 < 0) { { g_conn_fail ++; g_conn_active --; close(c); } } [Warning][Unknown] Calculated state for undefined function: unexpected node Statement c = accept(s, (struct sockaddr * __restrict )((struct sockaddr *)(& caddr)), (socklen_t * __restrict )(& len)); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement rv = pthread_attr_setdetachstate(& attr, 1); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement if (tmp < 0) { { perror((char const *)"setsockopt"); } goto while_continue; } [Warning][Unknown] Calculated state for undefined function: unexpected node Statement optval = 1; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement perror((char const *)"accept"); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement g_conn_fail ++; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement if (c < 0) { { perror((char const *)"accept"); } goto while_continue; } [Warning][Unknown] Calculated state for undefined function: unexpected node Statement tmp = setsockopt(c, 6, 1, (void const *)(& optval), (socklen_t )sizeof(optval)); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement process_client(c); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement attr_init_done = 1; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement len = (int )sizeof(caddr); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement g_conn_open ++; [Warning][Unknown] Calculated state for undefined function: unexpected node Statement if (g_spawn_on_demand) { if (! attr_init_done) { { pthread_attr_init(& attr); rv = pthread_attr_setdetachstate(& attr, 1); } if (rv != 0) { { assert_failed("knot.c", 472U, (char const *)"accept_loop", "rv == 0"); } } { attr_init_done = 1; } } { tmp___0 = pthread_create((pthread_t * __restrict )(& thread), (pthread_attr_t___0 const * __restrict )(& attr), & thread_process_client, (void * __restrict )((void *)c)); } if (tmp___0 < 0) { { g_conn_fail ++; g_conn_active --; close(c); } } } else { { process_client(c); close(c); g_conn_active --; } } [Warning][Race] Memory location g_conn_active@knot_comb.c:776:12-776:26 (race with conf. 110): read with [] (conf. 110) (knot_comb.c:1069:3-1069:19) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1069:3-1069:19) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1069:3-1069:19) read with thread:[main] (conf. 110) (knot_comb.c:1282:7-1282:34) read with [] (conf. 110) (knot_comb.c:1098:5-1098:21) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1098:5-1098:21) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1098:5-1098:21) read with [] (conf. 110) (knot_comb.c:1118:9-1118:25) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1118:9-1118:25) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1118:9-1118:25) read with [] (conf. 110) (knot_comb.c:1124:7-1124:23) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1124:7-1124:23) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1124:7-1124:23) write with [] (conf. 110) (knot_comb.c:1069:3-1069:19) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1069:3-1069:19) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1069:3-1069:19) write with [] (conf. 110) (knot_comb.c:1098:5-1098:21) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1098:5-1098:21) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1098:5-1098:21) write with [] (conf. 110) (knot_comb.c:1118:9-1118:25) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1118:9-1118:25) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1118:9-1118:25) write with [] (conf. 110) (knot_comb.c:1124:7-1124:23) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1124:7-1124:23) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1124:7-1124:23) [Warning][Race] Memory location g_conn_open@knot_comb.c:773:12-773:24 (race with conf. 110): read with thread:[main] (conf. 110) (knot_comb.c:1276:7-1276:30) read with [] (conf. 110) (knot_comb.c:1097:5-1097:19) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1097:5-1097:19) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1097:5-1097:19) write with thread:[main] (conf. 110) (knot_comb.c:1277:7-1277:22) write with [] (conf. 110) (knot_comb.c:1097:5-1097:19) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1097:5-1097:19) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1097:5-1097:19) [Warning][Race] Memory location attr.__align@knot_comb.c:1076:23-1076:28 (race with conf. 90): write with [] (conf. 90) (knot_comb.c:1107:9-1107:34) write with thread:[main, thread_main_autospawn] (conf. 90) (knot_comb.c:1107:9-1107:34) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1107:9-1107:34) write with [] (conf. 90) (knot_comb.c:1108:9-1108:52) write with thread:[main, thread_main_autospawn] (conf. 90) (knot_comb.c:1108:9-1108:52) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1108:9-1108:52) [Warning][Race] Memory location thread@knot_comb.c:1077:18-1077:25 (race with conf. 110): write with [] (conf. 90) (knot_comb.c:1114:7-1115:89) write with thread:[main, thread_main_autospawn] (conf. 90) (knot_comb.c:1114:7-1115:89) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1114:7-1115:89) write with [] (conf. 110) (knot_comb.c:1114:7-1115:89) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1114:7-1115:89) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1114:7-1115:89) [Warning][Race] Memory location attr_init_done@knot_comb.c:1075:12-1075:27 (race with conf. 110): read with [] (conf. 110) (knot_comb.c:1106:7-1113:7) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1106:7-1113:7) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1106:7-1113:7) write with [] (conf. 110) (knot_comb.c:1112:9-1112:27) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1112:9-1112:27) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1112:9-1112:27) [Warning][Race] Memory location ticks_rdiff@knot_comb.c:1327:12-1327:24 (race with conf. 110): read with [] (conf. 110) (knot_comb.c:1353:3-1353:29) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1353:3-1353:29) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1353:3-1353:29) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1353:3-1353:29) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1353:3-1353:29) read with thread:[main] (conf. 110) (knot_comb.c:1353:3-1353:29) read with [] (conf. 110) (knot_comb.c:1380:3-1380:31) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1380:3-1380:31) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1380:3-1380:31) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1380:3-1380:31) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1380:3-1380:31) read with thread:[main] (conf. 110) (knot_comb.c:1380:3-1380:31) write with [] (conf. 110) (knot_comb.c:1380:3-1380:31) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1380:3-1380:31) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1380:3-1380:31) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1380:3-1380:31) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1380:3-1380:31) write with thread:[main] (conf. 110) (knot_comb.c:1380:3-1380:31) [Warning][Race] Memory location g_conn_succeed@knot_comb.c:775:12-775:27 (race with conf. 110): read with [] (conf. 110) (knot_comb.c:1033:7-1033:24) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1033:7-1033:24) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1033:7-1033:24) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1033:7-1033:24) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1033:7-1033:24) read with thread:[main] (conf. 110) (knot_comb.c:1278:7-1278:36) write with [] (conf. 110) (knot_comb.c:1033:7-1033:24) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1033:7-1033:24) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1033:7-1033:24) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1033:7-1033:24) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1033:7-1033:24) write with thread:[main] (conf. 110) (knot_comb.c:1279:7-1279:25) [Warning][Race] Memory location vrnow_prev@knot_comb.c:1329:19-1329:30 (race with conf. 110): write with [] (conf. 110) (knot_comb.c:1378:3-1378:21) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1378:3-1378:21) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1378:3-1378:21) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1378:3-1378:21) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1378:3-1378:21) write with thread:[main] (conf. 110) (knot_comb.c:1378:3-1378:21) [Warning][Race] Memory location (alloc@sid:788).s@knot_comb.c:1252:7-1252:37 (race with conf. 110): write with [] (conf. 90) (knot_comb.c:1148:3-1148:22) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1148:3-1148:22) read with [] (conf. 110) (knot_comb.c:1147:3-1147:15) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1147:3-1147:15) write with thread:[main] (conf. 110) (knot_comb.c:1257:7-1257:19) [Warning][Race] Memory location g_bytes_sent@knot_comb.c:779:11-779:24 (race with conf. 110): read with [] (conf. 110) (knot_comb.c:918:7-918:42) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:918:7-918:42) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:918:7-918:42) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:918:7-918:42) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:918:7-918:42) read with [] (conf. 110) (knot_comb.c:1045:11-1045:42) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1045:11-1045:42) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1045:11-1045:42) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1045:11-1045:42) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1045:11-1045:42) read with thread:[main] (conf. 110) (knot_comb.c:1274:7-1274:32) write with [] (conf. 110) (knot_comb.c:918:7-918:42) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:918:7-918:42) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:918:7-918:42) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:918:7-918:42) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:918:7-918:42) write with [] (conf. 110) (knot_comb.c:1045:11-1045:42) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1045:11-1045:42) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1045:11-1045:42) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1045:11-1045:42) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1045:11-1045:42) write with thread:[main] (conf. 110) (knot_comb.c:1275:7-1275:25) [Warning][Race] Memory location (alloc@sid:788).id@knot_comb.c:1252:7-1252:37 (race with conf. 110): write with [] (conf. 90) (knot_comb.c:1148:3-1148:22) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1148:3-1148:22) read with [] (conf. 110) (knot_comb.c:1146:3-1146:17) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1146:3-1146:17) write with thread:[main] (conf. 110) (knot_comb.c:1256:7-1256:20) [Warning][Race] Memory location attr.__size[?]@knot_comb.c:1076:23-1076:28 (race with conf. 90): write with [] (conf. 90) (knot_comb.c:1107:9-1107:34) write with thread:[main, thread_main_autospawn] (conf. 90) (knot_comb.c:1107:9-1107:34) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1107:9-1107:34) write with [] (conf. 90) (knot_comb.c:1108:9-1108:52) write with thread:[main, thread_main_autospawn] (conf. 90) (knot_comb.c:1108:9-1108:52) write with thread:[main, thread_main] (conf. 90) (knot_comb.c:1108:9-1108:52) [Warning][Race] Memory location g_conn_fail@knot_comb.c:774:12-774:24 (race with conf. 110): read with [] (conf. 110) (knot_comb.c:1035:7-1035:21) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1035:7-1035:21) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1035:7-1035:21) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1035:7-1035:21) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1035:7-1035:21) read with [] (conf. 110) (knot_comb.c:1058:5-1058:19) read with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1058:5-1058:19) read with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1058:5-1058:19) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1058:5-1058:19) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1058:5-1058:19) read with thread:[main] (conf. 110) (knot_comb.c:1280:7-1280:30) read with [] (conf. 110) (knot_comb.c:1117:9-1117:23) read with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1117:9-1117:23) read with thread:[main, thread_main] (conf. 110) (knot_comb.c:1117:9-1117:23) write with [] (conf. 110) (knot_comb.c:1035:7-1035:21) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1035:7-1035:21) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1035:7-1035:21) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1035:7-1035:21) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1035:7-1035:21) write with [] (conf. 110) (knot_comb.c:1058:5-1058:19) write with thread:[main, thread_main_autospawn, thread_process_client] (conf. 110) (knot_comb.c:1058:5-1058:19) write with thread:[main, thread_main, thread_process_client] (conf. 110) (knot_comb.c:1058:5-1058:19) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1058:5-1058:19) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1058:5-1058:19) write with thread:[main] (conf. 110) (knot_comb.c:1281:7-1281:22) write with [] (conf. 110) (knot_comb.c:1117:9-1117:23) write with thread:[main, thread_main_autospawn] (conf. 110) (knot_comb.c:1117:9-1117:23) write with thread:[main, thread_main] (conf. 110) (knot_comb.c:1117:9-1117:23) Summary for all memory locations: safe: 8 vulnerable: 2 unsafe: 11 ------------------- total: 21 vars = 0 evals = 0 narrow_reuses = 0 aborts = 0 Timings: TOTAL 0.961 s parse 0.014 s convert to CIL 0.013 s analysis 0.935 s global_inits 0.006 s warn_global 0.005 s access 0.005 s Timing used Memory statistics: total=1186.36MB, max=190.42MB, minor=1170.01MB, major=180.68MB, promoted=164.32MB minor collections=563 major collections=11 compactions=0