-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Initial commit 1.0.0
- Loading branch information
0 parents
commit 865109c
Showing
5 changed files
with
360 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
# Prerequisites | ||
*.d | ||
|
||
# Object files | ||
*.o | ||
*.ko | ||
*.obj | ||
*.elf | ||
|
||
# Linker output | ||
*.ilk | ||
*.map | ||
*.exp | ||
|
||
# Precompiled Headers | ||
*.gch | ||
*.pch | ||
|
||
# Libraries | ||
*.lib | ||
*.a | ||
*.la | ||
*.lo | ||
|
||
# Shared objects (inc. Windows DLLs) | ||
*.dll | ||
*.so | ||
*.so.* | ||
*.dylib | ||
|
||
# Executables | ||
*.exe | ||
*.out | ||
*.app | ||
*.i*86 | ||
*.x86_64 | ||
*.hex | ||
|
||
# Debug files | ||
*.dSYM/ | ||
*.su | ||
*.idb | ||
*.pdb | ||
|
||
# Kernel Module Compile Results | ||
*.mod* | ||
*.cmd | ||
.tmp_versions/ | ||
modules.order | ||
Module.symvers | ||
Mkfile.old | ||
dkms.conf |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
MIT License | ||
|
||
Copyright (c) 2023 Quantum Leaps | ||
|
||
Permission is hereby granted, free of charge, to any person obtaining a copy | ||
of this software and associated documentation files (the "Software"), to deal | ||
in the Software without restriction, including without limitation the rights | ||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell | ||
copies of the Software, and to permit persons to whom the Software is | ||
furnished to do so, subject to the following conditions: | ||
|
||
The above copyright notice and this permission notice shall be included in all | ||
copies or substantial portions of the Software. | ||
|
||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR | ||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, | ||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE | ||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER | ||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, | ||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE | ||
SOFTWARE. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,80 @@ | ||
## Brought to you by: | ||
[![Quantum Leaps](https://www.state-machine.com/attachments/logo_ql_400.png)](https://www.state-machine.com) | ||
<hr> | ||
|
||
[![GitHub release (latest by date)](https://img.shields.io/github/v/release/QuantumLeaps/DBC-for-embedded-C)](https://github.com/QuantumLeaps/DBC-for-embedded-C/releases/latest) | ||
[![GitHub](https://img.shields.io/github/license/QuantumLeaps/DBC-for-embedded-C)](https://github.com/QuantumLeaps/DBC-for-embedded-C/blob/master/LICENSE) | ||
|
||
# Design By Contract (DBC) | ||
Design By Contract (DBC), pioneered by Bertrand Meyer, views a software system | ||
as a set of components whose collaboration is based on precisely defined | ||
specifications of mutual obligations—the contracts.1 The central idea of this | ||
method is to inherently embed the contracts in the code and validate them | ||
automatically at run time. Doing so consistently has two major benefits: | ||
|
||
1. It automatically helps detect bugs (as opposed to "handling" them), and | ||
2. It is one of the best ways to document code. | ||
|
||
# DBC for Embedded C and C++ | ||
You can implement the most important aspects of DBC (the contracts) in C or | ||
C++ with **assertions**. The Standard C Library macro `assert()` is rarely | ||
applicable to embedded systems, however, because its default behavior (when | ||
the integer expression passed to the macro evaluates to `false`) is to print | ||
an error message and exit. Neither of these actions makes much sense for most | ||
embedded systems, which rarely have a screen to print to and cannot really | ||
exit either (at least not in the same sense that a desktop application can). | ||
Therefore, in an embedded environment, you usually have to define your own | ||
assertions that suit your tools and allow you to customize the error response. | ||
However, you should think twice before you go about "enhancing" assertions | ||
because a large part of their power derives from their relative *simplicity*. | ||
|
||
# This DBC implementation | ||
The DBC implementation in this repository consists of just one header file | ||
[dbc_assert.h](./dbc_assert.h), which has been specifically tailored | ||
for embedded systems and has the following properties: | ||
|
||
- allows customizing the error response (by implementing the DBC | ||
fault handler `DBC_fault_handler()`); | ||
|
||
- conserves memory by avoiding proliferation of multiple copies | ||
of the filename string (macro `DBC_MODULE_NAME()`); | ||
|
||
- provides additional macros for checking and documenting preconditions | ||
(`DBC_REQUIRE()`), postconditions (`DBC_ENSURE()`), and invariants | ||
(`DBC_INVARIANT()`). | ||
|
||
> **NOTE**<br> | ||
The names of the three last macros are a direct loan from Eiffel, | ||
the programming language that natively supports DBC. | ||
|
||
|
||
# Example of Use | ||
``` | ||
#include "dbc_assert.h" /* Design By Contract (DBC) assertions */ | ||
DBC_MODULE_NAME("sst") /* for DBC assertions in this module */ | ||
/*..........................................................................*/ | ||
void SST_Task_post(SST_Task * const me, SST_Evt const * const e) { | ||
/*! @pre the queue must be sized adequately and cannot overflow */ | ||
DBC_REQUIRE(300, me->nUsed <= me->end); | ||
... | ||
} | ||
``` | ||
|
||
## More DBC Resources | ||
To learn more about DBC for embedded systems, please check out the following | ||
resources: | ||
|
||
[1] [Key Concept: Design by Contract](https://www.state-machine.com/dbc)<br> | ||
[2] ["Design by Contract for Embedded C"](https://barrgroup.com/embedded-systems/how-to/design-by-contract-for-embedded-software)<br> | ||
[3] ["A Nail for a Fuse"](https://www.state-machine.com/a-nail-for-a-fuse)<br> | ||
[4] ["An Exception or a Bug"](https://www.state-machine.com/doc/Samek0308.pdf) | ||
|
||
|
||
# How to Help this Project? | ||
Please feel free to clone, fork, and make pull requests to improve DBC | ||
for Embedded C. If you like this project, please give it a star (in the | ||
upper-right corner of your browser window): | ||
|
||
<p align="center"><img src="img/github-star.jpg"/></p> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,207 @@ | ||
/*============================================================================ | ||
* Design By Contract (DBC) for embedded C and C++ | ||
* GitHub: https://github.com/QuantumLeaps/DBC-for-embedded-C | ||
* | ||
* Q u a n t u m L e a P s | ||
* ------------------------ | ||
* Modern Embedded Software | ||
* | ||
* Copyright (C) 2005 Quantum Leaps, <state-machine.com>. | ||
* | ||
* SPDX-License-Identifier: MIT | ||
* | ||
* Permission is hereby granted, free of charge, to any person obtaining a | ||
* copy of this software and associated documentation files (the "Software"), | ||
* to deal in the Software without restriction, including without limitation | ||
* the rights to use, copy, modify, merge, publish, distribute, sublicense, | ||
* and/or sell copies of the Software, and to permit persons to whom the | ||
* Software is furnished to do so, subject to the following conditions: | ||
* | ||
* The above copyright notice and this permission notice shall be included in | ||
* all copies or substantial portions of the Software. | ||
* | ||
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR | ||
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, | ||
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL | ||
* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER | ||
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING | ||
* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER | ||
* DEALINGS IN THE SOFTWARE. | ||
============================================================================*/ | ||
#ifndef DBC_ASSERT_H_ | ||
#define DBC_ASSERT_H_ | ||
|
||
/*! @file | ||
* @brief Memory-efficient Design by Contract (DBC) for embedded C and C++. | ||
* | ||
* @note | ||
* The runtime checking of the DBC assertions can be disabled by defining | ||
* the macro #DBC_DISABLE. However, it is generally **not** advisable to | ||
* disable assertions, *especially* in the production code. Instead, the | ||
* assertion fault handler DBC_fault_handler() should be very carefully | ||
* designed and tested under all fault conditions. | ||
*/ | ||
|
||
/* Active DbC macros -------------------------------------------------------*/ | ||
#ifndef DBC_DISABLE | ||
|
||
/*! Define the user-specified module name for assertions in this file. | ||
* | ||
* @details | ||
* Macro to be placed at the top of each C/C++ module to define the | ||
* single instance of the module name string to be used in reporting | ||
* assertions in this module. This macro takes the user-supplied parameter | ||
* `name_`. | ||
* | ||
* @param[in] name_ string constant representing the module name | ||
* | ||
* @note | ||
* This macro should **not** be terminated by a semicolon. | ||
*/ | ||
#define DBC_MODULE_NAME(name_) \ | ||
static char const DBC_module_name_[] = name_; | ||
|
||
/*! General purpose assertion with user-specified ID number. | ||
* | ||
* @details | ||
* Makes sure the `expr_` parameter is TRUE. Calls the DBC_fault_handler() | ||
* callback if the `expr_` evaluates to FALSE. This assertion takes the | ||
* user-supplied parameter `label_` to identify the location of this | ||
* assertion within the module. This avoids the volatility of using line | ||
* numbers, which change whenever a line of code is added or removed | ||
* upstream from the assertion. | ||
* | ||
* @param[in] label_ numeric label of the assertion (unique within the module) | ||
* @param[in] expr_ Boolean expression to check | ||
* | ||
* @note | ||
* The `expr_` expression is **not** evaluated if assertions are | ||
* disabled with the ::DBC_DISABLE switch. | ||
*/ | ||
#define DBC_ASSERT(label_, expr_) ((expr_) \ | ||
? ((void)0) : DBC_fault_handler(&DBC_module_name_[0], (label_))) | ||
|
||
/*! General purpose assertion with user-specified ID number that | ||
* evaluates the `expr_` expression even when assertions are disabled. | ||
* | ||
* @details | ||
* Like the DBC_ASSERT() macro, except it **always** evaluates the | ||
* `expr_` expression even when DBC assertions are disabled with the | ||
* #DBC_DISABLE macro. | ||
* | ||
* @param[in] label_ numeric label of the assertion (unique within the module) | ||
* @param[in] expr_ Boolean expression to check | ||
*/ | ||
#define DBC_ALLEGE(label_, expr_) DBC_ASSERT(label_, expr_) | ||
|
||
/*! Assertion for a wrong path through the code | ||
* | ||
* @details | ||
* Calls the DBC_fault_handler() callback if ever executed. This assertion | ||
* takes the user-supplied parameter `id_` to identify the location of | ||
* this assertion within the file. This avoids the volatility of using | ||
* line numbers, which change whenever a line of code is added or removed | ||
* upstream from the assertion. | ||
* | ||
* @param[in] label_ numeric label of the assertion (unique within the module) | ||
*/ | ||
#define DBC_ERROR(label_) DBC_fault_handler(&DBC_module_name_[0], (label_)) | ||
|
||
/*! Assertion for checking preconditions. | ||
* | ||
* @details | ||
* Equivalent to DBC_ASSERT(), except the name provides a better | ||
* documentation of the intention of this assertion. | ||
* | ||
* @param[in] label_ numeric label of the assertion (unique within the module) | ||
* @param[in] expr_ Boolean expression to check | ||
* | ||
* @note | ||
* The `expr_` expression is **not** evaluated if assertions are | ||
* disabled with the ::DBC_DISABLE switch. | ||
*/ | ||
#define DBC_REQUIRE(label_, expr_) DBC_ASSERT((label_), (expr_)) | ||
|
||
/*! Assertion for checking postconditions. | ||
* | ||
* @details | ||
* Equivalent to DBC_ASSERT(), except the name provides a better | ||
* documentation of the intention of this assertion. | ||
* | ||
* @param[in] label_ numeric label of the assertion (unique within the module) | ||
* @param[in] expr_ Boolean expression to check | ||
* | ||
* @note | ||
* The `expr_` expression is **not** evaluated if assertions are | ||
* disabled with the ::DBC_DISABLE switch. | ||
*/ | ||
#define DBC_ENSURE(label_, expr_) DBC_ASSERT((label_), (expr_)) | ||
|
||
/*! Assertion for checking invariants. | ||
* | ||
* @details | ||
* Equivalent to DBC_ASSERT(), except the name provides a better | ||
* documentation of the intention of this assertion. | ||
* | ||
* @param[in] label_ numeric label of the assertion (unique within the module) | ||
* @param[in] expr_ Boolean expression to check | ||
* | ||
* @note | ||
* The `expr_` expression is **not** evaluated if assertions are | ||
* disabled with the ::DBC_DISABLE switch. | ||
*/ | ||
#define DBC_INVARIANT(label_, expr_) DBC_ASSERT((label_), (expr_)) | ||
|
||
#ifndef DBC_NORETURN | ||
#define DBC_NORETURN | ||
#endif | ||
|
||
#ifdef __cplusplus | ||
extern "C" { | ||
#endif | ||
|
||
/*! DBC assertion fault handler. | ||
* | ||
* @details | ||
* This is an application-specific callback function needs to be defined in | ||
* the application to perform the clean system shutdown and perhaps a reset. | ||
* The DBC_fault_handler() function is the last line of defense after the | ||
* system failure and its implementation should be very **carefully** | ||
* designed and **tested** under various fault conditions, including but | ||
* not limited to: stack overflow, stack corruption, or calling | ||
* DBC_fault_handler() from ISRs. | ||
* @param[in] module name of the file/module in which the assertion failed | ||
* (constant, zero-terminated C string) | ||
* @param[in] label unique label of the assertion within the module. | ||
* This could be a line number or a user-defined label. | ||
* | ||
* @returns | ||
* This callback function should **not return** (see #NORETURN), | ||
* as continuation after an assertion failure does not make sense. | ||
* | ||
* @note | ||
* It is typically a **bad idea** to implement DBC_fault_handler() as an | ||
* endless loop that ties up the CPU. During debugging, DBC_fault_handler() | ||
* is an ideal place to put a breakpoint. | ||
*/ | ||
DBC_NORETURN void DBC_fault_handler(char const * module, int label); | ||
|
||
#ifdef __cplusplus | ||
} | ||
#endif | ||
|
||
/* Inactive DbC macros -----------------------------------------------------*/ | ||
#else | ||
|
||
#define DBC_MODULE_NAME(dummy_) | ||
#define DBC_ASSERT(label_, expr_) ((void)0) | ||
#define DBC_ERROR(label_) ((void)0) | ||
#define DBC_REQUIRE(label_, expr_) ((void)0) | ||
#define DBC_ENSURE(label_, expr_) ((void)0) | ||
#define DBC_INVARIANT(label_, expr_) ((void)0) | ||
#define DBC_ALLEGE(label_, expr_) ((void)(expr_)) | ||
|
||
#endif /* Inactive DBC macros */ | ||
|
||
#endif /* DBC_ASSERT_ */ |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.