Code

Counterexamples (WIP)#258

Code

Draft

fabioali wants to merge 96 commits intoviperproject:masterviperproject/gobra:masterfrom fabioali:masterfabioali/gobra:masterCopy head branch name to clipboard

+3,751-54

Commits

Commits on Feb 23, 2021

• testfork

  fabioali

  committed
  817090d

  Copy full SHA for 817090d

• Merge branch 'master' of https://github.com/fabioali/gobra

  fabioali

  committed
  a9d4f85

  Copy full SHA for a9d4f85

Commits on Feb 25, 2021

• sync

  fabioali

  committed
  e972bea

  Copy full SHA for e972bea

Commits on Feb 28, 2021

• added playgound

  fabioali

  committed
  77ef28f

  Copy full SHA for 77ef28f

Commits on Mar 1, 2021

• created counterexample interface

  fabioali

  committed
  19a4f1e

  Copy full SHA for 19a4f1e

Commits on Mar 2, 2021

• added ppipeline and always-on counterexamples for silicon

  fabioali

  committed
  9de06ac

  Copy full SHA for 9de06ac

• something is happening: Backtranslator has a print statement

  fabioali

  committed
  7d9563f

  Copy full SHA for 7d9563f

Commits on Mar 3, 2021

• added counterexample to VerifierError, Cleanup of backtranslator and CounterexampleBackranslato, added counterexamples to message

  fabioali

  committed
  40a9c0d

  Copy full SHA for 40a9c0d

Commits on Mar 5, 2021

• cleanup of config

  fabioali

  committed
  0f3840d

  Copy full SHA for 0f3840d

• changed the varible names of the output

  fabioali

  committed
  be18224

  Copy full SHA for be18224

Commits on Mar 11, 2021

• added parsing, function selection,some filtering

  fabioali

  committed
  bf0203a

  Copy full SHA for bf0203a

Commits on Mar 12, 2021

• found relevant function

  fabioali

  committed
  ac0e190

  Copy full SHA for ac0e190

Commits on Mar 22, 2021

• fixed shortName path problem

  fabioali

  committed
  4ee340e

  Copy full SHA for 4ee340e

• added diffs from Felix

  fabioali

  committed
  d89b741

  Copy full SHA for d89b741

• modified for simplicity

  fabioali

  committed
  faed81a

  Copy full SHA for faed81a

• found function that is important using types

  fabioali

  committed
  4a4667c

  Copy full SHA for 4a4667c

Commits on Mar 26, 2021

• sourcemodel, mappings and such

  fabioali

  committed
  127cae1

  Copy full SHA for 127cae1

Commits on Mar 30, 2021

• added entries

  fabioali

  committed
  43e050a

  Copy full SHA for 43e050a

• cleanup

  fabioali

  committed
  9e0a15c

  Copy full SHA for 9e0a15c

Commits on Apr 1, 2021

• prettyprint

  fabioali

  committed
  9e882a8

  Copy full SHA for 9e882a8

Commits on Apr 6, 2021

• counterexample config

  fabioali

  committed
  afb3cd7

  Copy full SHA for afb3cd7

Commits on Apr 12, 2021

• Gobra interpreter, options and master interpreter

  fabioali

  committed
  a7476b0

  Copy full SHA for a7476b0

• changed to use Gobra Interpreter instead

  fabioali

  committed
  2292284

  Copy full SHA for 2292284

Commits on Apr 14, 2021

• Product interpreter

  fabioali

  committed
  d82c5fd

  Copy full SHA for d82c5fd

• added debug by means of native counterexample

  fabioali

  committed
  8614480

  Copy full SHA for 8614480

• added translation out of Util, and subverted Pnode overlap issue

  fabioali

  committed
  5ff1f8d

  Copy full SHA for 5ff1f8d

• cleanup

  fabioali

  committed
  5151cdb

  Copy full SHA for 5151cdb

• added sfetycheck to option

  fabioali

  committed
  6cf2631

  Copy full SHA for 6cf2631

• added unboxin (experimental)

  fabioali

  committed
  c7979c3

  Copy full SHA for c7979c3

Commits on Apr 16, 2021

• sync

  fabioali

  committed
  0695bc3

  Copy full SHA for 0695bc3

