BinderAnn-examples

Case studies of the BinderAnn GHC plugin

dotgen

Original repo

Test File

Compile and run it using ./run_dotgen.sh

Output:

digraph G {
green;
yellow;
red;
green -> yellow;
yellow -> red;
red -> green;
}

sbv

Original repo

Test File

Compile and run it using ./run_sbv.sh

Output:

...

== BEGIN: "addSub.c" ================
/* File: "addSub.c". Automatically generated by SBV. Do not edit! */

#include "addSub.h"

SInt32 addSub(const SInt32 x, const SInt32 y, SInt32 *diff)
{
  const SInt32 s0 = x;
  const SInt32 s1 = y;
  const SInt32 s2 = s0 - s1;
  const SInt32 s3 = s0 + s1;

  *diff = s2;
  return s3;
}
== END: "addSub.c" ==================

shellmate

Original repo

Test File

Compile and run it using ./run_shellmate.sh

Output:

...
shellmate-test: Exception raised at test/Test.hs(18,3):
The value "mem" produced the following error:
Command `cat' failed with error code 1
...

GRACe

Original repo

Test File

Compile and run it using ./run_GRACe.sh

Output:

{'capacity' : 6,
'flow' : 6,
'overflow' : 1,
'inflow' : 4}