Code

Add support for quantifiers#3993

Code

Merged

qinheping merged 28 commits intomodel-checking:mainmodel-checking/kani:mainfrom

qinheping:quantifiersqinheping/kani:quantifiersCopy head branch name to clipboard

May 13, 2025

Commits

Commits on Apr 7, 2025

• Add support for quantifiers

  Show description for a92688f
  

  feliperodri

  authored and

  qinheping

  committed
  a92688f

  Copy full SHA for a92688f

• Format code and avoid code duplication

  Show description for e8c5e43
  

  feliperodri

  authored and

  qinheping

  committed
  e8c5e43

  Copy full SHA for e8c5e43

• Inlining function calls in quantifier expressions

  qinheping

  committed
  0be406a

  Copy full SHA for 0be406a

Commits on Apr 11, 2025

• Fix ranged existential quantification

  qinheping

  committed
  f838e91

  Copy full SHA for f838e91

• Add support of switch in quantifier expression

  qinheping

  committed
  6d0017b

  Copy full SHA for 6d0017b

• Remove debug leftover

  qinheping

  committed
  df78d91

  Copy full SHA for df78d91

• Make tests depending on new CBMC fixme

  qinheping

  committed
  d463882

  Copy full SHA for d463882

• Fix clippy

  qinheping

  committed
  bf9eb97

  Copy full SHA for bf9eb97

• Fix clippy

  qinheping

  committed
  f21041d

  Copy full SHA for f21041d

• Fix clippy

  qinheping

  committed
  49c22c9

  Copy full SHA for 49c22c9

• Make universal quantification complete

  qinheping

  committed
  8210209

  Copy full SHA for 8210209

• Make universal quantification complete

  qinheping

  committed
  e276642

  Copy full SHA for e276642

Commits on Apr 15, 2025

• Add tests for quantifier expression with array indexing

  qinheping

  committed
  5a60da9

  Copy full SHA for 5a60da9

• Add fixme info

  qinheping

  committed
  8c242b8

  Copy full SHA for 8c242b8

• Update RFC with function inlining

  qinheping

  committed
  40195bc

  Copy full SHA for 40195bc

Commits on Apr 22, 2025

• Make even test non fixme

  qinheping

  committed
  fac313f

  Copy full SHA for fac313f

• Update array tests

  qinheping

  committed
  131d503

  Copy full SHA for 131d503

• Add tests with quantifiers in contracts

  qinheping

  committed
  3bf250b

  Copy full SHA for 3bf250b

• Add document for quantifiers

  qinheping

  committed
  acee4ef

  Copy full SHA for acee4ef

Commits on Apr 24, 2025

• Fix format

  qinheping

  committed
  e336cad

  Copy full SHA for e336cad

• Fix clippy

  qinheping

  committed
  a3549ec

  Copy full SHA for a3549ec

Commits on Apr 29, 2025

• Merge branch 'main' into quantifiers

  tautschnig

  authored
  39832fa

  Copy full SHA for 39832fa

• Update tests

  tautschnig

  committed
  41b4755

  Copy full SHA for 41b4755

Commits on Apr 30, 2025

• Add expected tests

  qinheping

  committed
  6d795e9

  Copy full SHA for 6d795e9

• Fix format

  qinheping

  committed
  71d1a92

  Copy full SHA for 71d1a92

Commits on May 1, 2025

• Address Carolyn's comments

  qinheping

  committed
  abb3e8e

  Copy full SHA for abb3e8e

• Remove the need of import quantifiers

  qinheping

  committed
  c8ea72f

  Copy full SHA for c8ea72f

Commits on May 7, 2025

• Make quantifier functions hidden

  qinheping

  committed
  445b809

  Copy full SHA for 445b809