Introduction
C for B (abbreviated as C4B) is a C code generator for Atelier B 4.0. Yes, another one …
The ComenC experiment was not successful for several reasons:
- ComenC code generator implements too many restrictions, issued form industrial safety critical code generators, that prevent the generation of C code in many cases or require to notably modify the B models.
- The underlying technology is outdated (Cocktail) and requires old machines to compile properly.
- Several bugs difficult to solve without redesigning the overall software.
Hence a new code generator has been designed, based on the B Compiler this time, and embedding less constraints to make it (we hope) more usable.
C4B is a translator, transforming a B model into a C program. It gathers experience gained during R&D projects as well as application to industry-strength case-studies.
C4B requires B models:
- typechecked
- 100% proved
- B0-checked: types used in the implementable model comply with the ones supported by C4B
Using C4B
C4B is integrated to Atelier B. However you could develop/contribute to a new version of C4B for experiment/bug correction. Hence it requires specific installation and use outside Atelier B. Basically you need to download C4B source code and ICU library (providing support for Unicode), and to compile it. Nothing too difficult.
Tutorial: How to compile C4B ?
And then launch C4B in a terminal on your existing B projects.
Status
C4B has been released as open source software (GPL v3.0) and is hosted on sourceforge.
Links
I have downloaded the C4b sources
and compiled it on WIN32 platform.
I followed your instructions note but
I needed to define some path in the CMakeCache.txt
file by hand regarding the DLL files for IUC libraries
because the name of those DLL depends on the IUC
release installed.
Another problem is that the intl.dll library and
intl.h files are not included in the MINGW distribution
so cmake cannot find them.
by chance I had those files in another GNU compiled tool.
Finally with the b2c.exe compiled I noticed
the following problem :
If I have the following machine
MACHINE Mach3 SETS ENS1 CONCRETE_CONSTANTS Func,Size PROPERTIES Func : ENS1 --> NAT1 & Size : NAT & Size = card(ENS1) END and its implementation: IMPLEMENTATION Mach3_i REFINES Mach3 VALUES ENS1 = (0..3); Func = (0..3)*{18}; Size = 4 END the code generated is #ifndef _Mach3_h #define _Mach3_h #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ #define Mach3__ENS1__max 3 /* Clause SETS */ typedef int Mach3__ENS1; /* Clause CONCRETE_VARIABLES */ /* Clause CONCRETE_CONSTANTS */ /* Basic constants */ #define Mach3__Size 4 /* Array and record constants */ extern const long Mach3__Func[Mach3__ENS1_card]; extern void Mach3__INITIALISATION(void); #ifdef __cplusplus } #endif /* __cplusplus */ #endif /* _Mach3_h */in that code the constant Mach3__ENS1__max is defined
but the constant Mach3__ENS1_card is missing.
Hello,
We have taken into account your remarks:
1.- We will modify the CMakeLists.txt to include the name of the IUC library post-fixed with a shell variable which must be defined with the version of the library installed in the system.
2.- The library intl is not used any more and it will be deleted from the CMakeLists.txt.
3.- We are currently working with the translator to fix the problems of arrays.
These changes will be incorporated in our next commits to the SourceForge repository.
Thank you for your feedback
Hello again,
I have another thing maybe you know already:
If you define a SET in a context machine
and if this one is valuated in the
implementation of this context machine
then “b2c” cannot translate properly the initialisation
of the arrays defined with this SET in external
machines that see the context machine.
But if you valuate everything in the same machine
the code tranlation is correct.
see here below:
MACHINE Ctxt SETS ENS1 END IMPLEMENTATION Ctxt_i REFINES Ctxt VALUES ENS1 = (0..3) END MACHINE Mach3 SEES Ctxt CONCRETE_CONSTANTS Func,initial_array PROPERTIES Func : ENS1 --> NAT1 & initial_array : ENS1 --> NAT1 END IMPLEMENTATION Mach3_i REFINES Mach3 SEES Ctxt VALUES Func = ENS1*{18}; initial_array = ENS1 * {3} END #ifndef _Ctxt_h #define _Ctxt_h #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ #define Ctxt__ENS1__max 3 /* Clause SETS */ typedef int Ctxt__ENS1; /* Clause CONCRETE_VARIABLES */ /* Clause CONCRETE_CONSTANTS */ /* Basic constants */ /* Array and record constants */ extern void Ctxt__INITIALISATION(void); #ifdef __cplusplus } #endif /* __cplusplus */ #endif /* _Ctxt_h */ #ifndef _Mach3_h #define _Mach3_h /* Clause SEES */ #include "Ctxt.h" #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ /* Clause SETS */ /* Clause CONCRETE_VARIABLES */ /* Clause CONCRETE_CONSTANTS */ /* Basic constants */ /* Array and record constants */ extern const long Mach3__Func[Ctxt__ENS1_card]; extern const long Mach3__initial_array[Ctxt__ENS1_card]; extern void Mach3__INITIALISATION(void); #ifdef __cplusplus } #endif /* __cplusplus */ #endif /* _Mach3_h */ #include "Mach3.h" /* Clause SEES */ #include "Ctxt.h" /* Clause CONCRETE_CONSTANTS */ /* Basic constants */ /* Array and record constants */ const long Mach3__Func[Ctxt__ENS1_card] = {}; /* ====> oopps ! should be {18,18,18,18} */ const long Mach3__initial_array[Ctxt__ENS1_card] = {}; /* ====> oopps ! should be {3,3,3,3} */ /* Clause CONCRETE_VARIABLES */ /* Clause INITIALISATION */ void Mach3__INITIALISATION(void) { ; }Thank you for your feedback.
I will add this issue to my list of improvements of c4b.
Hello,
I have dowloaded and compiled the latest C4B 4.1 .
I noticed a new error message during translation :
“Cardinality of abstract set is not allowed as upper bound”
What does that mean ?
Here the part of B code concerned :
PROPERTIES
initial_array : PRODUCT –> NAT1 &
VALUES
initial_array = PRODUCT * {3}
Another think: could it be possible for you to increment the b2c.exe version
this one displays always “V1.0”
Thanks,
Regards
Hello,
I tried to reproduce your error message in my development environment without success.
I wrote this sample code to test your example:
MACHINE
m6
SETS
PRODUCT
CONSTANTS
PRODUCT2,
initial_array,
initial_array2
PROPERTIES
PRODUCT2 = 0..1 &
initial_array : PRODUCT –> NAT1 &
initial_array2: PRODUCT2 –> NAT1
END
IMPLEMENTATION
m6_i
REFINES
m6
VALUES
PRODUCT = 0..3 ;
PRODUCT2 = 0..1 ;
initial_array = PRODUCT * {3} ;
initial_array2= PRODUCT2 * {0}
END
I declare the domain of the array constant as a SET or CONSTANT and
I don’t get error messages.
Can you provide your complete example and the command line used to translate it?
You can contact us at maintenance.atelierb@clearsy.com
Regards
Hello,
I tried to generate the C code of your example inside Atelier B V4.0.1.
I got the following errors :
Unsupported operator type Ligne 7, Colonne14
Unsupported operator type Ligne 7, Colonne14
(ComenC2) C translator error in Mach4_i
Anyway the C code files are well generated !
This example cannot be proved :
initial_array2= PRODUCT2 * {0}
should be replaced by
initial_array2= PRODUCT2 * {1}
as we defined
initial_array2: PRODUCT2 –> NAT1 /* and not as ->NAT */
But this mistake has noting to do with de code geration errors.
Regards