Restructure test suite folders

[viper-admin]

Created by @mschwerhoff on 2019-07-28 12:29
Last updated on 2019-07-28 12:30

The Silver test suite currently has the following directory structures:

all
  assume
  basic
  chalice
  domains
  functions
  heap-dependent_triggers
  import
    demo
    init_past
    issue203
      sub
    loop
    standard_import
  inhale_exhale
  invariants
  issues
    carbon
    silicon
    silver
  macros
  multisets
  old
  permissions
  permission_introspection
  predicates
  sequences
  sets
  third_party
    stefan_recent
    vercors
cfgtests
  determinism
examples
  binary-search
  graph-copy
  graph-marking
  longest-common-prefix
  max_array
  parallel-array-replace
  quickselect
  tree-delete-min
  vmcai2016
graphs
  static
    examples
    outlines
    tests
      binary
      lists
    unsound
import
  standard_import_tests
    loop_all
    loop_local
    loop_standard
plugintests
quantifiedcombinations
quantifiedpermissions
  consistency
  issues
  misc
  sequences
  sets
  third_party
quantifiedpredicates
  arity
  basic
  examples
  issues
  predicates
transformations
  ComplexMatching
  CopyPropagation
  CountAdditions
  DisjunctionToInhaleExhale
  FoldConstants
  IfThenElseTest
  ImplicationSimplification
  ImplicationsToDisjunction
  Imports
  Macros
    Expansion
    Hygienic  
  ManyToOneAssert
  MethodCallDesugaring
  Performance
  PresentationSlides
  QuantifiedPermissions
  UnfoldedChildren
  WhileToIfAndGoto
tutorial
wands
  examples
  examples_new_syntax
  examples_paper
  new_syntax
  regression

The current structure raises a couple of questions that should be addressed by a refactoring, e.g.:

• Which tests are in all? Clearly not all tests …
• Where should tests go that are not intended for verifiers/back-ends directly, and instead are read as inputs by a certain unit tests? This is the case for (most? all?) tests fromtransformations.
• Certain tests (e.g. in wands and quantifiedpermissions) were not added to all because they were initially only supported by one verifier, but are now supported by both. Should they be moved to all (or whatever will replace all)?
• Shouldn’t plugintests be part of the respective plugin?

[viper-admin]

@mschwerhoff commented on 2019-07-28 12:30

See also #268