Highly enhanced EwoK version, in full Ada, including more SPARK, cleaner and faster code

(HEAD -> master, tag: v0.9.9, m/master, github/master) [update] add production defconfig autotest to travis
[bugfix] support for clean reboot/wipe on panic. Allows task fault on userspace exception
[bugfix] add missing unmap flag set. typo for harden (not freezing) modes
[enhancement] More proofs
[enhancement] Proving some parts of the kernel with gnatprove
Removed file added by mistake
[enhancement] using a generic memory interface - Replacing ewok.mpu invocations by the more generic ewok.memory package
[enhancement] Inlining some subprograms for slightly improving performances
Removing get_current procedure
Completed fault handler with extra informations
Removing ewok.sched.get_current procedure (not useful)
SoftIRQ: simplifying isr_queue entries
[enhancement] More portable code
[bugfix] Protecting some critical resources
Adding SCB register
Indenting
[bugfix] add missing RCC activation for kernel serial
(pthierry/master) [bugfix] comment typo
[bugfix] corrected device addr check for pure IO devices
[update] support for configurable reentrancy support (kernel experimental mode)
[enhancement] add support for rentrancy in EwoK handler mode
[bugfix] updated travis cross-refs check
[performance] MPU update only when it's needed * MPU update is performed only when: - a task switch occurs - task's mode is changing
[design] Removing syscall management from SoftIRQ * Every syscalls are managed synchronously * SoftIRQ is simplified and manage only ISRs
[enhancement] Removing privileges from the SoftIRQ kernel task * MPU imposes some new constraints that forbid access to user tasks' memory space
[bugfix] add missing export
[enhancement] initial implementation of cross-project PR dependencies markup
[bugfix] corrected device size check for pure IO devices (e.g. LED or buttons)
[bugfix] deactivate USART RX for kernel console
[enhancement] MPU layer is abstracted - Kernel modules (tasks, sched...) do not need to "understand" how the MPU work anymore. The invocated methods are more simple. - The benefit is that it lead to a better decoupling packages and to an increase simplification - The major drawback is currently a performance penalty (about 3%). The explanation is that previous implementation use lot of hardcoded value.
Removed doxygen tags
Do some cleaning - Reformating some comments - Reformating some 'with' clauses - Lightening ewok.sleep package
[bugfix] Resolved Ada circular elaboration problems - 2019 GNAT compiler was ok but 2018 version didn't managed correctly dependencies - Root cause was that ewok.ads top package had a related body
Adding default values to records * Cleaning task and device initialization * Adding some default values to avoid unitilized values that lead to undefined behaviors
[enhancement] Misc. * Cleaning tools (removing unused variables) * Fixing some missing preprocessing directives: FISR and FIPC
[enhancement] cleaning build process, reducing makefiles to single one, using gprbuild instead
[enhancement] Removed the last remaing C file and cleaning startup.s
[enhancement] Cleaning * Removed unused files * Simplifications
[enhancement] Moved Ada entry point from ewok.init.main to ewok.main
[enhancement] Cleaning MPU management
[update] Removed useless code * RNG interface for C code is not used anymore * Directives KERNEL_ENABLE_DMA are removed where not usefull * Added KERNEL_ENABLE_DMA directives in src/ewok-syscalls-handler.adb to return DENIED when doing a related DMA syscall when it's not available
[enhancement] Cleaner serial management by the kernel for debugging purpose
[enhancement] Cleaner serial management by the kernel for debugging purpose
[bugfix] Remove unicode character unsupported by latex
[bugfix] Remove unicode character unsupported by latex
[update] EwoK description
[update] Cleaning, fixing minor things...
[bugfix] Removed useless file.
[bugfix] Minor. Fixed mkdir directive.
[enhancement] Removed unused code and added some few comments
Merge pull request #15 from PThierry/only_ada
[bugfix] add placeholder for generated root dir
[bugfix] add missing files during directory move
(pthierry/only_ada) [bugfix] create dir if it does not exists before generating header
[bugfix] add missing config.def links
add placeolder for generated dir
[update] removed Ada subdir of SoC and core dirs, as Ada is the single kernel language
moved src/Ada to src
Merge pull request #16 from arnauldm/master
[bugfix] Fixed some few errors in libgnat GPR build file * -O2 must be in Compiler package * Removed some redundant directives
[update] Removed unused files
Merge pull request #14 from arnauldm/ami/cleaning
[bugfix] Minor update in Makefile
[enhancement] Removed unused code * Stack protection (SSP) is no more useful for hardening the kernel, as its fully implemented in Ada * FPU is not used
(types, portable_types) Merge pull request #13 from PThierry/exit_handling
(pthierry/exit_handling, exit_handling) [update] add sys_exit initial documentation
[update] move exit handling to dedicated syscall
[bugfix] Updated broken URL in README.md
[bugfix] Fixed markdown formatting
[updated] Documentation
Merge pull request #12 from arnauldm/ami/master
[enhancement] Removed useless code
Merge pull request #11 from arnauldm/ami/c_to_ada
[bugfix] Updated soc-rcc.adb for disco407 board
[enhancement] soc-rng in Ada
[enhancement] SOC initialization in Ada
Merge pull request #10 from arnauldm/ami/adaification
[enhancement] Migrated C code to Ada * last_chance_handle in Ada * init.c do nothing more than calling ewok.init.main procedure * debug.c and debug.h are removed * removed some unused files
Merge pull request #9 from arnauldm/ami/sparkification
Merge pull request #7 from PThierry/prove_spark2019
[enhancement] Code simplification
[update] removing useless local access type after rebasing master
[update] add clean prove target inside kernel dir
[update] replacing global access type in tasks interface with local types
[bugfix] keeping t_task_access as rw pointer by now. the task accessor should be updated later on to support SPARK proof
[update] passing local task's IPC endpoint list from pointer array to id array
[enhancement] starting SPARK'19 integration, with pointers support
Merge pull request #8 from arnauldm/ami/usart
(refs/pull/8/head) [bugfix] Minor fixes for stm32f407 architecture
[bugfix] Missing symbolic links for stm32f407 and stm32f429 architectures
[bugfix] Updated Makefile.objs
[update] Replaced usart and debugging C code with Ada code * Added support to RCC with soc.rcc and soc.rcc.default Ada packages * Added (incomplete but functionnal) support to USART with soc.usart Ada package * Put debugging serial initialization in ewok.debug Ada package
Merge pull request #6 from PThierry/prove
(pthierry/prove) [bugfix] add missing new dir to prove target GPR file
Merge pull request #5 from arnauldm/ami/c_to_ada
[bugfix] BSP files adapted for stm32f407 board * Created stm32f407/Ada/generated * Adapted stm32f407/Ada/soc-rcc.adb to fulfill soc devices constraints
Merge pull request #4 from arnauldm/ami/syscalls
(refs/pull/5/head) [update] Replaced devmap C code with Ada code
[update] Big update in order to get rid of C code * Replaced devmap C code with Ada code /!\ Not working /!
(refs/pull/4/head) [update] Cleaning syscalls * Replacing SVC_TASK_DONE and SVC_ISR_DONE by SVC_EXIT * Renaming some syscalls so their name is more self-explanatory
[bugfix] Added missing checks in syscalls SVC_TASK_DONE and SVC_ISR_DONE
[update] SVC handler simplified
[update] Modified syscalls mechanism
Merge pull request #3 from PThierry/kernel_full_ada
(pthierry/kernel_full_ada) [enhancement] passing to full Ada kernel; removing the unused C code from the Ada version of EwoK

