SATABS Homepage Predicate Abstaction with SAT for ANSI-C

SNU Real-Time Benchmarks

Program Description
adpcm.c CCITT G.722 ADPCM (Adaptive Differential Pulse Code Modulation) algorithm
bs.c binary search program
crc.c CRC (Cyclic Redundancy Check) example program
fft1.c FFT (Fast Fourier Transform) using Cooly-Turkey algorithm
fft1k.c FFT (Fast Fourier Transform) for 1K array of complex numbers
fibcall.c Fibonacci series function
fir.c FIR filter with Gaussian number generation
insertsort.c Insertion sort
jfdctint.c JPEG slow-but-accurate integer implementation of the forward DCT
lms.c LMS adaptive signal enhancement
ludcmp.c LU decomposition algorithm
matmul.c Matrix multiplication
minver.c Matrix inversion algorithm
qsort-exam.c non-recursive quick sort algorithm
qurt.c Root computation of quadratic equations
select.c N-th largest number selection algorithm
sqrt.c Square root calculation
svd.c SV decomposition algorithm

The files are taken from http://archi.snu.ac.kr/realtime/benchmark/.

The original files require some minor modifications in order to make them ANSI-C compliant.

Examples:

float sin(rad)
float rad;
{

was replaced with

float sin(float rad)
{

int a[SIZE+1][SIZE+1] = { 0,0,0,0,0,0,
  0,0,9,4,7,9,
  0,12,14,15,16,11,
  0,2,3,4,5,6,
  0,4,3,2,1,2,
  0,2,7,6,4,9 };

was replaced with

int a[SIZE+1][SIZE+1] = { {0,0,0,0,0,0},
  {0,0,9,4,7,9},
  {0,12,14,15,16,11},
  {0,2,3,4,5,6},
  {0,4,3,2,1,2},
  {0,2,7,6,4,9} };
return;

was replaced with

return 0;

if it appears in 'int main() {...}'.

in the file bs.c:

binary_search(x)
{

was replaced with

binary_search(int x)
{

x was clearly used as an int inside binary_search(x).

and

main()
{
  binary_search(8);
}

was moved.

 

Download

 

Instructions

  1. Download the tarball (see above) and unpack the files.

  2. Run

    satabs file.c --show-claims

    to obtain the list of claims. Use

    satabs file.c --claim Nr

    to check a specific claim.

    Alternatively, you can use our Eclipse plugin for SATABS, as described in the SATABS user manual.