B Compiler In Depth

Introduction

This section presents all options of the B Compiler: input/output, analysis, and compiler options.

 

Input/Output Options

Input/Output options section will show you how use command tools who allow to have a better organization of your project. With those options, will can change the output path, add different input path to search files, all of that exist in order to give you more flexibility when you work on big project

Option « -i »

This option allows to specify the input file upon which a syntaxic analysis is performed. If no error is displayed, then the B model is correct.

Example : bcomp.exe -i M1_i.imp

 

Option « -h »

This option allows to generate a hmtl dump of the Betree resulting from the analysis of the input B model. The html files are generated in the directory containing the B model. The top level html file is main.html

Example : bcomp.exe -i M1_i.imp -h

Below is a page resulting from the analysis of a model: 

 

Option « -I »

This option allows to specify additional directory where input files are searched for.

Example : bcomp.exe -i M1_i.imp -I /include/A

 

Option « -L »

This option allows to specify an Atelier B project db file, where inputs files can be searched for.

Example : bcomp.exe -i M1_i.imp -L lib.db

 

Option « -P »

This option allows to specify a directory where output are generated. The directory must have been created before executing the command, unless the output files are generated in the local directory.

Example : bcomp.exe -P /html -i file.txt  -T output_file.html

 

Option « -r »

This option allows to specify a resource file.

   Syntax example : bcomp.exe -i file.txt -r file.txt

 

Option « -M »

This option allows to specify a file where dependency information is stored.

Example : bcomp.exe -i M1_i.imp -M output.txt

In this example, output.txt contains:

   M1_i.imp: 
         M1.mch

This syntax represents the hierarchy of implementation and machines files.

 

Analysis options

These options allow to specify which verifications have to be performed on the input model.

 

Option « -d »

This option allows to perform a dependency analysis. Dependency errors, if any, are displayed during the analysis.

Example : bcomp.exe -i M1_i.imp -d

 

Option « -a »

This option allows to perform a semantic analysis. Semantic errors, if any, are displayed during the analysis.

Example: bcomp.exe -i M1_i.imp -a

 

Option « -c »

This option allows to perform a B0 check (compliance with B0 definition: implementation should be implementable). B0 errors, if any, are displayed during the analysis.

Example : bcomp.exe -i M1_i.imp -c

 

Compiler options

These options allows to fine tune the behaviour of the B compiler as well as to display additional information.

 

Option « -C »

This option allows to print and report compilation informations, which are not printed by default, that would help to understand error messages.

Example : bcomp.exe -i M1_i.imp -C

Below is a page resulting from the analysis of a model: 

 

Option « -S »

This option sets the compiler into the strict B mode, allowing to only check compliancy with B language specification.

Example : bcomp.exe -i M1_i.imp -S

 

Option « -v »

This option sets the compiler into the verbose mode, leading to print more information about the behaviour of the B Compiler.

Example : bcomp.exe -i M1_i.imp -v

 

Option « -Wall » & « -Wno »

This option allows to specify if warnings are displayed or not, when a model is analyzed:

  • Wall allows to print extended warnings
  • Wno disables all warnings
Example : bcomp.exe -i M1_i.imp -Wall
Example : bcomp.exe -i M1_i.imp -Wno

 

Option « -k »

This option allows to display component checksums during analysis.

Example : bcomp.exe -i M1_i.imp -k

 

Option « -K »

This option allows to display clause checksums during analysis.

Example : bcomp.exe -i M1_i.imp -K

 

Option « -p »

This option allows to detect proof clashes.

Example : bcomp.exe -i M1_i.imp -p