Skip to content
Go to file

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time


PsycheC is a compiler frontend infrastructure for the C language that is enabled with an ML/Haskell-style (unification-based) type inference engine. This online interface illustrates the essential functionality of PsycheC.


  • Enabling static analysis on partial programs.
  • Supporting semantic tools despite of #include failures.
  • Compiling a code snippet (e.g., retrieved from a bug tracker).
  • Generating test-input data for a function, individually.
  • Prototyping of an algorithm without a type specification.

Be creative!


To build PsycheC:

  • Cmake
  • C++14 compiler
  • Haskell Stack

To use PsycheC (download here):

  • Python 3


cmake CMakeLists.txt  

Setting Up

export PATH=$PATH:/path/to/psychec


The simplest way to use PsycheC is through the Cnippet compiler adaptor.

Let us see an example.

Consider the file node.c below.

// node.c
void f()
    T v = 0;
    v->value = 42;
    v->next = v;

If you were to compile node.c with GCC/Clang, you would issue a command similar to this one:

gcc -c node.c

As a result, an object file node.o would have been produced. However, this will not happen, since a declaration for T is not available. Instead, you will get an "undeclared identifier" error.

Now, if you invoke Cnippet, the compilation succeeds (flag -f is for non-commercial use).

./ -f gcc -c node.c

That is because, under the hood, PsycheC will infer the necessary missing definitions.

typedef struct TYPE_1__
    int value;
    struct TYPE_1__* next;
}* T;

Generic Programming

This is a work-in-progress, feedback is welcome through this form.

PsycheC provides an alternative to void* and #macros for writing generic code in C. This is how you would implement a generic linked-list's prepend function.

_Template void prepend(_Forall(node_t)** head,
                      _Forall(value_t) value)
    node_t* n = malloc(sizeof(node_t));
    n->value = value;
    n->next = *head;
    *head = n;

It is not necessary to define neither node_t nor value_t. The definition of prepend applies "for all" kinds of nodes and values. This way, you can focus on the algorithms (the essence of generic programming).

Let us create 2 lists, one of int and another of point_t, and insert an new head to them.

int main()
    _Exists(node_t)* ilst = 0;
    prepend(&ilst, 42);

    _Exists(node_t)* plst = 0;
    struct point_t p;
    p.x = p.y = 42;
    prepend(&plst, p);

Now, PsycheC infers that there "exists" a (node) type whose value is an int, together with an specialization of prepend for such arguments. A different (node) type for point_t "exists" too, with its corresponding specialization of prepend.

Check the examples directory for this snippet.

Running the Tests

./psychecgen -t
cd solver && stack test && cd -
cd formalism && ./


PsycheC is an ongoing research project. It has been presented at:

Below is a list of papers whose developed tooling rely on PsycheC:

An small article about PsycheC:


C compiler frontend enabled with Haskel/ML-style type inference





No releases published


No packages published
You can’t perform that action at this time.