sample.c:11: Fresh storage x not released before
                return
   sample.c:5: Fresh storage x created
sample.c:5: Variable x declared but not used

Finished checking --- 2 code warnings, as expected

null.c:3: Dereference of possibly null pointer s: *s
   null.c:1: Storage s may become null

Finished checking --- 1 code warning, as expected

Finished checking --- no warnings

usedef.c:11: Value *x used before definition
usedef.c:13: Passed storage x not completely defined
                (*x is undefined): getVal (x)
usedef.c:15: Passed storage x not completely defined
                (*x is undefined): mysteryVal (x)

Finished checking --- 3 code warnings, as expected

usedef.c:11: Value *x used before definition
usedef.c:13: Passed storage x not completely defined
                (*x is undefined): getVal (x)

Finished checking --- 2 code warnings, as expected

bool.c:6: Test expression for if is assignment expression: i = 3
bool.c:6: Test expression for if not bool, type int: i = 3
bool.c:7: Return value type bool does not match declared type int: b1
bool.c:8: Operand of ! is non-boolean (int): !i
bool.c:8: Right operand of || is non-boolean (char *): !i || s
bool.c:10: Test expression for if not bool, type char *: s
bool.c:12: Use of == with bool variables (risks inconsistency because
              of multiple true values): b1 == b2

Finished checking --- 7 code warnings, as expected

palindrome.c:6: Cast from underlying
    abstract type mstring: (char *)s
palindrome.c:7: Function strlen expects arg
    1 to be char * gets mstring: s
palindrome.c:11: Array fetch from non-array
    (mstring): s[len - i - 1]
palindrome.c:19: Function isPalindrome
    expects arg 1 to be mstring gets char *:
    "bob"

Finished checking --- 4 code warnings, as
expected

only.c:11: Only storage glob (type int *) not released
              before assignment: glob = y
   only.c:1: Storage glob becomes only
only.c:11: Implicitly temp storage y assigned to only:
              glob = y
only.c:13: Dereference of possibly null pointer m: *m
   only.c:8: Storage m may become null
only.c:13: Variable x used after being released
   only.c:12: Storage x released
only.c:14: Implicitly temp storage z returned as only:
              z
only.c:14: Fresh storage m not released before return
   only.c:9: Fresh storage m created

Finished checking --- 6 code warnings, as expected

stack.c:12: Stack-allocated storage &loc reachable
               from return value: &loc
stack.c:12: Stack-allocated storage *x reachable from
               parameter x
   stack.c:10: Storage *x becomes stack-allocated
   storage
stack.c:12: Stack-allocated storage glob reachable
               from global glob
   stack.c:9: Storage glob becomes stack-allocated
   storage

Finished checking --- 3 code warnings, as expected

rstring.c:13: Reference counted storage returned
                 without modifying reference count: r1

Finished checking --- 1 code warning, as expected

unique.c:7: Parameter 1 (s) to function strcpy is
    declared unique but may be aliased externally by
    parameter 2 (t)

Finished checking --- 1 code warning, as expected

exposure.c:6: Function returns reference to
                 parameter e: e->name
exposure.c:6: Return value exposes rep of
                 employee: e->name
exposure.c:6: Released storage e->name reachable
                 from parameter at return point
   exposure.c:6: Storage e->name released
exposure.c:23: Suspect modification of observer
                  name: *name = toupper(*name)
   exposure.c:22: Storage *name becomes observer

Finished checking --- 4 code warnings, as
expected

modify.c:4: Undocumented modification of *y: *y = *x
modify.c:5: Suspect object listed in modifies of setx
               not modified: *x
   modify.c:1: Declaration of setx

Finished checking --- 2 code warnings, as expected

globals.c:5: Undocumented use of global glob2
globals.c:3: Global glob1 listed but not used

Finished checking --- 2 code warnings, as expected

annotglobs.c:13: Undef global globnum used before
                    definition
annotglobs.c:15: Global storage globname contains 1
    undefined field when call returns: firstname
annotglobs.c:21: Only storage globname.firstname (type
    char *) derived from killed global is not released
    (memory leak)

Finished checking --- 3 code warnings, as expected

Finished checking --- no warnings

order.c:11: Expression has undefined behavior (value of
    right operand modified by left operand): x++ * x
order.c:13: Expression has undefined behavior (left operand
    uses i, modified by right operand): y[i] = i++
order.c:14: Expression has undefined behavior (value of
    right operand modified by left operand):
    modglob() * glob
order.c:15: Expression has undefined behavior
    (unconstrained function mystery used in left operand
    may set global variable glob used in right operand):
    mystery() * glob

Finished checking --- 4 code warnings, as expected

order.c:11: Expression has undefined behavior (value
    of right operand modified by left operand):
    x++ * x
order.c:13: Expression has undefined behavior (left
    operand uses i, modified by right operand):
    y[i] = i++
order.c:14: Expression has undefined behavior (value
    of right operand modified by left operand):
    modglob() * glob

Finished checking --- 3 code warnings, as expected

loop.c:14: Suspected infinite loop.  No value used in
    loop test (x, glob1) is modified by test or loop
    body.
loop.c:15: Suspected infinite loop.  No condition
    values modified.  Modification possible through
    unconstrained calls: h

Finished checking --- 2 code warnings, as expected

loop.c:14: Suspected infinite loop.  No value used in
    loop test (x, glob1) is modified by test or loop
    body.

Finished checking --- 1 code warning, as expected

switch.c:11: Fall through case (no preceding break)
switch.c:14: Missing case in switch: DEFINITELY

Finished checking --- 2 code warnings, as expected

noeffect.c:6: Statement has no effect: y == *x
noeffect.c:7: Statement has no effect: nomodcall(x)
noeffect.c:8: Statement has no effect (possible
    undected modification through call to
    unconstrained function mysterycall):
    mysterycall(x)

Finished checking --- 3 code warnings, as expected

noeffect.c:6: Statement has no effect: y == *x
noeffect.c:7: Statement has no effect: nomodcall(x)

Finished checking --- 2 code warnings, as expected

ignore.c:8: Return value (type int) ignored: fi()
ignore.c:10: Return value (type bool) ignored: fb()

Finished checking --- 2 code warnings, as expected

ignore.c:8: Return value (type int) ignored: fi()

Finished checking --- 1 code warning, as expected

ignore.c:10: Return value (type bool) ignored: fb()

Finished checking --- 1 code warning, as expected

setChar.c:5: Likely out-of-bounds store: buf[10]
    Unable to resolve constraint:
    requires 9 >= 10
     needed to satisfy precondition:
    requires maxSet(buf @ setChar.c:5) >= 10

Finished checking --- 1 code warning, as expected

multiError.c:4: Possible out-of-bounds store: buf[2]
    Unable to resolve constraint:
    requires maxSet(buf @ multiError.c:4) >= 2
     needed to satisfy precondition:
    requires maxSet(buf @ multiError.c:4) >= 2

Finished checking --- 1 code warning, as expected

bounds.c:9: Possible out-of-bounds store:
    strcpy(str, tmp)
    Unable to resolve constraint:
    requires maxSet(str @ bounds.c:9) >=
    maxRead(getenv("MYENV") @ bounds.c:7)
     needed to satisfy precondition:
    requires maxSet(str @ bounds.c:9) >=
    maxRead(tmp @ bounds.c:9)
     derived from strcpy precondition: requires
    maxSet(<parameter 1>) >= maxRead(<parameter
    2>)

Finished checking --- 1 code warning, as expected