Shape Analysis of Possibly Cyclic Singly-Linked Lists

This directory contains analyses of programs manipulating possibly cyclic singly linked lists of the form

typedef struct node {
   struct node *n;
   int data;
} *L;

Goal

The aim of the analyses is to verify:
  1. Absence of null dereferences. This property is checked in all examples;
  2. No memory leakage. This means that no elements become unreachable from the program variables.
  3. Output list is unshared and acyclic.
The first property is checked in all examples and the last two properties are checked only in appropriate examples (that perform list mutations).

List of examples and their descriptions

(see additional comments below)
Example Example description Properties checked Command line
create A function that creates new list of elements and appends them to the input list
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla create sll -props sll_cyclic.properties
delete A function that deletes an element with a specified value from a list
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla delete sll -props sll_cyclic.properties
deleteAll A function that deallocates all elements in a list
  1. Absence of null dereferences
  2. No memory leakage
tvla deleteAll sll -props sll_cyclic.properties
getLast A function that returns a pointer to the last element of a list Absence of null dereferences tvla getLast sll -props sll_cyclic.properties
insert A function that creates an element with a specified value and inserts it before the first element with a larger value
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla insert sll -props sll_cyclic.properties
merge A function that merges two ordered lists into one ordered list
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla merge merge -props sll_cyclic.properties
reverse A function that successfuly reverses a singly-linked list in-situ
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla reverse sll -props sll_cyclic.properties
reverse_fumble A function that attempts to reverse a singly-linked list but loses its elements
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla reverse_fumble sll -props sll_cyclic.properties
rotate A function that moves the first element to the position following the last element
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla rotate rotate -props sll_cyclic.properties
search A function that searches a list for an element with a specified value Absence of null dereferences tvla search sll -props sll_cyclic.properties
search_nullderef A function that searches a list for an element with a specified value and causes a null dereference Absence of null dereferences tvla search_nullderef sll -props sll_cyclic.properties
swap A function that swaps the first two elements in a list
  1. Absence of null dereferences
  2. No memory leakage
  3. Output list is unshared and acyclic
tvla swap sll -props sll_cyclic.properties

Comments on the way C functions are modelled by first-order transition systems

The original C functions were pre-processed in the following ways in order to simplify the analysis:
  1. Statements that assign to fields are preceded by statements that assign the value NULL to the fields.
    For example, x->n = y; is replaced with x->n = NULL; x->n = y;
  2. Statements that deallocate memory are preceded by statements that assign NULL to fields.
    For example, free(x); is replaced with x->n = NULL; free(x);
  3. Statements that copy a value from one field to another are simplified by using temporary variables.
    For example, x->n = y->n; is replaced with the sequence of assignments
    t = y->n; x->n = NULL; x->n = t; t = NULL;
Program conditions are modelled by two actions---one for the true branch and one for the false branch.
Update formulas for instrumentation predicates were produced manually.