Skip to content


Subversion checkout URL

You can clone with
Download ZIP
branch: master
Commits on Sep 8, 2014
  1. Update the library interface parsing code (and aeson version)

    The old library interface parser relied in the generically-derived JSON
    parser from aeson.  Unfortunately, the format that aeson used for these
    parsers changed in 0.7.  Instead of updating all of the data, we now use
    manually-written ToJSON and FromJSON instances.  We can now safely use
    modern versions of aeson.
  2. Update to a newer version of sbv

    This one works with newer releases of z3.  No code changes required, luckily.
Commits on May 22, 2014
  1. Version updates

Commits on Oct 27, 2013
Commits on Oct 20, 2013
Commits on Aug 20, 2013
Commits on Aug 19, 2013
  1. Update two test inputs to the newer json format

    This adds a missing field (libraryAnnotations)
Commits on Aug 16, 2013
  1. Notes for future work

  2. Newline

  3. Convert Output analysis to backwards dataflow

    Matches the description in the dissertation
Commits on Aug 12, 2013
  1. Add an extra inout test

    This is from Susan.  It shouldn't work under the current formulation,
    but it happens to due to a quirk in the translation from clang.  The
    new formulation coming should fix it for any possible translation.
Commits on May 30, 2013
  1. Remove commented-out code.

Commits on May 24, 2013
Commits on May 23, 2013
  1. Remove commented out code

  2. Improve a highlighting regex

    This regular expression replaces function calls in code snippets with
    links to the called function.  This tweaks the regex to make sure the
    matched word ends at a word boundary and doesn't just highlight some
    prefix of a word.  This showed up in various places, but an example
    was deflate/deflateEnd, where deflate highlighted a prefix of
    deflateEnd, preventing deflateEnd from being correctly highlighted.
Commits on May 22, 2013
  1. Apply the transitive error analysis to all functions

    Transitive error returning functions might not return other error
    constants.  The prior version of the analysis only looked at
    functions that returned error constants.
    This change just checks every function for transitive error returns.
  2. Improve link handling in generated html reports

    Wasn't stripping off enough bitcasts, so some links were missed.
  3. Include a new error analysis option

    This option forces the analysis to never consider 0 as an error code
    (to generalize from).  It will still be reported if an error is
    definitely transformed into a zero.
Commits on May 21, 2013
  1. More expressive error actions

    Include assigning to arguments.  This code doesn't fire often due to
    the size of basic blocks (and since we only really look at nearly
    terminal blocks).
Commits on May 20, 2013
  1. Remove commented out code

    This code is obsolete reporting code (the general reporting
    infrastructure takes care of it now).
  2. Addressed fixme

  3. Eliminate empty error report summaries

    The transitive reporter would produce empty summaries;
    suppress those.
  4. Fix the boolean function detection.

    The detector flattens phi nodes into a list of values before
    inspecting them; it used to leave the phi node itself in, which
    threw off the boolean function detection.
    This change removes the phi node from the list.
  5. Aggressively remove successes from error descriptors

    Once we learn something is a success (by the new majority criterion),
    never consider a success code to be an error code, even if we
    previously thought so.
    This works because we aren't classifying boolean functions anymore.
    This change also modifies how error code summaries are used.  Before,
    only the first FAReportsErrors annotation would be used.  Now all are
    Furthermore, for transitive errors, the error action is dropped because
    only the callee takes that action - the caller does not.
Commits on May 17, 2013
  1. Only analyze functions that could return an error.

    There is now a check to ignore functions that are trivially boolean
    or always return 1 or 0.  This removes a large source of errors where
    we would classify boolean returns as error codes, polluting all
    of the results after that.
  2. Add a more selective model of success

    Now, in order to be a success indicator, a function whose error
    return is ignored must be followed by some other non-return
    non-phi non-direct-branch code.  The idea is to try to avoid flagging
    cleanup code with an ignored return code as a success.
    It may be worth expanding this so that a basic block of cleanup code
    (e.g. free; free; free;) could also be handled.
  3. Update a comment

Something went wrong with that request. Please try again.