C4B

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

 

 

 

7 réponses à C4B

  1. laurentg dit :

    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.

  2. Hector Ruiz Barradas dit :

    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

  3. laurentg dit :

    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)
    {
        
        ;
    }
  4. Hector Ruiz Barradas dit :

    Thank you for your feedback.

    I will add this issue to my list of improvements of c4b.

  5. laurentg dit :

    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

    • Hector Ruiz Barradas dit :

      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

      • laurentg dit :

        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

Les commentaires sont fermés.