Add preliminary support for vdm

ada/buildsupport.adb

@@ -200,6 +200,9 @@ procedure BuildSupport is
                         when Language_CPP =>
                            Imported_Routines.C_Set_Language_To_CPP;
 
+                        when Language_VDM =>
+                           Imported_Routines.C_Set_Language_To_VDM;
+
                         when Language_SDL_OpenGEODE =>
                            Imported_Routines.C_Set_Language_To_SDL;
 

ada/imported_routines.ads

@@ -150,6 +150,7 @@ package Imported_Routines is
    procedure C_Set_Language_To_QGenAda;
    procedure C_Set_Language_To_QGenC;
    procedure C_Set_Language_To_CPP;
+   procedure C_Set_Language_To_VDM;
    procedure C_Set_Language_To_OpenGEODE;
    procedure C_Set_Language_To_BlackBox_Device;
    procedure C_Set_Language_To_RTDS;
@@ -232,7 +233,8 @@ private
    pragma Import (C, C_Set_Language_To_Other, "Set_Language_To_Other");
    pragma Import (C, C_Set_Language_To_C, "Set_Language_To_C");
    pragma Import (C, C_Set_Language_To_CPP, "Set_Language_To_CPP");
-   pragma Import (C, C_Set_Language_To_OpenGEODE, "Set_Language_To_OpenGEODE");
+   pragma Import (C, C_Set_Language_To_VDM, "Set_Language_To_VDM");
+   pragma Import (C, C_Set_Language_To_OpenGEODE, "Set_Language_To_SDL");
    pragma Import (C, C_Set_Language_To_BlackBox_Device,
      "Set_Language_To_BlackBox_Device");
    pragma Import (C, C_Set_Language_To_RTDS, "Set_Language_To_RTDS");

c/build_vdm_skeletons.c

+/* Buildsupport is (c) 2008-2016 European Space Agency
+ * contact: maxime.perrotin@esa.int
+ * License is LGPL, check LICENSE file */
+/* build_vdm_skeletons.c
+
+   Generate code skeletons for VDM functions
+ */
+
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <sys/stat.h>
+#include <stdbool.h>
+#include <assert.h>
+
+#include "my_types.h"
+#include "practical_functions.h"
+
+static FILE *user_code = NULL, *interface = NULL;
+
+
+/* Adds header to user_code.h and (if new) user_code.c */
+void vdm_gw_preamble(FV * fv)
+{
+    assert (NULL != interface);
+
+    fprintf(interface,
+          "-- This file was generated automatically: DO NOT MODIFY IT ! \n\n");
+
+    fprintf(interface,
+            "class %s_Interface\n"
+            "operations\n"
+            "    public Startup: () ==> ()\n"
+            "    Startup (-) is subclass responsibility\n\n",
+            fv->name);
+
+
+    if (NULL != user_code) {
+        fprintf(user_code,
+              "-- User code: This file will not be overwritten by TASTE.\n\n");
+
+        fprintf(user_code,
+            "class %s\n"
+            "is subclass of %s_Interface\n"
+            "operations\n"
+            "    public Startup: () ==> ()\n"
+            "    -- user: fill your code\n\n",
+            fv->name,
+            fv->name);
+    }
+}
+
+/* Creates interface and if necessary user code template (if it did not exist) */
+void Init_VDM_GW_Backend(FV *fv)
+{
+    char *path = NULL;
+    char *filename = NULL;
+
+    path     = make_string("%s/%s", OUTPUT_PATH, fv->name);
+    filename = make_string("%s_interface.vdmpp", fv->name);
+    create_file(path, filename, &interface);
+    free(filename);
+    filename = make_string("%s_code.vdmpp", fv->name);
+
+    if (!file_exists(path, filename)) {
+        create_file(path, filename, &user_code);
+        free(filename);
+    }
+
+    free(path);
+    vdm_gw_preamble(fv);
+}
+
+
+/* Add a Provided interface. Can contain in and out parameters
+ * Write in user_code.h the declaration of the user functions
+ * and if user_code.c is new, copy these declarations there too.
+ */
+void add_pi_to_vdm_gw(Interface * i)
+{
+    if (NULL == interface)
+        return;
+
+    char *signature = make_string("public PI_%s:",
+                                  i->name);
+
+
+    fprintf(interface, "%s", signature);
+
+    if (NULL != user_code) {
+        fprintf(user_code, "%s", signature);
+    }
+
+    char *sep = " * ";
+    bool comma = false;
+
+    FOREACH (p, Parameter, i->in, {
+        char *sort = make_string("%s%s`%s",
+                                 comma? sep: "",
+                                 p->asn1_module,
+                                 p->type);
+        fprintf(interface, "%s", sort);
+        if(NULL != user_code) {
+            fprintf(user_code, "%s",sort);
+        }
+        free(sort);
+        comma = true;
+    });
+
+    if (NULL != i->out) {
+        char *out = make_string(" ==> %s`%s",
+                                i->out->value->asn1_module,
+                                i->out->value->type);
+        fprintf(interface, "%s", out);
+        if(NULL != user_code) {
+            fprintf(user_code, "%s", out);
+        }
+        free(out);
+    }
+
+    fprintf(interface,
+            "\n"
+            "%s%s == is subclass responsibility\n\n",
+            i->name,
+            NULL != i->in? " (-)" : "");
+
+    if (NULL != user_code)
+        fprintf(user_code,
+                "\n"
+                "%s == -- Write your code here\n\n",
+                i->name);
+
+    free(signature);
+    free(sep);
+}
+
+/* Declaration of the RI */
+void add_ri_to_vdm_gw(Interface * i)
+{
+    if (NULL == interface || NULL == i)
+        return;
+    // TODO
+}
+
+
+void End_VDM_GW_Backend(FV *fv)
+{
+    fprintf(interface, "end %s_Interface\n", fv->name);
+    fprintf(user_code, "end %s\n", fv->name);
+    close_file(&interface);
+    close_file(&user_code);
+}
+
+/* Function to process one interface of the FV */
+void GW_VDM_Interface(Interface * i)
+{
+    switch (i->direction) {
+        case PI:
+            add_pi_to_vdm_gw(i);
+            break;
+
+        case RI:
+            /*
+             * There can be duplicate RI name but one sync, the other async
+             * In that case, discard the async one (generated by VT to allow
+             * a mix of sync and async PI in one block
+             */
+            if (asynch == i->synchronism) {
+                FOREACH(ri, Interface, i->parent_fv->interfaces, {
+                    if (RI == ri->direction &&
+                        !strcmp(ri->name, i->name) &&
+                        synch == ri->synchronism) {
+                        return;
+                    }
+
+                });
+            }
+            // RI not supported yet
+            //add_ri_to_vdm_gw(i);
+            break;
+        default:
+            break;
+    }
+}
+
+/* External interface (the one and unique) */
+void GW_VDM_Backend(FV * fv)
+{
+    if (fv->system_ast->context->onlycv)
+        return;
+    if (vdm == fv->language) {
+        Init_VDM_GW_Backend(fv);
+        FOREACH(i, Interface, fv->interfaces, {
+            GW_VDM_Interface(i);
+        });
+        End_VDM_GW_Backend(fv);
+    }
+}

