issues
search
utwente-fmt
/
vercors
The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
56
stars
26
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Readable#fileName is being used incorrectly
#1284
superaxander
opened
3 days ago
0
Only run test_report if the run was not cancelled
#1283
superaxander
closed
4 days ago
0
Unexpected behaviour when defining functions wrongly
#1282
ArmborstL
opened
5 days ago
0
VeyMont: parameterization syntax & AST changes
#1281
bobismijnnaam
opened
6 days ago
0
Integrate Pallas FunctionContracts
#1280
RobertMensing
opened
6 days ago
0
Recursively self-referential generic Java class causes MonomorphizeClass to not terminate
#1279
wandernauta
opened
1 week ago
1
Log and exit error if --compile (PVL-to-Java translation) mode fails
#1278
wandernauta
closed
6 days ago
3
Extend pointer encoding
#1277
superaxander
opened
1 week ago
0
VeyMont: remove PushInChor
#1276
bobismijnnaam
closed
2 weeks ago
0
Crash report: Viper has crashed: java.util.NoSuchElementException: None.get
#1275
etiennebirling
opened
1 month ago
5
Crash report: The silver AST delivered to viper is not valid: - Consistency error: Perm and forperm in this conte
#1274
etiennebirling
opened
1 month ago
1
Generic classes with final fields trigger TransformationCheckError, crash
#1273
wandernauta
opened
1 month ago
1
generateSingleOwnerPermissions fails with classes containing final fields
#1272
wandernauta
opened
1 month ago
1
TruncDiv applied to permission values crashes VerCors
#1271
superaxander
opened
1 month ago
0
Struct examples
#1270
superaxander
closed
2 weeks ago
0
VeyMont: remove ChorPerm
#1269
bobismijnnaam
closed
2 weeks ago
0
Neglecting to specify type arguments in PVL new expression triggers crash
#1268
wandernauta
closed
1 month ago
4
Attempting to return a resource in PVL triggers NoSuchElementException
#1267
wandernauta
opened
1 month ago
2
Syntax error in right-plus operator overload triggers ParseMatchError, crash
#1266
wandernauta
closed
1 month ago
0
Type of \type, \typeof expressions is inconsistently integer in PVL
#1265
wandernauta
opened
1 month ago
0
Channel invariant expressions outside channel invariants trigger crash
#1264
wandernauta
closed
1 month ago
0
Labels in some method bodies trigger "There is no scope to place LabelDecl" error
#1263
wandernauta
closed
1 month ago
0
Generated trigger by SimplifyNestedQuantifiers crashes Viper
#1262
superaxander
opened
1 month ago
0
Collect bip_annotation modifier in all ToCol classes
#1261
wandernauta
closed
1 month ago
1
Add stringToName special case for all-underscores identifier strings
#1260
wandernauta
closed
1 month ago
2
VeyMont: support inline, wrapped, and no stratified permissions, fix some of Wander's issues, update VeyMont pass order.
#1259
bobismijnnaam
closed
1 month ago
0
Fix mill for Windows
#1258
ArmborstL
opened
1 month ago
2
"unfold" in pure method is silently dropped
#1257
ArmborstL
opened
1 month ago
0
`extract while` does not propagate `this != null`
#1256
bobismijnnaam
opened
1 month ago
0
VerCors crash should be more informative if crash is caused by unsound axiom being added
#1255
bobismijnnaam
opened
1 month ago
0
Update to setup-java@v4
#1254
superaxander
closed
1 month ago
0
Attempt to fix the test reporting by running the test report on the default branch
#1253
superaxander
closed
1 month ago
0
AutoValue unsoundness, Test Suite runner, Paths with spaces
#1252
superaxander
closed
1 month ago
0
Bump dorny
#1251
bobismijnnaam
closed
1 month ago
3
Make contract of free (for C) conditional on ptr being non-null
#1250
wandernauta
closed
1 month ago
0
Restrict C++ character literals to a single UTF-8 char
#1249
wandernauta
closed
1 month ago
0
Fix empty PVL enums causing verification failure
#1248
wandernauta
closed
1 month ago
9
Generics do not support method calls with implicit `this.` prefix
#1247
bobismijnnaam
opened
2 months ago
0
Test MatrixTransposeWithF is unstable
#1246
bobismijnnaam
opened
2 months ago
2
Wand is not correctly documented.
#1245
sakehl
opened
2 months ago
1
VeyMont: lightweight permissions
#1244
bobismijnnaam
closed
2 months ago
0
CPPToCol assumes integer value of character literals equals Unicode code point in C++
#1243
wandernauta
closed
1 month ago
1
System.in, System.out, System.err fields are incorrectly treated as immutable in Java
#1242
wandernauta
opened
2 months ago
3
Simplify rules ignore side-effects
#1241
superaxander
opened
2 months ago
0
Null pointer can not be passed to free in C
#1240
wandernauta
closed
1 month ago
1
Encode that malloc may return NULL in C (weaken postcondition)
#1239
wandernauta
closed
1 month ago
1
Remove unused nlohmann/json dep for vcllvm.origin module
#1238
wandernauta
closed
2 months ago
2
Pointers to nonheap objects can be passed to free in C
#1237
wandernauta
opened
2 months ago
2
Don't try to delete nonexistent preprocessor output if clang fails
#1236
wandernauta
closed
2 months ago
0
Errors during C preprocessing confusingly logged as "File not found"
#1235
wandernauta
closed
2 months ago
1
Next