Code

Unreachable code detection#1385

Code

Open

simon-hrabec wants to merge 42 commits intoviperproject:masterviperproject/prusti-dev:masterfrom simon-hrabec:feature/unreachable-code-detectionsimon-hrabec/prusti-dev:feature/unreachable-code-detectionCopy head branch name to clipboard

+73-52

Commits

Commits on Feb 6, 2023

• Add prusti_refute! macro

  

  Simon Hrabec

  committed
  9ac293b

Commits on Feb 15, 2023

• Merge branch 'master' of github.com:simon-hrabec/prusti-dev into feature/refute_macro

  

  Simon Hrabec

  committed
  2c4fb37

Commits on Feb 21, 2023

• Add macro to generate getters/setters for fields via JNI

  

  Simon Hrabec

  committed
  c49f9a7

• Resolve fmt-check and clippy errors, simplify naming, small refactoring

  

  Simon Hrabec

  committed
  6c3d955

• Merge branch 'master' of github.com:viperproject/prusti-dev into feature/jni-field-getter-setter

  

  Simon Hrabec

  committed
  bee6c22

Commits on Feb 26, 2023

• Add test for field! macro

  

  Simon Hrabec

  committed
  a896d5a

• Update field! macro to not ask for signature (WIP)

  

  Simon Hrabec

  committed
  ec17da5

Commits on Feb 27, 2023

• Update field! macro to search all the class hierarchy for the field to determine its signature

  

  Simon Hrabec

  committed
  dc8642c

• Merge pull request #2 from simon-hrabec/feature/jni-field-getter-setter-without-signature

  Show description for 019f222
  simon-hrabec

  authored
  019f222

• Rename variables, add comments, delete leftover commented code

  

  Simon Hrabec

  committed
  608c4aa

• Merge branch 'feature/refute_macro' into combined

  

  Simon Hrabec

  committed
  0c2ecc8

• Merge branch 'master' of github.com:viperproject/prusti-dev into combined

  

  Simon Hrabec

  committed
  a60bb1e

• Merge branch 'master' of github.com:viperproject/prusti-dev into combined

  simon-hrabec

  committed
  542d905

• Follow update in master branch

  simon-hrabec

  committed
  667c3b6

Commits on Mar 6, 2023

• current code, just a snapshot of my working dir

  simon-hrabec

  committed
  864c896

Commits on Mar 13, 2023

• fix bug with env/ast_utils with_local_frame - calling wrong function

  simon-hrabec

  committed
  b9796a6

• Merge branch 'master' of github.com:viperproject/prusti-dev into combined

  simon-hrabec

  committed
  a490f2f

• add

  simon-hrabec

  committed
  0d48d5a

• Remove unecessary changes

  simon-hrabec

  committed
  ea965ab

• additional temporary code removal

  simon-hrabec

  committed
  76e0376

• Add "refute.failed:refutation.true" into error_manager

  simon-hrabec

  committed
  8117694

• Remove unnecessary code, fmt-all

  simon-hrabec

  committed
  e6b5692

• Merge branch 'master' of github.com:viperproject/prusti-dev into combined

  simon-hrabec

  committed
  7443fd2

• cargo lock update

  simon-hrabec

  committed
  cc7bb62

Commits on Mar 17, 2023

• add frotend support also for carbon

  simon-hrabec

  committed
  fc2bda8

Commits on Mar 19, 2023

• add assert.failed:assertion.false-PanicCause::Refute entry to the error manager

  simon-hrabec

  committed
  d0ad6a6

Commits on Mar 20, 2023

• Add field access via Scala methods, use SilFrontend wrapper and remove unecessary dispatch

  simon-hrabec

  committed
  6867a3b

• Remove empty line - fmt-all error

  simon-hrabec

  committed
  0415395

Commits on Mar 21, 2023

• add tests for prusti_refute!

  simon-hrabec

  committed
  2695baf

• update docs (user guide) - add mention to refute

  simon-hrabec

  committed
  a207e10

Commits on Mar 27, 2023

• trying to figure out positions for added refutes

  simon-hrabec

  committed
  e6897da

Commits on Mar 28, 2023

• use terminator span

  simon-hrabec

  committed
  e71787a

Commits on Mar 29, 2023

• Update unreachable message

  simon-hrabec

  committed
  31bc7d9

• delete lefrover code

  simon-hrabec

  committed
  bdfcd24

Commits on Apr 3, 2023

• make code unreachable errors just warnings

  simon-hrabec

  committed
  b66210e

• change detection of assert/panic terminators

  simon-hrabec

  committed
  7592282

• remove unecessary case in the error manager

  simon-hrabec

  committed
  ca94f92

Commits on Apr 4, 2023

• make line/column numbers unique for code reachability refute statements

  simon-hrabec

  committed
  27ecb2e

• remove unecessary member variable, use just position id

  simon-hrabec

  committed
  b9cb939

• Merge branch 'master' of github.com:viperproject/prusti-dev into feature/unreachable-code-detection

  simon-hrabec

  committed
  d7deab6

Commits on Apr 5, 2023

• make position manager return positions with unique line/column

  simon-hrabec

  committed
  5cd88f5

Commits on Apr 6, 2023

• rely on the change in position manager for unique line/column numbers in positions

  simon-hrabec

  committed
  8433a89