Case studies of the BinderAnn GHC plugin
Compile and run it using ./run_dotgen.sh
Output:
digraph G {
green;
yellow;
red;
green -> yellow;
yellow -> red;
red -> green;
}
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" ==================
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
...
Compile and run it using ./run_GRACe.sh
Output:
{'capacity' : 6,
'flow' : 6,
'overflow' : 1,
'inflow' : 4}