Ada code architecture

General architecture

EwoK Ada sources are hosted in the following directories:

  • kernel/Ada for the kernel, arch-independent Ada code
  • kernel/Ada/generated hosts the generated Ada files, like kernel/generated hosts the generated C files
  • arch-specific Ada content (BSP) is hosted in the Ada subdirectory of each SoC and core source directory

Ada has a hierarchical scoping principle, based on packages. In the case of EwoK, various packages and subpackages are used.

  • kernel pacakges belong to the ewok package
  • SoC-related packages belong to the soc package
  • Core-related packages belong to the core-relative package (e.g. m4 for Cortex-M4)

As the EwoK kernel is an hybrid C/Ada/SPARK kernel, some packages require an external interface with the C code. For a given package ̀`foo` interacting with external C code, a foo_interface package must exist.

In the same way, as some various C types (structures, union, enumerates, etc.) have to be used in the interfaces packages, the following C-specific packages exist, containing only specifications:

  • c package containing all C types and API that are arch-independent
  • c_soc package, containing all C types and API that are SoC-specific

Ada and Tataouine configuration

Ada versus preprocessing

Ada does support preprocessing and the configuration options sometime use the preprocessing principle to enable or not some specific functions. The preprocessing usage is quite similar to C:

#if CONFIG_KERNEL_DOMAIN
   function is_same_domain
     (from    : in t_real_task_id;
      to      : in t_real_task_id)
   return boolean
   with
      Global    => null,
      Post      => (if (from = to) then is_same_domain'Result = false);
#end if;

Integration of autogenerated files

Generated files are not created by the microkernel internal tools, but by the SDK. The reason is that the generated files contain information about the applications list, associated permissions and layout. All these information are stored by the SDK configuration mechanism, not by the kernel itself.

The scripts generating these files (and the C equivalent) are hosted in the tools/ directory of the SDK:

  • tools/gen_ld: generates the global layout and the application layout header
  • tools/gen_symhdr.pl: generates the applications section mapping. Used to map .data and zeroify .bss of each application at boot time
  • tools/apps/permissions.pl: generates the application permissions header