c/c_ast_construction.c

@@ -162,6 +162,12 @@ void Set_Language_To_CPP()
         fv->language = cpp;
 }
 
+void Set_Language_To_VDM()
+{
+    if (NULL != fv)
+        fv->language = vdm;
+}
+
 void Set_Language_To_OpenGEODE()
 {
     if (NULL != fv)

c/python_ast_backend.c

@@ -22,7 +22,7 @@ void Generate_Python_AST(System *s, char *dest_directory)
 
     fprintf (py,
         "#! /usr/bin/python\n\n"
-        "Ada, C, GUI, SIMULINK, VHDL, OG, RTDS, SYSTEM_C, SCADE6 = range(9)\n"
+        "Ada, C, GUI, SIMULINK, VHDL, OG, RTDS, SYSTEM_C, SCADE6, VDM, CPP = range(11)\n"
         "thread, passive, unknown = range(3)\n"
         "PI, RI = range(2)\n"
         "synch, asynch = range(2)\n"

include/c_ast_construction.h

@@ -62,6 +62,7 @@ void Set_ASync_IF();
 void Set_Sync_IF();
 void Set_Language_To_GUI();
 void Set_Language_To_CPP();
+void Set_Language_To_VDM();
 void Set_Language_To_OpenGEODE();
 void Set_Language_To_BlackBox_Device();
 void Set_Language_To_Ada();

include/my_types.h

@@ -72,6 +72,7 @@ typedef enum {
     vhdl,
     system_c,
     blackbox_device,
+    vdm,
     other
 } Language;
 

include/practical_functions.h

@@ -19,7 +19,7 @@
 /* Return a string representing the selected encoding rules for a Parameter */
 #define BINARY_ENCODING(p) (native==p->encoding)?"NATIVE":(uper==p->encoding)?"UPER":(acn==p->encoding)?"ACN":"#ERROR#"
 
-#define LANGUAGE(fv) ada==fv->language?"Ada": c==fv->language?"C": sdl==fv->language?"OG": rtds==fv->language?"RTDS": scade==fv->language?"SCADE6":simulink==fv->language?"SIMULINK": blackbox_device==fv->language? "C": rhapsody==fv->language? "C": vhdl==fv->language?"VHDL": system_c==fv->language?"SYSTEM_C":gui==fv->language?"GUI": qgenc==fv->language?"QGenC": qgenada==fv->language?"QGenAda": cpp==fv->language?"CPP": "UNSUPPORTED_LANGUAGE!"
+#define LANGUAGE(fv) ada==fv->language?"Ada": c==fv->language?"C": sdl==fv->language?"OG": rtds==fv->language?"RTDS": scade==fv->language?"SCADE6":simulink==fv->language?"SIMULINK": blackbox_device==fv->language? "C": rhapsody==fv->language? "C": vhdl==fv->language?"VHDL": system_c==fv->language?"SYSTEM_C":gui==fv->language?"GUI": qgenc==fv->language?"QGenC": qgenada==fv->language?"QGenAda": cpp==fv->language?"CPP": vdm==fv->language?"VDM": "UNSUPPORTED_LANGUAGE!"
 
 #define RCM_KIND(IF) (protected==IF->rcm?"protected":unprotected==IF->rcm?"unprotected":sporadic==IF->rcm?"sporadic":cyclic==IF->rcm?"cyclic":variator==IF->rcm?"variator":"unknown")