Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added modifies clause generation for Boogie files. #267

Open
wants to merge 17 commits into
base: develop
Choose a base branch
from
Open

Added modifies clause generation for Boogie files. #267

wants to merge 17 commits into from

Commits on Oct 21, 2017

  1. Added modifies clause generation for Boogie files.

    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    5e400da View commit details
    Browse the repository at this point in the history

  2. Fixed some issues with the modifies pass and smack.c causing the memo… 

    …ry-safety regtests to fail.

The modifies pass was not handling the prelude section of Boogie files.
When the --memory-safety option is specified, this prelude section
contains a procedure called $global_allocations which modifies some
variables. Additionally, the modifies pass only adds modifies
clauses to SMACK-generated procedures that do not already have one, which
does not cover the $malloc procedure when the --memory-safety option is
set. This is directly changed in smack.c.
    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    5d6448b View commit details
    Browse the repository at this point in the history

  3. Modifies pass was improperly handling prelude section when -memory-sa… 

    …fety option is not specified.
    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    015de8b View commit details
    Browse the repository at this point in the history

  4. $malloc procedure's modifies clause included variables that should no… 

    …t have been there.
    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    8154002 View commit details
    Browse the repository at this point in the history

  5. Removed unnecessary #include header

    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    e3617e0 View commit details
    Browse the repository at this point in the history

  6. Changed name of modifies pass from GenModifies to ModAnalysis.

    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    266e82b View commit details
    Browse the repository at this point in the history

  7. Removed unnecessary empty lines.

    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    cb81255 View commit details
    Browse the repository at this point in the history

  8. Added back in /nologo and /noinfer options to Boogie command.

    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    d9393e9 View commit details
    Browse the repository at this point in the history

  9. Changed name of GenModifies.h/cpp to ModAnalysis.h/cpp

    @liammachado
    liammachado committed Oct 21, 2017
    Configuration menu
    Copy the full SHA
    cff3d8b View commit details
    Browse the repository at this point in the history

Commits on Jan 1, 2019

  1. Merge branch 'develop' into develop

    @liammachado
    liammachado authored Jan 1, 2019
    Configuration menu
    Copy the full SHA
    9d1d413 View commit details
    Browse the repository at this point in the history

  2. Changed BoogieAst to be consistent with most recent version

    @liammachado
    liammachado committed Jan 1, 2019
    Configuration menu
    Copy the full SHA
    432a3cb View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2019

  1. Merge branch 'develop' into develop

    @liammachado
    liammachado authored Jan 27, 2019
    Configuration menu
    Copy the full SHA
    7ccfb44 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2019

  1. Merge branch 'develop' of https://github.com/smackers/smack into HEAD

    @liammachado
    liammachado committed Jul 18, 2019
    Configuration menu
    Copy the full SHA
    88099dd View commit details
    Browse the repository at this point in the history

  2. Fixed formatting

    @liammachado
    liammachado committed Jul 18, 2019
    Configuration menu
    Copy the full SHA
    591137b View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2019

  1. Fixed method signature

    @liammachado
    liammachado committed Jul 19, 2019
    Configuration menu
    Copy the full SHA
    97f7fd1 View commit details
    Browse the repository at this point in the history

  2. More fixes to method signature

    @liammachado
    liammachado committed Jul 19, 2019
    Configuration menu
    Copy the full SHA
    4095a64 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2019

  1. Merge branch 'develop' into develop

    @liammachado
    liammachado authored Aug 29, 2019
    Configuration menu
    Copy the full SHA
    e370e66 View commit details
    Browse the repository at this point in the history