m.c: (in function t) m.c:9:1: Index of possibly null pointer f: f m.c:8:5: Storage f may become null sizeof.c: (in function f) sizeof.c:17:1: Possible out-of-bounds store. Unable to resolve constraint: requires: : ( 2 ) >= ( 3 ) needed to satisfy precondition: requires: : maxSet ((x @ sizeof.c:17:1 ) ) >= ( 3 ) test3.c:2:6: Function t defined more than once m.c:11:1: Previous definition of t test3.c: (in function t) test3.c:9:3: Possible out-of-bounds store. Unable to resolve constraint: requires: : ( 99 ) >= ( 101 ) needed to satisfy precondition: requires: : maxSet ((g @ test3.c:9:3 ) ) >= ( 101 ) test7.c:2:6: Function t defined more than once m.c:11:1: Previous definition of t test7.c: (in function t) test7.c:6:3: Possible out-of-bounds store. Unable to resolve constraint: requires: : maxSet ((g @ test7.c:4:3 ) ) >= ( 4 ) needed to satisfy precondition: requires: : maxSet ((g @ test7.c:6:3 ) ) >= ( 2 ) test7.c:8:3: Possible out-of-bounds store. Unable to resolve constraint: requires: : maxSet ((j @ test7.c:8:3 ) ) >= ( 0 ) needed to satisfy precondition: requires: : maxSet ((j @ test7.c:8:3 ) ) >= ( 0 ) Finished LCLint checking --- 7 code errors found