Skip to content
forked from obicons/sa4u

Static Analysis for Unit Type Error Detection

Notifications You must be signed in to change notification settings

TangramFlex/sa4u

 
 

Repository files navigation

SA4U

SA4U is a static analyzer for detecting unit conversion errors in UAV source code.

Directory Layout

  • bugs/ - contains scripts to recreate bugs diagnosed by SA4U
  • demos/ - contains examples to analyze with SA4U
  • lsp/ - contains the SA4U VSCode extension
  • platforms/ - contains support data for SA4U to analyze special subjects
  • sa4u_z3/ - contains the source code for the latest SA4U

Running on a Demo

Step 1: Build Docker Image

$ (cd sa4u_z3 && docker image build -t sa4u ./)

Step 2: Invoke SA4U on demos/01

$ docker container run        \
  -v "$(pwd)/demos/01":/src/  \
  sa4u                        \
  -m /src/CMASI.xml           \
  -p /src/ex_prior.json       \
  -c /src/compile_commands_dir

You should see no errors.

Step 3: Insert an error in demos/01

Uncomment the first line in demos/01 that indicates that there is an error. Invoke SA4U like you did in step 2. You should see output like this:

ERROR!
  afrl::cmasi::Location3D::getAltitude return unit known from CMASI definition
  afrl::cmasi::Location3D::getAltitude known from CMASI definition
  Variable z declared in /src/ex.cpp on line 25 (1)
  Call to set_alt_in_cm in /src/ex.cpp on line 29 column 3 (9)
  Call to set_alt_in_cm in /src/ex.cpp on line 31 column 3 (10)

About

Static Analysis for Unit Type Error Detection

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • C++ 93.3%
  • Python 4.3%
  • TypeScript 1.3%
  • Shell 0.5%
  • Dockerfile 0.5%
  • JavaScript 0.1%