-
Notifications
You must be signed in to change notification settings - Fork 37
Issues: viperproject/silicon
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Avoid linear scan in isKnownToBeTrue
enhancement
New feature or request
performance
#522
opened Nov 11, 2020 by
fpoli
Retire state consolidation hack
enhancement
New feature or request
#510
opened Jul 31, 2020 by
mschwerhoff
Retire resource havocking hack
enhancement
New feature or request
major
#407
opened Dec 28, 2019 by
viper-admin
Outputs differ between Silicon and Carbon
enhancement
New feature or request
minor
#366
opened Jan 21, 2019 by
viper-admin
Deprecate 'new' and its semantics
enhancement
New feature or request
major
#344
opened Jun 29, 2018 by
viper-admin
bad recursive function definition not (apparently) available
enhancement
New feature or request
minor
z3
#330
opened May 8, 2018 by
viper-admin
Replace "Verification Aborted Exceptionally" and "Unknown Reason"/loglevel-related messages with more-specific messages
enhancement
New feature or request
logging-reporting-ide
#306
opened Sep 8, 2017 by
viper-admin
Support Magic Wand Snapshots for Wands That Were Inhaled
enhancement
New feature or request
magic-wands
major
#304
opened Sep 6, 2017 by
viper-admin
Compress the heap more aggressively and/or support secondary permissions
enhancement
New feature or request
major
permissions
#286
opened May 15, 2017 by
viper-admin
block_array examples exhibit unstable Z3 performance - potentially related to non-linear arithmetic
enhancement
New feature or request
examples
minor
#266
opened Feb 1, 2017 by
viper-admin
Don't warn about unresolved expressions in functions if they are unreachable/dead code
enhancement
New feature or request
logging-reporting-ide
major
#261
opened Dec 13, 2016 by
viper-admin
Optimize addition of injectivity checks / inverse functions
enhancement
New feature or request
major
quantified-permissions
#244
opened Aug 6, 2016 by
viper-admin
Frame heap assumptions into read-only loops
enhancement
New feature or request
major
permissions
#218
opened Feb 22, 2016 by
viper-admin
Non-null assumptions from predicates unfolding predicates inside functions
enhancement
New feature or request
minor
#112
opened Aug 19, 2014 by
viper-admin
Make sequence axiomatisation common with Carbon
enhancement
New feature or request
major
#104
opened Jul 14, 2014 by
viper-admin
Disjunctive aliasing constraints and permissions
enhancement
New feature or request
minor
more-complete-exhale
#72
opened Feb 21, 2014 by
viper-admin
Non-aliasing assumptions from unfolding predicates
enhancement
New feature or request
incompleteness
#40
opened Jul 31, 2013 by
viper-admin
Finding predicates with arguments in the heap
enhancement
New feature or request
minor
more-complete-exhale
#36
opened Jul 25, 2013 by
viper-admin
Reporting multiple errors/continue verification assuming that a failed assertion holds
enhancement
New feature or request
major
#34
opened Jul 23, 2013 by
viper-admin
New objects and non-aliasing information
enhancement
New feature or request
minor
#29
opened May 24, 2013 by
viper-admin
Permission incompletenesses
enhancement
New feature or request
incompleteness
minor
permissions
#16
opened Apr 15, 2013 by
viper-admin
ProTip!
Exclude everything labeled
bug
with -label:bug.