The main guidance system consists of a number of more or less independent subsystems, linked at the top level. Each subsystem listed below has a package spec and body with the same name in which it handles reading of the data from the device and writing control information from the device. It also has a package spec and body where the name is prefixed if_ which is the test harnesses' mock-up of the sensor. As an example, the Airspeed subsystem implements its reading and writing in airspeed.ads, airspeed.adb and has its mock-up in if_airspeed.ads, if_airspeed.adb.
The test_harness.adb file is the Ada main program for the system. It takes commands from standard input, parses them and either executes changes in the if_... packages or monitors the state of subsystems.
The test harness has a Cycle command which runs each subsystem component through one polling cycle. This emulates a 20ms slice of system operation. Multiple cycles can be run with the Cycle_Many N command where N is the number of cycles required.
The code is set up for comprehensive SPARK analysis including full proof of absence of run-time errors (exceptions). There is a spark.sw switch which defines the standard options to be used for SPARK analysis, including use of the missile.idx index file, the missile.wrn warning control file, and use of .lss, .lsb extensions for specification and body listing files respectively.
The -exp switch generates proof obligations to show the absence of any run-time errors including those for expression overflow. For this purpose it uses the gnat.cfg file that specifies the type sizes for a specimen target compiler. If you are planning to run this code on a real system, check that the type sizes are correct for your target compiler.
The system Makefile is set up to use the pogs and sparksimp tools to simplify and log the system proofs.