EwoK security enhancement and CI integration

This release is a patchset relase, including the following:

• EwoK MPU handling update for Ada code, updating the way the MPU permissions is configured for supervisor mode. The kernel memory access is now controlled by the MPU with restrictive constraints:
  • Only the currently executed task data can be acceded by the kernel
  • The kernel has no access to unmapped regions (including, for e.g. flash memory control registers)
  • The bootrom is never mapped and can't be accessed
• EwoK master branch commits and pull-requests are automatically checked by the travis CI
  • disco407 and wookey profiles are built
  • kernel doc is built

Warning: the EwoK kernel C implementation is no more updated, as it will shortly be removed from the EwoK sources. The C implementation will be forked in a separated repository as an example

EwoK 0.9.5 release note

EwoK full public version initial release

This is the first complete public release of the EwoK kernel. This release includes:

1. A complete C implementation of the EwoK kernel, including support for STM32F407, STM32F4029 and STM32F439 kernel
2. A nearly complete Ada implementation of the EwoK kernel, with a higly reduced part of residual C content (mostly USART console handling)
3. A complete kernel API, internals and principles documentation
4. Various proven components, based on SPARK (MPU, permissions handling...)

The C kernel implementation is provided as an example and potential helper. The effective secured and proven kernel implementation is the Ada-based one. The C kernel will not be maintained for a long time. Although, both implementations are API-compatible.

EwoK 0.9.4 release note

EwoK pre-release

This is the first public elease of the EwoK micro-kernel.
This release is a pre-version of the kernel and is not production-compatible.

This version is a preview of what will be released in the future official public releases