Airac Family Seal Airac5
Static Analyzer for Automatic Detection of Buffer Overrun Errors in C Programs

RopasWork Spa-arrow.com/ Programming Research Laboratory
Seoul National University

Introduction

Airac5는 할당한 메모리 영역을 벗어나서 접근하는 C 프로그램 오류(buffer overrun error)의 위치를 미리 모두 자동으로 찾아준다.
예를 들어, 아래의 파란색 식들중에서 배열 a의 범위를 벗어나는 식들을 모두 찾아준다.

    int *a = (int *)malloc(sizeof(int)*10);          /* int array of size 10 */
    a[i] = 1; a[i + f()] = 1; a[*k + (*g)()] = 1; /* accesses to a */
    x = a;            x[1] = *(x+1)+1;                /* a and x are aliases */
    y = a + f();    y[*(y+1)] = 1;                    /* some of a and y are aliases */
    z->v = a;       (z->v)+i = 1;                      /* a is pointed to by a struct */

Airac5 statically detects all buffer-overrun errors in C programs.
For example, in the above C expressions where blue-colored expressions access array a, Airac5 detects all accesses that can overrun the target array.

QnA

Keywords
  • C: Airac5 supports the full set of ANSI C + some GNU C extensions.
  • all: Airac5 detects all buffer-overrun places in source code.
  • statically: Airac5 analyzes source code at their compile-time.
  • false alarms: Airac5 inevitably reports some false alarms.
  • always stops: Airac5 always finishes even for infinite-loop programs.
  • automatic: Airac5 is fully automatic.
  • modular: Airac5 accepts separate C files that constitute a program.
  • correct: Airac5's design is formally founded.

Online Demo

Free On-Site Trial

We prove Airac5 on-site. We don't ask you to ship your code off-site.
  • We visit your site in person to run Airac5 for your C code.
  • This trial is for corportations only, not for individual C programmers.
  • Individual C programmers can download the free trial version below.
Email us (run@ropaswork DOT com) to register for a trial.

Download

Performance

References

Contact

Prof. Kwangkeun Yi
(office) +82 2 880 1857
(mobile) +82 11 895 9374
(email) kwang@ropaswork/com (with . for /)
Spa-arrow.com
Programming Research Laboratory
Seoul National University
© Copyright 2005, 2006, 2007, 2008 Spa-arrow.com, Programming Research Lab., Seoul National University