viperproject/carbon issues and pull requests

#314 - Set exit status correctly when exiting Carbon.main

Issue - State: closed - Opened by viper-admin about 9 years ago - 1 comment
Labels: merged, pull request

#313 - Default

Issue - State: closed - Opened by viper-admin about 9 years ago - 1 comment
Labels: merged, pull request

#312 - Add support for creating Carbon verifier by reflection.

Issue - State: closed - Opened by viper-admin about 9 years ago - 1 comment
Labels: merged, pull request

#311 - BOOGIE_EXE and Z3_EXE can be overridden by env variables

Issue - State: closed - Opened by viper-admin about 9 years ago
Labels: pull request, declined

#310 - Launch script is now path independent (can be called from anywhere).

Issue - State: closed - Opened by viper-admin about 9 years ago - 1 comment
Labels: merged, pull request

#309 - Added support for passing multiple arguments to Boogie.

Issue - State: closed - Opened by viper-admin about 9 years ago - 1 comment
Labels: merged, pull request

#308 - Bumped Scala version to 2.11.7.

Issue - State: closed - Opened by viper-admin about 9 years ago - 1 comment
Labels: merged, pull request

#307 - Improvement of carbon.bat startup script.

Issue - State: closed - Opened by viper-admin about 9 years ago
Labels: merged, pull request

#306 - Added README.

Issue - State: closed - Opened by viper-admin over 9 years ago - 8 comments
Labels: merged, pull request

#305 - Improved support for InhaleExhale expressions

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: merged, pull request

#304 - expressed two implications with same condition by just one implication using explicit brackets

Issue - State: closed - Opened by viper-admin over 9 years ago - 1 comment
Labels: merged, pull request

#303 - "good mask" bug fix

Issue - State: closed - Opened by viper-admin over 9 years ago - 1 comment
Labels: merged, pull request

#302 - Bug fix: field translation is not lazy anymore.

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: merged, pull request

#301 - Bug fix: trying to completely reset DefaultFuncPredModule state.

Issue - State: closed - Opened by viper-admin over 9 years ago - 1 comment
Labels: merged, pull request

#300 - Bug fix: verifier does not need to be recreated between runs (issue #47).

Issue - State: closed - Opened by viper-admin over 9 years ago - 5 comments
Labels: merged, pull request

#299 - Loop Variables Fix

Issue - State: closed - Opened by viper-admin over 9 years ago - 1 comment
Labels: pull request, declined

#298 - Removed fraction optimization and added test case

Issue - State: closed - Opened by viper-admin over 9 years ago - 1 comment
Labels: merged, pull request

#297 - Make Carbon compile again and add Bash script for running Carbon

Issue - State: closed - Opened by viper-admin about 11 years ago - 7 comments
Labels: merged, pull request

#280 - Verification is taking more time than usual

Issue - State: open - Opened by viper-admin over 5 years ago - 7 comments
Labels: enhancement, major, performance

#81 - perm expressions (for field locations) don't generate checks that the receiver is non-null

Issue - State: closed - Opened by viper-admin almost 9 years ago - 2 comments
Labels: bug, invalid, minor

#80 - Carbon ignores permissions when unfolding `acc(predicate, perm)`

Issue - State: closed - Opened by viper-admin almost 9 years ago - 3 comments
Labels: bug, major

#79 - all/issues//silicon//0045.sil does not terminate

Issue - State: closed - Opened by viper-admin about 9 years ago - 4 comments
Labels: bug, minor

#78 - Carbon rejects a valid assertion that Silicon accepts

Issue - State: closed - Opened by viper-admin about 9 years ago - 3 comments
Labels: bug, major

#77 - Third party tests fail

Issue - State: open - Opened by viper-admin about 9 years ago - 3 comments
Labels: bug, major

#76 - Incompleteness with respect to quantifiers in functions ?

Issue - State: open - Opened by viper-admin about 9 years ago - 1 comment
Labels: bug, major

#75 - unsoundness with perm in predicates / functions

Issue - State: closed - Opened by viper-admin about 9 years ago - 4 comments
Labels: bug, wontfix, major

#74 - Crash when loop contains variable declaration

Issue - State: closed - Opened by viper-admin about 9 years ago - 3 comments
Labels: bug, major

#73 - After exhale information about unrelated variables is lost

Issue - State: open - Opened by viper-admin about 9 years ago - 1 comment
Labels: bug, critical

#72 - Crash when postcondition contains permission typed field

Issue - State: closed - Opened by viper-admin over 9 years ago - 5 comments
Labels: bug, critical

#71 - iterator2.chalice test fails

Issue - State: open - Opened by viper-admin over 9 years ago - 1 comment
Labels: bug, major

#70 - Loop invariant is not checked for wellformedness

Issue - State: open - Opened by viper-admin over 9 years ago - 2 comments
Labels: bug, major