• fixed Pnode overlap (by ignoring invalids)

  fabioali

  committed
  bcdabdc

  Copy full SHA for bcdabdc

• Merge branch 'master' of https://github.com/viperproject/gobra

  fabioali

  committed
  fe1df32

  Copy full SHA for fe1df32

Commits on Apr 19, 2021

• added Slices and Idexed interpreter

  Show description for 1a63e4b
  fabioali

  committed
  1a63e4b

  Copy full SHA for 1a63e4b

• added lit string entry

  fabioali

  committed
  b190b0e

  Copy full SHA for b190b0e

• added interpreters to mater interpreter

  fabioali

  committed
  0a171d0

  Copy full SHA for 0a171d0

• Added Strings to Entries and backtranslation,

  Show description for 5cd39ad
  fabioali

  committed
  5cd39ad

  Copy full SHA for 5cd39ad

Commits on Apr 20, 2021

• added names for in-domain functions

  Show description for ae45520
  fabioali

  committed
  ae45520

  Copy full SHA for ae45520

• added names to interpreter

  fabioali

  committed
  cc5a1a4

  Copy full SHA for cc5a1a4

• added pointers interpreter (WIP)

  fabioali

  committed
  d8469a6

  Copy full SHA for d8469a6

• cleanup of direcory

  fabioali

  committed
  59add40

  Copy full SHA for 59add40

• cleanup gitignore

  fabioali

  committed
  d7456a1

  Copy full SHA for d7456a1

Commits on Apr 23, 2021

• lazyness for debugging

  fabioali

  committed
  d0c4bc0

  Copy full SHA for d0c4bc0

• improved pointers

  fabioali

  committed
  ccbd308

  Copy full SHA for ccbd308

• added default entries for types

  fabioali

  committed
  b001d69

  Copy full SHA for b001d69

• imrpved pointer interpreter

  fabioali

  committed
  d198faa

  Copy full SHA for d198faa

Commits on Apr 25, 2021

• resoved recursive calls

  fabioali

  committed
  973c091

  Copy full SHA for 973c091

Commits on Apr 26, 2021

• cleanup

  fabioali

  committed
  997b35b

  Copy full SHA for 997b35b

Commits on Apr 27, 2021

• separated shared struct and normal struct

  fabioali

  committed
  ec82097

  Copy full SHA for ec82097

• fixed test by propagating typeinfo

  fabioali

  committed
  9886258

  Copy full SHA for 9886258

Commits on Apr 28, 2021

• pointer domains distinction

  fabioali

  committed
  de72fa8

  Copy full SHA for de72fa8

• added return (which is different than returnLabel)

  fabioali

  committed
  c204aa9

  Copy full SHA for c204aa9

Commits on Apr 29, 2021

• sanatized decalared adresses

  fabioali

  committed
  a8a11dd

  Copy full SHA for a8a11dd

• mitigated adressable variables

  fabioali

  committed
  5682058

  Copy full SHA for 5682058

• sanitation of values

  fabioali

  committed
  29f2e35

  Copy full SHA for 29f2e35

Commits on May 3, 2021

• imroved prettyprint

  fabioali

  committed
  308a59a

  Copy full SHA for 308a59a

• shared struct improvement

  fabioali

  committed
  9f64b9b

  Copy full SHA for 9f64b9b

• improved fieldname

  fabioali

  committed
  cb5de9e

  Copy full SHA for cb5de9e

Commits on May 4, 2021

• iproved addresses of shared Structs

  fabioali

  committed
  c611817

  Copy full SHA for c611817

• pretty struct,

  Show description for 0300315
  fabioali

  committed
  0300315

  Copy full SHA for 0300315

• whitespaceless fix

  fabioali

  committed
  c86c0b4

  Copy full SHA for c86c0b4

Commits on May 7, 2021

• fixed addressed pointer issue

  fabioali

  committed
  0a61951

  Copy full SHA for 0a61951

• sorted test output for easier checking

  fabioali

  committed
  294abee

  Copy full SHA for 294abee

Commits on May 8, 2021

• fields

  fabioali

  committed
  8e3c0a8

  Copy full SHA for 8e3c0a8

• named types for literals

  fabioali

  committed
  4d17871

  Copy full SHA for 4d17871

