Added debugfcnconstraint flag to make lclint do checking anyway.
Changed test suit to use this flag.
# Make sure .lclintrc files are not used so test results do not
# depend on local settings.
LCLINTRN = $(LCLINTP) -nof -hints -booltype "bool"
-LCLINTR = $(LCLINTRN) -exportlocal
+LCLINTR = $(LCLINTRN) -exportlocal +debugfcnconstraint
UNITTESTS = help sizeoftest bufferTest simplebufferConstraintTests moreBufferTests globalbufferannotation maxset strchr for abstptr abstract alias alttypes ansireserved argorder args blocks break cases cast \
charlit clauses commentchar compdestroy controldepth csyntax czechnames czechoslovaknames deadparam \
+++ /dev/null
-
-czechnames.c:26:5: Function budweiser name is not consistent with Czechoslovak
- naming convention.
- Function name is not consistent with Czechoslovak naming convention. (Setting
- either -czechoslovakfcns or -namechecks will suppress message)
-
-Finished LCLint checking --- 1 code error found, as expected
-
-slovaknames.c:32:5: Function budweiser name is not consistent with Czechoslovak
- naming convention.
- Function name is not consistent with Czechoslovak naming convention. (Setting
- either -czechoslovakfcns or -namechecks will suppress message)
-
-Finished LCLint checking --- 1 code error found, as expected
-
-slovaknames.c:5:5: Variable michelobLight name violates Slovak naming
- convention. Slovak prefix michelob is not the name of a type.
- Variable name is not consistent with Slovak naming convention. (Setting
- either -slovakvars or -namechecks will suppress message)
-slovaknames.c:32:5: Function budweiser name is not consistent with Czechoslovak
- naming convention.
- Function name is not consistent with Czechoslovak naming convention. (Setting
- either -czechoslovakfcns or -namechecks will suppress message)
-
-Finished LCLint checking --- 2 code errors found, as expected
czechoslovakvars
czechtypes
czechvars
+ debugfcnconstraint
declundef
deepbreak
deparrays
arrayread --- possible out of bounds read
arraywrite --- possible buffer overflow from an out of bounds write
fcnpost --- Function has the post condition
+debugfcnconstraint --- debuging constraint flas
fcnconstraint --- unresolved constraint
checkpost --- unable to verify ensures annotation
constraintlocation --- display full c expression for every constraint generated
-
-init.c:1:16: Global c[0] initialized to null value: c[0] = NULL
-init.c:1:43: Initial value of c[2][2] is type int, expects char: 3
-init.c:1:48: Global c[3] initialized to null value: c[3] = NULL
-init.c:4:23: Global st.uname initialized to null value: st.uname = NULL
-init.c:4:29: Initial value of st.y is type double, expects int: 1.2
-init.c:7:7: Initializer block for st2[0] has 3 fields, but struct { char *
- name; int [] x; char * uname;, ... } has 4 fields: "bob", { 1, 2 }, NULL
-init.c:8:19: Initial value of st2[1].x is type int, expects int []: 3
-init.c:8:22: Global st2[1].uname initialized to null value: st2[1].uname = NULL
-init.c:10:27: Initial value of a[4] is type double, expects int: 3.4
-init.c:12:34: Initial value of aa[1][1] is type double, expects int: 3.2
-init.c:14:15: Initializer block used for b[0] where int is expected: { 1, 2 }
-init.c:14:25: Initializer block used for b[1] where int is expected: { 3, 4 }
-
-Finished LCLint checking --- 12 code errors found, as expected
-
-init.c:1:16: Global c[0] initialized to null value: c[0] = NULL
-init.c:1:22: Read-only string literal storage used as initial value for
- unqualified storage: c[1] = "hullo"
-init.c:1:43: Initial value of c[2][2] is type int, expects char: 3
-init.c:1:48: Global c[3] initialized to null value: c[3] = NULL
-init.c:4:7: Read-only string literal storage used as initial value for
- unqualified storage: st.name = "bob"
-init.c:4:23: Global st.uname initialized to null value: st.uname = NULL
-init.c:4:29: Initial value of st.y is type double, expects int: 1.2
-init.c:7:7: Initializer block for st2[0] has 3 fields, but struct { char *
- name; int [] x; char * uname;, ... } has 4 fields: "bob", { 1, 2 }, NULL
-init.c:8:9: Read-only string literal storage used as initial value for
- unqualified storage: st2[1].name = "charly"
-init.c:8:19: Initial value of st2[1].x is type int, expects int []: 3
-init.c:8:22: Global st2[1].uname initialized to null value: st2[1].uname = NULL
-init.c:10:27: Initial value of a[4] is type double, expects int: 3.4
-init.c:12:34: Initial value of aa[1][1] is type double, expects int: 3.2
-init.c:14:15: Initializer block used for b[0] where int is expected: { 1, 2 }
-init.c:14:25: Initializer block used for b[1] where int is expected: { 3, 4 }
-
-Finished LCLint checking --- 15 code errors found, as expected
+++ /dev/null
-
-slovaknames.c: (in function pivoYedno)
-slovaknames.c:15:11: Left operand of == is abstract type (pivo): p == 1
- An abstraction barrier is broken. If necessary, use /*@access <type>@*/ to
- allow access to an abstract type. (-abstract will suppress message)
-
-Finished LCLint checking --- 1 code error found, as expected
-
-Finished LCLint checking --- no code errors found
-
-slovaknames.c:5:5: Variable michelobLight name violates Slovak naming
- convention. Slovak prefix michelob is not the name of a type.
- Variable name is not consistent with Slovak naming convention. (Setting
- either -slovakvars or -namechecks will suppress message)
-slovaknames.c:19:5: Function samAdams name violates Slovak naming convention.
- Slovak prefix sam is not the name of a type.
- Function or iterator name is not consistent with Slovak naming convention.
- (Setting either -slovakfcns or -namechecks will suppress message)
-slovaknames.c:32:5: Function budweiser name is not consistent with Slovak
- naming convention. Accessible types: pivo
- Function or iterator name is not consistent with Slovak naming convention.
- (Setting either -slovakfcns or -namechecks will suppress message)
-
-Finished LCLint checking --- 3 code errors found, as expected
-
-slovaknames.c:19:5: Function samAdams name violates Slovak naming convention.
- Slovak prefix sam is not the name of a type.
- Function or iterator name is not consistent with Slovak naming convention.
- (Setting either -slovakfcns or -namechecks will suppress message)
-slovaknames.c:32:5: Function budweiser name is not consistent with Slovak
- naming convention. Accessible types: pivo
- Function or iterator name is not consistent with Slovak naming convention.
- (Setting either -slovakfcns or -namechecks will suppress message)
-
-Finished LCLint checking --- 2 code errors found, as expected
-
-slovaknames.c:4:5: Variable pivoPyet name violates Slovak naming convention.
- Slovak prefix pivo names an abstract type that is not accessible.
- Use +accessslovak to allow access to type <t> in functions named <t>_<name>.
-slovaknames.c:5:5: Variable michelobLight name violates Slovak naming
- convention. Slovak prefix michelob is not the name of a type.
- Variable name is not consistent with Slovak naming convention. (Setting
- either -slovakvars or -namechecks will suppress message)
-slovaknames.c:8:17: Constant pivoDevenast name violates Slovak naming
- convention. Slovak prefix pivo names an abstract type that is not
- accessible.
- Use +accessslovak to allow access to type <t> in functions named <t>_<name>.
-slovaknames.c:11:6: Function pivoYedno name violates Slovak naming convention.
- Slovak prefix pivo names an abstract type that is not accessible.
- Use +accessslovak to allow access to type <t> in functions named <t>_<name>.
-slovaknames.c: (in function pivoYedno)
-slovaknames.c:15:11: Left operand of == is abstract type (pivo): p == 1
- An abstraction barrier is broken. If necessary, use /*@access <type>@*/ to
- allow access to an abstract type. (-abstract will suppress message)
-slovaknames.c:19:5: Function samAdams name violates Slovak naming convention.
- Slovak prefix sam is not the name of a type.
-slovaknames.c:32:5: Function budweiser name is not consistent with Slovak
- naming convention. Accessible types: pivo
-
-Finished LCLint checking --- 7 code errors found, as expected
andersk / splint.git / commitdiff
