utwente-fmt/vercors

Issues

• Idea: Program analyses/annotation for not verifying 'dead code'

  #1222 opened 5 months ago by sakehl
  0

• Rewriter did not respect order of annotations

  #1215 opened 5 months ago by sakehl
  0

• VerCors does not check if assign target is an lvalue

  #1199 opened 7 months ago by bobismijnnaam
  0

• Yields on PVL class constructor crashes VerCors.

  #1198 opened 7 months ago by OmerSakar
  0

• Slow VerCors passes for simple program

  #1195 opened 7 months ago by sakehl
  8

• Bool/Int coercion for C is incomplete

  #1187 opened 8 months ago by ArmborstL
  3

• GPU programs do not give fault for to much permission, which leads to incomplete verification

  #1184 opened 5 months ago by sakehl
  3

• Cannot use inline predicate in unfolding

  #1120 opened a year ago by ArmborstL
  0

• Using \gtid in barrier contracts breaks down and does not verify

  #1178 opened 9 months ago by sakehl
  0

• `refute` does not work as expected

  #1183 opened 8 months ago by superaxander
  1

• Performance issues

  #1214 opened 6 months ago by sakehl
  13

• Building VerCors on Java 21 results in package ops not found error

  #1146 opened 6 months ago by bobismijnnaam
  0

• The windows run script does not use parallelisation

  #1211 opened 6 months ago by pieter-bos
  0

• Val sections of _ToCOL are out of sync

  #1204 opened 7 months ago by pieter-bos
  0

• `expectedError` and console output

  #1201 opened 7 months ago by pieter-bos
  1

• Override all standard locations for sources in the build

  #1196 opened 7 months ago by pieter-bos
  0

• Implement and merge VCLLVM

  #1191 opened 7 months ago by alexchandel
  1

• Release task fails on push to `master` since it should only respond to tag pushes on that branch

  #1186 opened 8 months ago by pieter-bos
  0

• Parallel Block encoder, saving ranges as variables

  #1165 opened 8 months ago by sakehl
  1

• Wrong usages of `getPreferredName`

  #1179 opened 9 months ago by pieter-bos
  0

• `frame` is not documented

  #1175 opened 9 months ago by pieter-bos
  1

• Can't reason about old values for which we have write permission in GPU kernels

  #1176 opened 9 months ago by sakehl
  2

• VerCors throws an error when Specifying a resource as trigger

  #1173 opened 9 months ago by sakehl
  1

• Broken position when reporting incompatible modifier

  #1115 opened a year ago by ArmborstL
  1

• The --skip-backend flag does nothing

  #1152 opened 9 months ago by superaxander
  1

• Windows progress rendering is broken

  #1150 opened 10 months ago by pieter-bos
  1

• Program with array class member does not verify with parallel block

  #1166 opened 10 months ago by sakehl
  2

• [VS Code] As a user, I want checkboxes to include command line options.

  #1163 opened 10 months ago by pandasansgains
  0

• [VS Code] As a user, I want keywords to be highlighted with different colours in Java when adding JML.

  #1162 opened 10 months ago by pandasansgains
  0

• [VS Code] Add a button to stop an analysis during run time

  #1164 opened 10 months ago by pandasansgains
  0

• [VS Code] As a user, I want keywords to be highlighted with different colours in PVL.

  #1161 opened 10 months ago by pandasansgains
  0

• [VS Code] As a user, I want to be able to click on a variable to go to its definition in PVL.

  #1160 opened 10 months ago by pandasansgains
  0

• Cannot define permissions for global structs in C

  #1143 opened a year ago by ArmborstL
  3

• Division defaults to rationals instead of integer floor division when using --backend-file-base

  #1129 opened a year ago by sakehl
  1

• OpenCL files actually do not import 'opencl.h'

  #1151 opened 10 months ago by sakehl
  0

• VerCors crashes when predicate is missing argument in C

  #1147 opened 10 months ago by ArmborstL
  2

• Specification cannot resolve value for C "define" macro

  #1148 opened 10 months ago by ArmborstL
  2

• Relation and equality operators in C have int as return type

  #1153 opened 10 months ago by sakehl
  1

• `seq<_>.prepend` does not work

  #1158 opened 10 months ago by pieter-bos
  0

• Cannot use "NULL" as struct pointer

  #1141 opened a year ago by ArmborstL
  5

• Cache protobuf versions of the simplification rules

  #1116 opened a year ago by pieter-bos
  0

• ConstantifyFinalFields is a bit dubious

  #1134 opened a year ago by pieter-bos
  0

• VerCors crashes when missing a "decreases" for functions with recursive contract

  #1133 opened a year ago by ArmborstL
  0

• Cannot read-scale a predicate

  #1128 opened a year ago by bobismijnnaam
  2

• Subscript blame reported on wrong node

  #1123 opened a year ago by bobismijnnaam
  0

• Nit: consider giving `ADTFunction` type arguments

  #1125 opened a year ago by pieter-bos
  0

• Option to make viper output a bit nicer for reporting viper problems

  #1122 opened a year ago by pieter-bos
  1

• VerCors does not find global declarations if given multiple files

  #1119 opened a year ago by ArmborstL
  2

• Consider moving `CoercingRewriter.coerce` and `Resolve{References,Types}.resolveOne` to the impl traits

  #1117 opened a year ago by pieter-bos
  0

• Dividing by zero

  #1112 opened a year ago by sakehl
  2