Code

Add opaque/reveal to Gobra#715

Code

Merged

jcp19 merged 23 commits intoviperproject:masterviperproject/gobra:masterfrom dnezam:masterCopy head branch name to clipboardFeb 8, 2024

+3,425-2,956

Commits

Commits on Dec 27, 2023

• Port fac from Viper's opaque test

  dnezam

  committed
  f7ab65c

• Remove auto-generated files

  dnezam

  committed
  b92fd37

Commits on Jan 30, 2024

• Roughly implement opaque

  dnezam

  committed
  3c5177c

• Roughly implement opaque (rest of files)

  dnezam

  committed
  f790863

Commits on Jan 31, 2024

• Implemented reveal?

  dnezam

  committed
  a764da9

• Fix a pinch of errors

  dnezam

  committed
  dc28aca

Commits on Feb 2, 2024

• Fix PrettyPrint + Default/Call encoding errors

  dnezam

  committed
  6f8f3f3

• Fix rest of compile errors

  dnezam

  committed
  984ac8a

Commits on Feb 3, 2024

• Add typing checks

  dnezam

  committed
  ef0656b

• Fix parsing of opaque

  dnezam

  committed
  e042bd8

• Add check in wellDefSpec

  dnezam

  committed
  97ac851

• Add opaque test for outline

  dnezam

  committed
  0f1dab6

• Merge branch 'master' into master

  dnezam

  authored
  c6ffaa9

• Add missing termination measure to test

  dnezam

  committed
  641cacb

Commits on Feb 5, 2024

• Add more tests

  dnezam

  committed
  ee3c2d4

• Fix error message in ExprTyping.scala

  dnezam

  committed
  c7c4e35

• Add missing license header

  dnezam

  committed
  28531cb

• Add test for opaque abstract function

  dnezam

  committed
  38a3fe3

• Remove comment and fix tabs

  Show description for 265365d
  dnezam

  committed
  265365d

Commits on Feb 8, 2024

• Address feedback

  dnezam

  committed
  bcd8ef6

• Remove comment + test for revealing closure

  dnezam

  committed
  0d5fc69

• Merge branch 'viperproject:master' into master

  dnezam

  authored
  0741c88

• Fix misplaced test annotation

  dnezam

  committed
  f8c8613