#69 - Post condition violation is not reported for not wellformed functions

Issue - State: open - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#68 - “function.not.wellformed” → “not.wellformed” for not wellformed function contracts

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#67 - InhaleExhale in contracts not always checked for wellformedness

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#66 - Fails to infer that this != null inside InhaleExhale expression

Issue - State: closed - Opened by viper-admin over 9 years ago - 7 comments
Labels: bug, blocker

#65 - Crash when verifying conjunction of InhaleExhale expressions

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#64 - Function precondition fails to verify in InhaleExhale expression

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, duplicate, major

#63 - Crash when verifying exhale with unfolding expressions before other conjuncts

Issue - State: closed - Opened by viper-admin over 9 years ago - 10 comments
Labels: bug, critical

#62 - Carbon crashes if Silver program contains an empty constraining block

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: bug, major

#61 - producer-consumer.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 4 comments
Labels: bug, major

#60 - workitem-10199.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: bug, major

#59 - Unfolding under "old" doesn't work correctly

Issue - State: closed - Opened by viper-admin over 9 years ago - 12 comments
Labels: bug, major

#58 - Permissions under quantifiers are not supported.

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: bug, invalid, major

#57 - nestedPredicates.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, invalid, major

#56 - dining-philosophers.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: bug, major

#55 - linkedlist.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 4 comments
Labels: bug, major

#54 - scaling.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: bug, major

#53 - unfolding_old_heap.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 4 comments
Labels: bug, duplicate, major

#52 - Incorrect wellformedness check: precondition can frame postcondition

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#51 - linked_list.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#50 - join_function_returning_token.chalice test fails

Issue - State: closed - Opened by viper-admin over 9 years ago - 6 comments
Labels: bug, major

#49 - When folding is used, it is possible to assert false.

Issue - State: closed - Opened by viper-admin over 9 years ago - 9 comments
Labels: bug, major

#48 - Carbon runs out of memory when trying to verify Injection.chalice

Issue - State: closed - Opened by viper-admin over 9 years ago - 6 comments
Labels: bug, invalid, major

#47 - Heisenbug: Carbon crashes with NoSuchElementException.

Issue - State: closed - Opened by viper-admin over 9 years ago - 3 comments
Labels: bug, major

#46 - Mixing sets and sequences doesn't work

Issue - State: closed - Opened by viper-admin over 9 years ago - 4 comments
Labels: bug, minor

#45 - Non-recursive functions are not triggered when predicates from their preconditions get (un)folded

Issue - State: closed - Opened by viper-admin over 9 years ago - 4 comments
Labels: bug, major

#44 - requirement failures in tests cannot be captured by testing infrastructure

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: enhancement, major

#43 - Reject negative permission values when (un)folding predicates

Issue - State: open - Opened by viper-admin over 9 years ago
Labels: bug, major

#42 - Perm-typed functions are not known to be at least 'none'

Issue - State: closed - Opened by viper-admin over 9 years ago - 4 comments
Labels: bug, wontfix, major

#41 - Give command-line option to retain Boogie file directly

Issue - State: closed - Opened by viper-admin over 9 years ago - 2 comments
Labels: enhancement, major

#40 - Carbon reports no errors if prover dies

Issue - State: open - Opened by viper-admin almost 10 years ago
Labels: bug, major

#39 - Conjunctions under quantifiers don't trigger reliably

Issue - State: open - Opened by viper-admin almost 10 years ago - 1 comment
Labels: bug, minor

#38 - linkedlists.sil test case takes too long (and so is currently disabled)

Issue - State: closed - Opened by viper-admin almost 10 years ago - 2 comments
Labels: bug, major

#37 - Add support for let-expressions

Issue - State: closed - Opened by viper-admin almost 10 years ago - 3 comments
Labels: enhancement, major

#36 - Add well-definedness checks for built-in axiomatisations

Issue - State: closed - Opened by viper-admin about 10 years ago - 6 comments
Labels: enhancement, minor

#35 - Carbon doesn't build without NonPositivePermission class

Issue - State: closed - Opened by viper-admin about 10 years ago - 2 comments
Labels: bug, major

#34 - sequence test cases can be unstable

Issue - State: closed - Opened by viper-admin about 10 years ago - 4 comments
Labels: bug, major

#33 - epsilon support disabled

Issue - State: closed - Opened by viper-admin about 10 years ago - 2 comments
Labels: wontfix, minor, task

#32 - Quantified variable escapes its scope

Issue - State: closed - Opened by viper-admin about 10 years ago - 2 comments
Labels: bug, wontfix, major

#31 - Insufficient permissions, maybe due to constraining-blocks and wildcards

Issue - State: closed - Opened by viper-admin about 10 years ago - 3 comments
Labels: bug, major

#30 - Predicate bodies not checked for self-framedness

Issue - State: closed - Opened by viper-admin about 10 years ago - 1 comment
Labels: bug, major

