team-worthwhile worthwhile issues

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)

BSD 3-Clause "New" or "Revised" License

5 stars 3 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Create class DivisorNotZeroInvariant

#117 bafain opened 12 years ago
0
AstNodeCreatorHelper#createLiteral ignores assigned indexes

#116 bafain closed 12 years ago
0
NullPointerException when trying to prove {} = {}

#115 jspam closed 12 years ago
0
FunctionCallSubstitution uses legal Worthwhile identifiers for inserted return value variables

#114 bafain closed 12 years ago
1
EmptyStackException when evaluating 1/0 as expression

#113 jspam closed 12 years ago
0
ConcurrentModificationException in TimeoutProverCaller::runCleanupTasks

#112 jspam closed 12 years ago
0
Interpreter does not resolve symbols in Assumptions

#111 bafain closed 12 years ago
0
Interpreter ignores in-path assumptions

#110 bafain closed 12 years ago
3
Parse prover output for ProverResult to return AST model

#109 bafain opened 12 years ago
1
SMT error: select requires as many arguments as the size of the domain

#108 jspam closed 12 years ago
2
Reference function declaration in ReturnValueReference

#107 jspam closed 12 years ago
0
Function call substitution does not always need to create quantified expressions

#106 jspam closed 12 years ago
0
Success Kid Dialog does not adapt to font size

#105 jspam closed 12 years ago
0
EmptyStackException in prover

#104 jspam closed 12 years ago
1
Breakpoints on empty lines should not be ignored

#103 stefanorf closed 12 years ago
1
Irritating Invariant/FunctionAnnotation `true` when Invariants/FunctionAnnotations present

#102 bafain closed 12 years ago
0
WPStrategy::visit(Loop) reuses AssignedVariables with their initial value set

#101 bafain closed 12 years ago
2
feature: allow line wrapping of statements

#100 danielgrahl closed 12 years ago
0
Interpreter should pass axioms to prover

#99 leonhandreke closed 12 years ago
0
GuardAssertion subclasses should specify the type of guarded node

#98 leonhandreke closed 12 years ago
0
Signal and display the assertion the prover is currently verifying

#97 bafain opened 12 years ago
0
Field access of primitive return value is valid

#96 bafain closed 12 years ago
0
NullPointerException trying to call getVariable().getName() on a ReturnValueReference

#95 jspam closed 12 years ago
1
NullPointerException when returning empty array literal

#94 jspam closed 12 years ago
1
NullPointerException on loop after return statement

#93 jspam closed 12 years ago
0
Debugger should only show "worst" validity on statement

#92 jspam closed 12 years ago
0
Watch expressions are not validated

#91 jspam closed 12 years ago
0
Debugger allows setting variable value to wrong type

#90 jspam closed 12 years ago
0
UnsupportedOperationException on breakpoint with condition

#89 jspam closed 12 years ago
0
Formatter breaks syntactic correctness and modifies the program iteratively

#88 jspam opened 12 years ago
1
"Toggle watchpoint" causes line breakpoint to disappear and vice versa

#87 jspam closed 12 years ago
0
IllegalArgumentException when launching configuration with empty file name

#86 jspam closed 12 years ago
0
"Prove it" does not launch selection

#85 jspam closed 12 years ago
0
Comments after _ensures are colored after proof

#84 leonhandreke closed 12 years ago
1
SMTLIB: When modifying an array index the old and new array do not not equal

#83 bafain closed 12 years ago
1
Multiple quantifiers for equal variables when trying to prove automaton.ww

#82 bafain closed 12 years ago
1
Stackoverflow error when trying to prove bubblesort.ww

#81 bafain closed 12 years ago
0
"No viable alternative at input" when forall is not in brackets

#80 leonhandreke closed 12 years ago
0
WorthwhileExpressions.xmi not found when evaluating expressions

#79 jspam closed 12 years ago
0
Programs are not marked as terminated after proving

#78 jspam closed 12 years ago
0
Programs are not marked as terminated when reaching end of code

#77 jspam closed 12 years ago
0
Stepping over loop or function call causes debugger to step over rest of program

#76 jspam closed 12 years ago
0
Validator tries to check parameter count on undeclared function

#75 jspam closed 12 years ago
0
When loop condition + invariant is verified, the whole loop is marked in the UI

#74 jspam opened 12 years ago
8
Better visualize proofs for assertions inserted by SpecificationChecker

#73 leonhandreke closed 12 years ago
5
Race condition when settings prover result markers in editor

#72 leonhandreke closed 12 years ago
2
Assignment should use Unicode "colon equals"

#71 leonhandreke closed 12 years ago
3
Allow arrays as variables in quantified expressions

#70 jspam closed 12 years ago
0
Variables in loops are not bound to function preconditions

#69 jspam closed 12 years ago
4
Prover fails to incorporate condition of quantified expression into proof

#68 jspam closed 12 years ago
0