This software is made available under the Open Government License v3.0. Please attribute to United Kingdom - Norway Initiative, http://ukni.info (2016) ********************************************************************** Introduction ********************************************************************** This readme is intended as a quick introduction into how to build, run and analyse the Ada UKNI IB. More details on the code and the compilation and analysis setup can be found in the IB Software Development Report. The following topics are presented * building the code from the command line * editing the ihex file to insert CRC * downloading the code * analysing the code from the command line * toolsets used Building and analysing the code can also be done via GPS. For more information on how to perform these operations, see the GPS user guides. Make sure that all the tools listed in the "toolsets used" section are installed and in the path. ********************************************************************** Building the code from the command line ********************************************************************** To build the code base from the command line, perform the following steps (where > is used to denote the command prompt): * extract the zipped source code files into a new folder (e.g. c:\MYPATH\ib) * create a build folder to build the source into (e.g. C:\MYPATH\IB_Phase3_Build) * open up a command prompt * change directory into the build folder (where C:\MYPATH\IB_Phase3_Build is an existing folder to build into) > cd C:\MYPATH\IB_Phase3_Build * type the following into the prompt (where c:\MYPATH\ib contains the source code) > gprbuild --target=avr -d -PC:\MYPATH\ib\ib.gpr Main.adb -s * convert the produced file into an ihex file > avr-objcopy -O ihex main main.ihex * fill the rest of the ihex file with zeros > srec_cat main.ihex -intel --crop 0 0x3FFFF --fill 0x00 0x0000 0x40000 -output main.ihex -intel --address_length=2 --line_length=44 ********************************************************************** Editing the ihex file to insert CRC ********************************************************************** The generated file will not have the correct CRC at the end of the file. The CRC check is part of the IB start-up integrity checks. * open the main.ihex file (from C:\MYPATH\IB_Phase3_Build contains the main.ihex file) * edit the last line of the ihex file (starting :10FFF0) to contain the CRC (calculated as per application note AVR236). For the provided code this is CEB3 * calculate the checksum (required to ensure the ihex is in valid intel hex file format) as the twos complement of the entire line (including the CRC bytes added). For the provided code this is 80 * the last line of the code is: :10FFF0000000000000000000000000000000CEB380 ********************************************************************** Downloading the code ********************************************************************** To use a JTAGICE mkII in JTAG mode to download the code onto the AVR using AVR Studio 4.0 * on the main Tab select Device = ATmega2560 Programming Mode and Target Settings = JTAG mode * on the Fuses Tab set EXTENDED= 0xFF HIGH = 0x99 LOW = 0xFF7 * on the LockBits tab set LOCKBIT = 0xFF * on the Program Tab select Flash Input HEX File = C:\MYPATH\IB_Phase3_Build\main.ihex Press the "Program" button in the Flash section * If the code has successfully downloaded and the CRC correctly calculated, the IB will illuminate the LEDS as per the IB start-up routine ********************************************************************** Analysing the code from the command line ********************************************************************** To analyse the code from the command line, perform the following steps (where > is used to denote the command prompt) * open up a command prompt * change the current directory to the folder containing the source code > cd c:\MYPATH\ib * clean the old analysis files > sparkclean * use the SPARK examiner to examine the files > spark -pl -flow_analysis=information -html -index_file=C:\MYPATH\ib\Main.idx -vcg -config=C:\MYPATH\ib\config.cfg -error_explanations=first -dpc -language=2005 -statistics -warning_file=C:\MYPATH\ib\warnings.wrn -output_directory=C:\MYPATH\ib\SPARK_Output -casing -rules=keen @main.smf * change directory to the SPARK output folder > cd SPARK_Output * run the Spark simplifier > sparksimp -p=1 -nz -l -sargs "-plain" * the proof checker is used to discharge the undischarged verification conditions. Change directory to enable the checker to be run on this file > cd c:\MYPATH\ib\SPARK_Output\toolbox_\peak_net_area\ * run the proof checker > checker -exec=roi_02 roi_area.siv * change directory to where all the output files are stored > cd c:\MYPATH\ib\SPARK_Output * run the Proof ObliGation Summariser tool to collate the results > pogs -i ********************************************************************** Toolsets used ********************************************************************** The following toolsets were used: * GPS 6.0.0 (20131030) * GNAT Pro 7.0.1 (20120104-45) * SPARK 11.1.0 (26142) * srec_cat 1.42.D001 * AVR Studio 4 (4, 19, 0, 730)