viperproject chalice2silver issues

viperproject / chalice2silver

Other

0 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Unsound translation of `receive newC := newC`

#87 viper-admin opened 7 years ago
0
Typechecker allows assignment to method parameter via fork

#86 viper-admin opened 7 years ago
0
Crash when receive expression creates new variable

#85 viper-admin opened 7 years ago
0
mustTerminate encoding is unsound

#84 viper-admin opened 8 years ago
0
Merge obligations into default fork

#102 viper-admin closed 4 years ago
2
Returned obligations are always fresh

#83 viper-admin opened 8 years ago
0
The lifetime of obligations converted from unbounded to bounded is unknown

#82 viper-admin opened 8 years ago
0
Crash with mustRelease(this, 1); in precondition.

#81 viper-admin opened 8 years ago
0
Channels of different types are not known to be non-aliases

#80 viper-admin opened 8 years ago
0
Conditional mustTerminate obligation not allowed in loop invariant

#79 viper-admin opened 8 years ago
0
Wrong emitted operation order allows negative amount of mustSend obligations

#78 viper-admin opened 8 years ago
1
mustTerminate(0) is not allowed in while (false)

#77 viper-admin opened 8 years ago
4
Chalice2Silver does not support ide mode.

#76 viper-admin opened 9 years ago
0
Chalice2Silver outputs errors to stderr

#75 viper-admin opened 9 years ago
0
add Silver test cases for new language features

#74 viper-admin opened 9 years ago
0
Selecting verifier should be supported by name

#73 viper-admin opened 9 years ago
1
Quantified permissions parsed and translated incorrectly

#72 viper-admin opened 9 years ago
0
Regression test and partial fix for Chalice2Silver issue 71.

#101 viper-admin closed 4 years ago
0
Bodyless functions are not supported

#71 viper-admin opened 9 years ago
3
Updated test annotations to reflect fixed Carbon issue 52.

#100 viper-admin closed 4 years ago
1
Just to make Jenkins happy…

#99 viper-admin closed 4 years ago
1
Just to make Jenkins happy…

#98 viper-admin closed 4 years ago
0
Fixed dependency number.

#97 viper-admin closed 4 years ago
1
Added dependency to Carbon + bugfix

#96 viper-admin closed 4 years ago
0
Typechecker does not capture the case when fork shadows method argument

#70 viper-admin opened 9 years ago
0
Cross method join is not supported

#69 viper-admin opened 9 years ago
0
Translation of “forall c in collection” is wrong

#68 viper-admin opened 9 years ago
0
Reviewed Chalice2Silver test suite

#95 viper-admin closed 4 years ago
1
Test internal-bug-10.chalice fails only when executed on AST generated by Chalice2Silver

#67 viper-admin opened 9 years ago
0
Switch to Carbon and Silicon versions that support quantified permissions.

#66 viper-admin opened 9 years ago
0
Crash when translating UnboundedThreads.chalice

#65 viper-admin opened 9 years ago
0
Overlaping variables are translated incorrectly

#64 viper-admin closed 4 years ago
3
Heisenbug: Verifier crashes with null pointer exception

#63 viper-admin closed 4 years ago
6
A workaround for issue #52.

#94 viper-admin closed 4 years ago
1
Bug Fix: Chalice2SILFrontEnd was silently picking only the first file.

#93 viper-admin closed 4 years ago
1
Improved syntax and type error reporting.

#92 viper-admin closed 4 years ago
1
Merge yChallice project into Chalice2Silver.

#91 viper-admin closed 4 years ago
1
Removed dependency on yChalice, improved error reporting.

#90 viper-admin closed 4 years ago
0
Test accessInQuantifiers causes a java.lang.IllegalArgumentException

#62 viper-admin opened 9 years ago
0
Compilation error fix and small changes.

#89 viper-admin closed 4 years ago
1
Bug fix: renaming dependencies to lower case to be consistent with silicon project.

#88 viper-admin closed 4 years ago
1
Different semantics of [x..y] between old and new Chalice

#61 viper-admin opened 10 years ago
0
Token permissions are not supported

#60 viper-admin opened 10 years ago
0
Test ll-lastnode fails with Silicon

#59 viper-admin closed 4 years ago
2
Lock block semantics in Chalice is different from Chalice2Silver

#58 viper-admin opened 10 years ago
0
Rely-guarantee invariants are not supported in Chalice2Silver

#57 viper-admin opened 10 years ago
1
rd(P) where P is a predicate is not translated correctly

#56 viper-admin opened 10 years ago
1
Permission model does not work correctly with the permission parameter of a method

#55 viper-admin opened 10 years ago
3
Issue annotations may only be marked as "silicon" issues

#54 viper-admin closed 4 years ago
2
Chalice2Silver does not work with a CLI specified verifier

#53 viper-admin opened 10 years ago
0