Code

Theory of heaps translation (again)#13

Code

Merged

zafer-esen merged 55 commits intouuverifiers:masteruuverifiers/tricera:masterfrom woosh:ola-theory-of-heaps-translationwoosh/tricera:ola-theory-of-heaps-translationCopy head branch name to clipboardJun 19, 2024

+3,488-15

Commits

Commits on May 23, 2024

• Add TheoryOfHeapProcessor and ContractConditionTools

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  0577ace

  Copy full SHA for 0577ace

• Add EqualityReader and IExpressionProcessor trait

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  62b6458

  Copy full SHA for 62b6458

• Add PostconditionSimplifier

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  aec33c9

  Copy full SHA for aec33c9

• Add ACSLExpressionProcessor and improve match readability

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  69e9a3e

  Copy full SHA for 69e9a3e

• Add EqualitySwapper

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  d860aba

  Copy full SHA for d860aba

• Add ClauseRemover

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  8d117c6

  Copy full SHA for 8d117c6

• Add ACSLExpressions to ACSLLineariser

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  27a6df5

  Copy full SHA for 27a6df5

• Add ADTSimplifier and fix getter extraction in TOHProcessor

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  d17525b

  Copy full SHA for d17525b

• Add struct dereference translation

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  76bb29e

  Copy full SHA for 76bb29e

Commits on May 24, 2024

• Fix uniform expression processing

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  aa24644

  Copy full SHA for aa24644

• Replace IExpressionProcessor by ContractProcessor

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  394b6ab

  Copy full SHA for 394b6ab

• Refactor ACSLExpressionProcessor

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  aa636fc

  Copy full SHA for aa636fc

• Refactor ADTSimplifier

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  3663942

  Copy full SHA for 3663942

• Refactor classes with ContractProcessor

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  7745649

  Copy full SHA for 7745649

• Refactor TheoryOfHeapFunApp

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  c3a95e6

  Copy full SHA for c3a95e6

• Move out AssignmentProcessor and fix TheoryOfHeapFunApp

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  ae50c3f

  Copy full SHA for ae50c3f

• Replace Equalities by ValSet

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  0794c78

  Copy full SHA for 0794c78

• Refactor EqualitySwapper

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  17047cc

  Copy full SHA for 17047cc

• Add HeapPropProcessor and remove PostconditionSimplifier from processors

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  01a89b7

  Copy full SHA for 01a89b7

• Add separated and first write filtering to AssignmentProcessor

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  c919d9d

  Copy full SHA for c919d9d

• Add getClauses for Assignment- and PointerPropProcessor

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  d0f2066

  Copy full SHA for d0f2066

• Add properties to ContractInfo

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  83cc797

  Copy full SHA for 83cc797

• Add PostconditionSimplifier again

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  32cf7fe

  Copy full SHA for 32cf7fe

• Add ExplicitPointerRemover and TrivialEqualityRemover

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  82dd990

  Copy full SHA for 82dd990

• Add general removal of explicit pointers

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  26ae945

  Copy full SHA for 26ae945

• Fix bug where an empty separatedSet would result in no assignments

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  aeab155

  Copy full SHA for aeab155

• Add false check for PostconditionSimplifier

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  e791d0f

  Copy full SHA for e791d0f

• Fix bug where equalities within OR clauses were read

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  99cc2d6

  Copy full SHA for 99cc2d6

• Fix bug where ExplPointerRemover missed pointers

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  0d6972c

  Copy full SHA for 0d6972c

• Fix bug where quantifierDepth wasn't passed

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  0963b3e

  Copy full SHA for 0963b3e

• Fix bug where ExplicitPointerRemover missed last formula

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  5fe19fb

  Copy full SHA for 5fe19fb

• Add HeapEqualityRemover

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  a5ce42e

  Copy full SHA for a5ce42e

• Remove is_O_<sort> to valid translation

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  b7c21dd

  Copy full SHA for b7c21dd

• Refactor getStructMap to val

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  2f09eae

  Copy full SHA for 2f09eae

• Rename isCurrentHeap

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  9a101d2

  Copy full SHA for 9a101d2

• Fix formula shift in EqualitySwapper and fix prints

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  548324d

  Copy full SHA for 548324d

• Clean up main function

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  267965f

  Copy full SHA for 267965f

• (WIP) Do not apply heap processor when there is no heap.

  

  zafer-esen

  authored and

  Ola Wingbrant (sssowo)

  committed
  ca08a61

  Copy full SHA for ca08a61

• Fix heap processors running when no heap available

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  f457942

  Copy full SHA for f457942

• Add preambles and high-level descriptions

  

  OskarSoderberg

  authored and

  Ola Wingbrant (sssowo)

  committed
  2aacdf7

  Copy full SHA for 2aacdf7

• Add -debug option for printing debug messages and clean up some debug printing.

  

  zafer-esen

  authored and

  Ola Wingbrant (sssowo)

  committed
  f1917e7

  Copy full SHA for f1917e7

• Update years in preambles and list of contributors

  

  zafer-esen

  authored and

  Ola Wingbrant (sssowo)

  committed
  19042b1

  Copy full SHA for 19042b1

• Fix build issues after rebase to master

  

  Wingbrant Ola

  committed
  13f0ced

  Copy full SHA for 13f0ced

Commits on May 29, 2024

• Remove extraneous 'UNSAFE' printout

  

  Ola Wingbrant (sssowo)

  committed
  30d17a0

  Copy full SHA for 30d17a0

• Draft regression tests for ACSL theory of heap translation

  

  Ola Wingbrant (sssowo)

  committed
  b9a3251

  Copy full SHA for b9a3251

Commits on May 30, 2024

• Second draft regression tests for ACSL theory of heap translation

  

  Ola Wingbrant (sssowo)

  committed
  a78d299

  Copy full SHA for a78d299

• Add regression-tests/toh-contract-translation/runtests

  

  Ola Wingbrant (sssowo)

  committed
  bbfbf9b

  Copy full SHA for bbfbf9b

Commits on May 31, 2024

• Add regression tests to 'runalldirs'

  

  Ola Wingbrant (sssowo)

  committed
  3869799

  Copy full SHA for 3869799

• Removed unused files

  

  Ola Wingbrant (sssowo)

  committed
  be699b7

  Copy full SHA for be699b7

• Add regression-tests/toh-contract-translation/Answers

  

  Ola Wingbrant (sssowo)

  committed
  971f955

  Copy full SHA for 971f955

• Correct projec/build.properties

  

  Ola Wingbrant (sssowo)

  committed
  b081923

  Copy full SHA for b081923

Commits on Jun 12, 2024

• Remove failing regression test from toh-contract-translation suite

  

  Ola Wingbrant (sssowo)

  committed
  a529938

  Copy full SHA for a529938

Commits on Jun 17, 2024

• Add changes from theory-of-heaps-translation-thesis-version

  

  Ola Wingbrant (sssowo)

  authored and

  woosh

  committed
  481819f

  Copy full SHA for 481819f

• Merge branch 'ola-theory-of-heaps-translation' of https://github.com/woosh/tricera into ola-theory-of-heaps-translation

  

  Ola Wingbrant (sssowo)

  committed
  c6db602

  Copy full SHA for c6db602

Commits on Jun 19, 2024

• Use empty heap instead of quantified heap variable

  

  Ola Wingbrant (sssowo)

  committed
  ed405fe

  Copy full SHA for ed405fe