Development environment

Development environment prerequisites

• a C/C++ compiler to compile the code generated by the tests.
• cmake and make is needed in order to run the tests.
• valgrind is needed to run memory management tests that check for memory leaks.

Compiler tool dependencies

Install glib

• ubuntu

sudo apt-get install libglib2.0

• OSX

brew install glib

Install gettext

gettext is not present on OSX so install it with

brew install gettext
brew link --force gettext

Using Eclipse

Please install: CDT + C/C++ Unit Testing Support

Other packages

• ubuntu

sudo apt-get install cmake make gcc g++

Compiling

The generated code is tested using googletest, which is available via a git submodule. This submodule must be initialised after a successful checkout:

1. git submodule update --init
2. Enter the directory c
3. Either:

• for release cmake .
• for debug

cmake -DCMAKE_BUILD_TYPE=Debug .

3. To build it: make

Development

The translation is developed in two parts:

1. A C library, stored in <root>/c/vdmclib, containing:

• Library support for all operations that can be carried our on numbers, sets, seqs, maps etc.
• Library support providing a number of macros to ease class encoding

2. A translation of VDM into C using this library

Import the entire runtime in Eclipse

1. execute cmake in the root (and make sure you have initialised the googletest submodule)
2. Create a new C++-project in Eclipse based on a standard makefile project using your avaliable tool chain.

• Name the project with the name of the cmake project you want to import
• Select source location to be the location of the cmake project

3. Build the project to see if Eclipse picks up the imports

• If it do not pickup the includes then use the fix below

Update CDT GCC Build Output Parser to work with CMake on OSX

1. Goto Project Properties -> C/C++ General -> Preprocessor Include Paths, Macros etc.
2. Enable CDT GCC Build Output Parser
3. Change the Compiler Command Pattern to (.*gcc)|(.*[gc]\+\+)|(.*cc)|(clang)

Source: https://developer.mozilla.org/en-US/docs/Eclipse_CDT

Running tests

• To run the tests one must pass the location of the VDM library as a property -DVDM_LIB_PATH="/path/to/vdm2c-exploration/c-examples/lib"
• Pass the -DTEST_OUTPUT property to get the googletest output

Test the runtime library

All the code used to test the runtime library is stored in <root>/c/vdmclib/src/tests and written using the googletest framework. The tests are run automatically as part of the Maven build, but may also be executed manually using the steps below:

## Go into runtime library folder
cd <root>/c
## Generate the make file
cmake .
## Build the google test binary
make -j<no-of-cpu-cores-plus-one>
## Go to the folder that contains the tests
cd vdmclib/
## Run the generated google tests 
make test

The test report is available in report.xml

Notes

Using googletest

https://bjornarnelid.wordpress.com/2014/03/10/how-to-get-started-with-google-test-in-eclipse-cdt-on-linux/

Name mangling

https://en.wikipedia.org/wiki/Name_mangling http://www.avabodh.com/cxxin/namemangling.html

Eclipse editor for velocity

• Remember to install Eclipse 2.0 Style Plugin Support before trying to install the editor *

https://marketplace.eclipse.org/content/veloeclipse

Translation Notes

If one wants to use the C code from C++ it can be included as shown below:

extern "C"
{
#include "lib/TypedValue.h"
#include "lib/VdmBasicTypes.h"
...
}

Therefore:

• never use any C++ keywords in C. It leads to trouble later...

Transformation Rules

All nodes that is shared between VDM and C must have a C plain C template. This means it cannot use the VDM library for code generation.

Implementing classes

• http://www.pvv.ntnu.no/~hakonhal/main.cgi/c/classes/
• http://www.eventhelix.com/RealtimeMantra/basics/ComparingCPPAndCPerformance2.htm#.VmbPCuODFBc
• http://www.go4expert.com/articles/virtual-table-vptr-multiple-inheritance-t16616/
• http://www.go4expert.com/articles/virtual-table-vptr-t16544/

C/C++ language related stuff

• http://stackoverflow.com/questions/3523145/pointer-arithmetic-for-void-pointer-in-c
• https://www.cs.uaf.edu/2010/fall/cs301/lecture/10_15_struct_and_class.html
• http://www.eventhelix.com/RealtimeMantra/basics/ComparingCPPAndCPerformance2.htm#.VpmaslMrLUr
• https://en.wikipedia.org/wiki/Virtual_method_table
• http://www.go4expert.com/articles/virtual-table-vptr-multiple-inheritance-t16616/
• http://www.go4expert.com/articles/virtual-table-vptr-t16544/
• http://www.learncpp.com/cpp-tutorial/125-the-virtual-table/
• http://www.drdobbs.com/cpp/single-inheritance-classes-in-c/184406396?pgno=1
• http://www.pvv.ntnu.no/~hakonhal/main.cgi/c/classes

C Macro

• Compare arguments (#a==#b) http://stackoverflow.com/questions/33491170/whats-the-difference-in-the-and-in-the-following-c-code
• Statements inline eval http://stackoverflow.com/questions/4712720/typechecking-macro-arguments-in-c

Compiler -- platform dependent stuff

Remember that:

• malloc leaves the memory uninitialised
• calloc zero-initializes the buffer (which takes more time)

This is important since free only frees the memory if ptr != NULL

Other debugging related stuff

Core dump in terminal only

Enable the core to be dumped by:

ulimit -c unlimited

On Linux the core is dumped in the application folder, while OSX uses /cores/

Build vdm2c as standalone app

cd <root-of-vdm2c-repository>/core/vdm2c/
mvn install -DskipTests assembly:single

The standalone vdm2c application is located into <root-of-vdm2c-repository>/core/vdm2c/target named as vdm2c-<version>-SNAPSHOT-jar-with-dependencies.jar. To execute the CG run the following command:

java -jar vdm2c-<version>-SNAPSHOT-jar-with-dependencies.jar input_file.vdmrt -dest out_dir/