The installation process of C32SAT which is described in the appendix of the master thesis "C32SAT: A Satisfiable Checker for C Expressions" has been changed. The new installation process works as follows: 1 INSTALLING C32SAT WITH THE SATSOLVER NANOSAT (default) ------------------------------------------------------------------------------ First you have to download the satsolver NANOSAT from the software archive of the institute of formal models and verification. NANOSAT can be found at http://fmv.jku.at/nanosat/. 1.1 USING C32SAT's NANOSAT PRECONFIGURATION (default) ------------------------------------------------------------------------------ Extract NANOSAT into the same directory in which you have extracted C32SAT. Do NOT extract NANOSAT into the root directory of C32SAT! Finally, rename the directory "nanosat-1.X" into "nanosat": mv nanosat-1.X nanosat Goto section 1.3 1.2 EDITING C32SAT's NANOSAT CONFIGURATION MANUALLY (alternative) ------------------------------------------------------------------------------ If you have already installed NANOSAT on your system and you don't want to copy NANOSAT into the same directory in which you have extracted C32SAT then you can edit C32SAT's configuration files as described in 1.2.1, 1.2.2 and 1.2.3. 1.2.1 CONFIGURING AND COMPILING MAKEFILE GENERATOR ------------------------------------------------------------------------------ Go into the directory "config/makefile_generator/" and open the file "nanosat.conf". Edit the variable "SATSOLVER_DIR" which holds the path to NANOSAT. If you want to use a relative path then this path has to be relative to the root directory of C32SAT. Save your configuration. Repeat this process for the file "nanosat_test.conf". The only difference ist that if you want to use a relative path then this path has to be relative to the test directory of C32SAT. Finally, call "make" to compile the makefile generator. 1.2.2 CONFIGURING AND COMPILING SATSOLVER CONFIG GENERATOR ------------------------------------------------------------------------------ Go into the directory "config/satsolver_config_generator/". Open the file "nanosat.conf". Edit the variable "HEADER" so that it points to the NANOSAT headerfile "nanosat.h". If you want to use a relative path then this path has to be relative to the C32SAT root directory. Save your configuration and call "make" to compile the satsolver config generator. 1.2.3 GENERATING FINAL CONFIGURATION ------------------------------------------------------------------------------ Go into the directory "config" and call the shell script "generate_config_nanosat.sh". This script calls the makefile generator and the satsolver generator and generates the corresponding configurations so that C32SAT can work with NANOSAT. 1.3 CONFIGURING AND COMPILING NANOSAT ------------------------------------------------------------------------------ Go into the root directory of NANOSAT and edit the file "configure". Set the value of the variable "log" to "no" and save the file. Now call "configure" to start the configuration process of NANOSAT. Call "make" to compile NANOSAT. Finally, you should run NANOSAT's test suite to verify that NANOSAT works correctly on your system. Simply call the command "test" to run the test suite. 1.4 CONFIGURING AND COMPILING C32SAT ------------------------------------------------------------------------------ C32SAT is preconfigured for the i686 architecture. If you use an incompatible architecture then you have to edit the corresponding GCC compilerflag in the makefile. The makefile can be found in the root directory of C32SAT. Call "make project" in the root directory of C32SAT. The whole C32SAT project should now be compiled and linked against the NANOSAT library. Calling "make help" lists you all make options of C32SAT. Finally, you should run C32SAT's test suite to verify that C32SAT works correctly on your system. Simply call "make run_tests" in the root directory of C32SAT. 2 DOCUMENTATION (optional) ------------------------------------------------------------------------------ This section discusses the available documentation of C32SAT. 2.1 MAIN DOCUMENTATION ------------------------------------------------------------------------------ The main documentation of C32SAT is the master thesis "C32SAT:A Satisfiability Checker for C Expressions" by Robert Brummayer. It can be downloaded at http://www.fmv.jku.at/c32sat/. 2.2 CODE DOCUMENTATION ------------------------------------------------------------------------------ A documentation of the source can be generated by the tool Doxygen which can be found at http://www.doxygen.org. Just run it on the configuration file "doxyconfig" to generate the code documentation. Doxygen generates a subdirectory "doc/html" where the code documentation can be found. The Doxygen configuration file of C32SAT can be found in the root directory of C32SAT. The Doxygen configuration file of C32SAT's test suite can be found in the directory "test".