This directory contains a number of examples that illustrate the capabilities of
Progvis in different ways. The examples are divided into different categories
as follows:

- basics/

  This directory contains examples that show basic concepts in C, such as
  variables, function scope and the like.

  - loops.c: Shows various types of loops in action.

  - scope.c: Illustrates the difference between function scope and global scope.

  - recursion.c: Shows recursion in action. This particular example is designed to
    also have a proper understanding of scope (to see the different values of "result").

  - pintos_live.c: Larger example of C programming used to show how C++ concepts
    are typically implemented in C.

  - printf.c: Using printf to format output.

- pointers/

  This directory contains examples that illustrate how pointers and pointer
  arithmetics work in C.

  - stack_heap.c: Shows the difference between stack and heap allocations.

  - leak.c: Shows how a memory leak looks in the tool.

  - use_after_free.c: Shows how the tool handles use-after-free problems.

  - free_ptr.c: Another case of use after free.

  - locals.c: Show many pointer indirections to a local variable.

  - pointer_param.c: Shows how pointer-parameter can be used as output parameters.

  - struct.c: Shows how a struct is laid out in memory, and that we can use pointer
    arithmetics to step through it (although it is a bit dubious in practice).

  - array.c: Shows how an array is similar to a struct, and how pointer arithmetics
    correspond to the array-acces operator.

  - struct_array.c: Combines 'struct.c' and 'array.c'.

  - string.c: Illustrates how strings work.

  - tricky.c: A program we let students debug to learn to use the debugger. The bug
    is corrected in this version, but the tool illustrates very well how the program
    works, even though it is fairly tricky (with multiple levels of pointers etc.)

  - data_to_stack.c: Illustrates storing a pointer to stack-allocated memory in
    a heap-allocated data structure.

  - ptr.c: Complex pointers to illustrate the strengths of the visualization.

- concurrency/

  This directory contains examples that illustrate how concurrency issues can be
  detected by the tool.

  - shared_global.c: Two threads modifying a shared global variable
    concurrently. The tool will detect the concurrent writes (if executed in the
    same "step") and report the issue.

  - shared_by_ptr.c: Simple data shared by pointer to another thread. Written by
    one thread and read by the other. Once again, the tool reports this error if
    it is executed properly.

  - incorrect_sync.c: Illustrates a linked stack where the push function is not
    correctly synchronized. In this case, there are no data races, but since the
    critical section is split into two, we can still lose elements.

  - atomics.c: Illustrates various atomic operations available.

  - cond.c: Illustrates using a condition variable.

  - sum/: Summing a large arrays in various ways.

  - bank/: Many variants of a small program that simulates a bank. This example
    is not synchronized at all and can exhibit many kinds of incorrect
    behaviors. Try disabling "Run -> Track reads/writes" and try to find cases
    where funds are lost or created out of thin air. The "bank_bad.c" is
    synchronized with bad parallellism, others may contain deadlocks.

  - buffer/: An implementation of a circular buffer (a UNIX pipe). One thread
    reads from it while the other writes to it. This directory contains many
    versions of synchronizations, some that support multiple readers/writers,
    others don't.

  - philosophers/: Implementation of the classical Dining Philosopher's problem.

  - lock_impl/: Various classical lock implementations. These are useful only
    when using the simple memory model that enforces SC.

- cpp/

  This directory contains examples of some concepts in C++ that are potentially
  difficult to grasp, such as copy/move constructors, etc.

  Note that there are many aspects of C++ that are not implemented yet. For
  example, support for iostreams is currently missing.

  - references.cpp: This example shows how references work, and some potential
    issues with them.

  - special_members.cpp: Illustrates how and when special member functions are called.

  - self_assignment.cpp: Illustrates the issue of self-assignment in assignment operators.

  - return_complex.cpp: Illustrates how complex data types (may) be returned in C++.

- bs/

  This directory contains a few examples of code in Basic Storm. The point is to
  show that the tool is versatile and can be extended to support other languages
  as well.

  - list.bs: Creation of a linked list.

  - list2.bs: Creation of a linked list using inheritance and recursion.

  - array.bs: Creation of nested arrays. Note that tracing reads and writes is
    not currently working due to the abstractions around the dynamic arrays are
    not properly supported yet.

- test/

  This directory contains various examples used for testing various aspects of
  the implementation. They are not made to illustrate some concept in
  particular, but rather to exercise relevant parts of the implementation, and
  test it for correctness.