#29 - Functions for linkedlists.sil example aren't triggering enough

Issue - State: closed - Opened by viper-admin about 10 years ago - 3 comments
Labels: bug, major

#28 - Multiset axiomatisation is weak

Issue - State: closed - Opened by viper-admin about 10 years ago - 3 comments
Labels: bug, major

#27 - Normalise exceptional error messages

Issue - State: open - Opened by viper-admin about 10 years ago
Labels: enhancement, major

#26 - Enhance strength of function axioms

Issue - State: open - Opened by viper-admin about 10 years ago - 1 comment
Labels: enhancement, minor

#25 - Carbon cannot verify test case that needs the least-fixed-point semantics of recursive predicates

Issue - State: closed - Opened by viper-admin about 10 years ago - 3 comments
Labels: bug, major

#24 - Carbon queries Boogie without proper command-line arguments

Issue - State: closed - Opened by viper-admin over 10 years ago - 4 comments
Labels: bug, major

#23 - Error reporting for failing method calls

Issue - State: closed - Opened by viper-admin over 10 years ago - 3 comments
Labels: bug, minor

#22 - Improve Boogie error reporting

Issue - State: closed - Opened by viper-admin over 10 years ago - 2 comments
Labels: enhancement, major

#21 - make sequence axiomatisation common with Silicon

Issue - State: closed - Opened by viper-admin over 10 years ago - 4 comments
Labels: enhancement, minor

#20 - Enable keeping the bpl file

Issue - State: closed - Opened by viper-admin over 10 years ago - 2 comments
Labels: enhancement, major

#19 - names should be output to Boogie in a way which avoids clashes

Issue - State: open - Opened by viper-admin over 10 years ago - 4 comments
Labels: enhancement, major

#18 - Carbon does not manage to prove some assertions in AVLTree that proved in Chalice

Issue - State: open - Opened by viper-admin over 10 years ago - 1 comment
Labels: bug, major

#17 - unfolding test cases

Issue - State: closed - Opened by viper-admin over 10 years ago - 2 comments
Labels: major, task

#16 - rename check definedness of spec methods to indicate that they also inhale

Issue - State: closed - Opened by viper-admin over 10 years ago - 2 comments
Labels: minor, task

#15 - simplePartialCheckDefinedness in DefaultHeapModule needs checking

Issue - State: closed - Opened by viper-admin over 10 years ago - 3 comments
Labels: minor, task

#14 - unfolding expressions are not properly handled in method signatures

Issue - State: closed - Opened by viper-admin over 10 years ago - 2 comments
Labels: bug, major

#13 - Quantifier merging by Boogie causes errors with automatic triggers

Issue - State: closed - Opened by viper-admin over 10 years ago - 2 comments
Labels: bug, trivial

#12 - Object allocation problem, apparently caused by loops

Issue - State: closed - Opened by viper-admin almost 11 years ago - 3 comments
Labels: bug, major

#11 - Crashing with "not a permission expression: tk1.par$Testf$k$"

Issue - State: closed - Opened by viper-admin almost 11 years ago - 9 comments
Labels: bug, major

#10 - Translation from Chalice2SIL fails to verify

Issue - State: closed - Opened by viper-admin almost 11 years ago - 9 comments
Labels: bug, major

#9 - Crashing with "assertion failed: Found 2 errors, but there should be 0"

Issue - State: closed - Opened by viper-admin almost 11 years ago - 5 comments
Labels: bug, minor

#8 - well-definedness checks inside quantifiers are not general enough

Issue - State: closed - Opened by viper-admin almost 11 years ago - 3 comments
Labels: bug, major

#7 - Set-related constructs are not handled in triggers

Issue - State: closed - Opened by viper-admin almost 11 years ago - 2 comments
Labels: bug, invalid, major

#6 - Disjunction is not treated as short-circuiting in well-definedness checks

Issue - State: closed - Opened by viper-admin almost 11 years ago - 4 comments
Labels: bug, major

#5 - Exception when requiring 'none' permissions

Issue - State: closed - Opened by viper-admin about 11 years ago - 2 comments
Labels: bug, major

#4 - Exception for conditional permissions expressions

Issue - State: closed - Opened by viper-admin about 11 years ago - 2 comments
Labels: bug, major

#3 - Quantified variables inside predicate bodies do not work (unfolding generates exception)

Issue - State: closed - Opened by viper-admin about 11 years ago - 2 comments
Labels: bug, blocker

#2 - Sequence-typed fields create boogie syntax errors

Issue - State: closed - Opened by viper-admin about 11 years ago - 2 comments
Labels: bug, major

#1 - Crashing with "unparsable output from Boogie"

Issue - State: closed - Opened by viper-admin over 11 years ago - 3 comments
Labels: bug, major

GitHub / viperproject/carbon issues and pull requests