CBMC Test Case

test_case.c

#include <assert.h>
#include <stdbool.h>
#include <stdlib.h>

struct list_entry {
	struct list_entry *next;
};

struct linked_list {
	struct list_entry *head;
	struct list_entry **tail;
};

struct linked_list_container {
	struct linked_list list;
};

int main(int argc, char* argv[])
{
	struct linked_list_container container;
	struct linked_list *list = &container.list;
	struct list_entry head;

	list->head = NULL;
	list->tail = &list->head;

	*list->tail = &head;
	list->tail = &head.next;

	assert(list->head);

	return 0;
}

test_case.log

CBMC version 5.4 64-bit x86_64 linux
Parsing test_case.c
Converting
Type-checking test_case
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 47 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
564 variables, 540 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.002s
Building error trace

Counterexample:

State 18  thread 0
----------------------------------------------------
  argv'[4098]=((char *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 21 file test_case.c line 18 thread 0
----------------------------------------------------
  argc=4098 (00000000000000000001000000000010)

State 22 file test_case.c line 18 thread 0
----------------------------------------------------
  argv=argv' (0000001000000000000000000000000000000000000000000000000000000000)

State 23 file test_case.c line 20 function main thread 0
----------------------------------------------------
  container={ .list={ .head=((struct list_entry *)NULL), .tail=((struct list_entry **)NULL) } } ({ { 0000000000000000000000000000000000000000000000000000000000000000, 0000000000000000000000000000000000000000000000000000000000000000 } })

State 24 file test_case.c line 21 function main thread 0
----------------------------------------------------
  list=((struct linked_list { struct list_entry *head; struct list_entry **tail; } *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 25 file test_case.c line 21 function main thread 0
----------------------------------------------------
  list=&container!0@1.list.head (0000001100000000000000000000000000000000000000000000000000000000)

State 26 file test_case.c line 22 function main thread 0
----------------------------------------------------
  head={ .next=((struct list_entry *)NULL) } ({ 0000000000000000000000000000000000000000000000000000000000000000 })

State 27 file test_case.c line 24 function main thread 0
----------------------------------------------------
  container={ .list={ .head=((struct list_entry *)NULL), .tail=((struct list_entry **)NULL) } } ({ { 0000000000000000000000000000000000000000000000000000000000000000, 0000000000000000000000000000000000000000000000000000000000000000 } })

State 28 file test_case.c line 25 function main thread 0
----------------------------------------------------
  container={ .list={ .head=((struct list_entry *)NULL), .tail=&container!0@1.list.head } } ({ { 0000000000000000000000000000000000000000000000000000000000000000, 0000001100000000000000000000000000000000000000000000000000000000 } })

State 29 file test_case.c line 27 function main thread 0
----------------------------------------------------
  invalid_object0=&head!0@1.next (0000010000000000000000000000000000000000000000000000000000000000)

State 30 file test_case.c line 28 function main thread 0
----------------------------------------------------
  container={ .list={ .head=((struct list_entry *)NULL), .tail=&head!0@1.next } } ({ { 0000000000000000000000000000000000000000000000000000000000000000, 0000010000000000000000000000000000000000000000000000000000000000 } })

Violated property:
  file test_case.c line 30 function main
  assertion list->head
  list->head != ((struct list_entry *)NULL)

VERIFICATION FAILED