Commits on May 10, 2021

• interface begin

  fabioali

  committed
  b54c4df

  Copy full SHA for b54c4df

• removed asresses from test string

  fabioali

  committed
  010831f

  Copy full SHA for 010831f

Commits on May 14, 2021

• Slices no longer depend on all of the original

  fabioali

  committed
  91927a0

  Copy full SHA for 91927a0

• moved adressed outside of array

  fabioali

  committed
  c42275e

  Copy full SHA for c42275e

• cleanup

  fabioali

  committed
  ed11954

  Copy full SHA for ed11954

• removed pointer values from test string

  fabioali

  committed
  7792b8c

  Copy full SHA for 7792b8c

Commits on May 17, 2021

• start of interface interpreter

  fabioali

  committed
  4b1b5ee

  Copy full SHA for 4b1b5ee

Commits on May 22, 2021

• added interfaces fo any non pointer types

  fabioali

  committed
  e694f9d

  Copy full SHA for e694f9d

Commits on May 25, 2021

• added sequences, improved named types

  fabioali

  committed
  d0cc22a

  Copy full SHA for d0cc22a

Commits on May 26, 2021

• added possibility for unresolved interfaces

  fabioali

  committed
  e4abbe0

  Copy full SHA for e4abbe0

Commits on May 30, 2021

• improved interfaces

  fabioali

  committed
  41b008b

  Copy full SHA for 41b008b

• correct interface poly matching

  fabioali

  committed
  5f64756

  Copy full SHA for 5f64756

• better filterning of unnecessary values

  fabioali

  committed
  f99d1fe

  Copy full SHA for f99d1fe

Commits on Jun 9, 2021

• added channels

  fabioali

  committed
  3d8acb1

  Copy full SHA for 3d8acb1

Commits on Jun 11, 2021

• added perms and heap entries

  fabioali

  committed
  4a1816c

  Copy full SHA for 4a1816c

• improved channel interpretation

  fabioali

  committed
  091ff89

  Copy full SHA for 091ff89

Commits on Jun 21, 2021

• added predicate translation

  fabioali

  committed
  c84d95e

  Copy full SHA for c84d95e

• made permission an option

  fabioali

  committed
  ee9a593

  Copy full SHA for ee9a593

Commits on Jun 27, 2021

• added predicate interpreteation

  fabioali

  committed
  9c623cd

  Copy full SHA for 9c623cd

Commits on Jun 28, 2021

• Channel improvements

  fabioali

  committed
  79cbb78

  Copy full SHA for 79cbb78

• Merge branch 'master' of https://github.com/viperproject/gobra

  fabioali

  committed
  66e1c91

  Copy full SHA for 66e1c91

Commits on Jul 5, 2021

• cleanup after merge

  fabioali

  committed
  365e54a

  Copy full SHA for 365e54a

Commits on Jul 6, 2021

• added sparsity

  fabioali

  committed
  5a6ad0a

  Copy full SHA for 5a6ad0a

Commits on Jul 8, 2021

• sync

  fabioali

  committed
  bba2cb5

  Copy full SHA for bba2cb5

Commits on Jul 9, 2021

• ghost slices, cleanup of sparsity

  fabioali

  committed
  cf5ba7d

  Copy full SHA for cf5ba7d

Commits on Jul 14, 2021

• Added better support for Gobra IDE

  fabioali

  committed
  02acdf8

  Copy full SHA for 02acdf8

Commits on Jul 18, 2021

• Added translation for UserDomains

  fabioali

  committed
  fdb776a

  Copy full SHA for fdb776a

Commits on Jul 21, 2021

• addded string concatination to translation

  fabioali

  committed
  1f9af32

  Copy full SHA for 1f9af32

Commits on Jul 23, 2021

• reduced counterexamples

  fabioali

  committed
  d8c9caa

  Copy full SHA for d8c9caa

Commits on Aug 6, 2021

• added reduced option

  fabioali

  committed
  2bbfbc7

  Copy full SHA for 2bbfbc7

Commits on Aug 19, 2021

• cleanup

  fabioali

  committed
  a19c351

  Copy full SHA for a19c351

• added unit test to master

  fabioali

  committed
  f28dcdb

  Copy full SHA for f28dcdb