Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
d61c3464
Commit
d61c3464
authored
9 years ago
by
Kostyantyn Vorobyov
Browse files
Options
Downloads
Patches
Plain Diff
[RTL] Doxygen-style comments for e_acsl_assert.h
parent
470eb7d8
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
+22
-14
22 additions, 14 deletions
src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
with
22 additions
and
14 deletions
src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
+
22
−
14
View file @
d61c3464
...
@@ -20,27 +20,34 @@
...
@@ -20,27 +20,34 @@
/* */
/* */
/**************************************************************************/
/**************************************************************************/
/*! ***********************************************************************
* \file e_acsl_assert.h
* \brief E-ACSL assertions and abort statements.
***************************************************************************/
#ifndef E_ACSL_ASSERT
#ifndef E_ACSL_ASSERT
#define E_ACSL_ASSERT
#define E_ACSL_ASSERT
#include
"e_acsl_string.h"
#include
"e_acsl_string.h"
#include
"e_acsl_printf.h"
#include
"e_acsl_printf.h"
/* Drop-in replacement for abort function */
/*
! \brief
Drop-in replacement for abort function */
#define abort() exec_abort(__LINE__, __FILE__)
#define abort() exec_abort(__LINE__, __FILE__)
/* Output a message to error stream using printf-like format string and abort
/*! \brief Output a message to error stream using printf-like format string
* the execution. This is a wrapper for eprintf combined with abort */
* and abort the execution.
*
* This is a wrapper for \p eprintf combined with \p abort */
static
void
vabort
(
char
*
fmt
,
...);
static
void
vabort
(
char
*
fmt
,
...);
/* Drop-in replacement for system-wide assert macro */
/*
! \brief
Drop-in replacement for system-wide assert macro */
#define assert(expr) \
#define assert(expr) \
((expr) ? (void)(0) : vabort("%s at %s:%d\n", \
((expr) ? (void)(0) : vabort("%s at %s:%d\n", \
#expr, __FILE__,__LINE__))
#expr, __FILE__,__LINE__))
/* Assert with printf-like error message support */
/*
! \brief
Assert with printf-like error message support */
#define vassert(expr, fmt, ...) \
#define vassert(expr, fmt, ...) \
vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
static
void
exec_abort
(
int
line
,
const
char
*
file
)
{
static
void
exec_abort
(
int
line
,
const
char
*
file
)
{
eprintf
(
"Execution aborted (%s:%d)
\n
"
,
file
,
line
);
eprintf
(
"Execution aborted (%s:%d)
\n
"
,
file
,
line
);
...
@@ -62,7 +69,7 @@ static void vassert_fail(int expr, int line, char *file, char *fmt, ...) {
...
@@ -62,7 +69,7 @@ static void vassert_fail(int expr, int line, char *file, char *fmt, ...) {
}
}
}
}
/* Print a message to stderr and abort the execution */
/*
! \brief
Print a message to stderr and abort the execution */
static
void
vabort
(
char
*
fmt
,
...)
{
static
void
vabort
(
char
*
fmt
,
...)
{
va_list
va
;
va_list
va
;
va_start
(
va
,
fmt
);
va_start
(
va
,
fmt
);
...
@@ -71,7 +78,7 @@ static void vabort(char *fmt, ...) {
...
@@ -71,7 +78,7 @@ static void vabort(char *fmt, ...) {
abort
();
abort
();
}
}
/* Default implementation of E-ACSL runtime assertions */
/*
! \brief
Default implementation of E-ACSL runtime assertions */
static
void
runtime_assert
(
int
predicate
,
char
*
kind
,
static
void
runtime_assert
(
int
predicate
,
char
*
kind
,
char
*
fct
,
char
*
pred_txt
,
int
line
)
{
char
*
fct
,
char
*
pred_txt
,
int
line
)
{
if
(
!
predicate
)
{
if
(
!
predicate
)
{
...
@@ -81,17 +88,18 @@ static void runtime_assert(int predicate, char *kind,
...
@@ -81,17 +88,18 @@ static void runtime_assert(int predicate, char *kind,
}
}
}
}
/* Alias for runtime assertions. Since `__e_acsl_assert` is added as a weak
/*! \brief Alias for runtime assertions.
* alias user-defined implementation of the `__e_acsl_assert` function will be
*
* preferred at link time. */
* Since \p __e_acsl_assert is added as a weak alias user-defined implementation
* of the \p __e_acsl_assert function will be preferred at link time. */
void
__e_acsl_assert
(
int
pred
,
char
*
kind
,
char
*
fct
,
char
*
pred_txt
,
int
line
)
void
__e_acsl_assert
(
int
pred
,
char
*
kind
,
char
*
fct
,
char
*
pred_txt
,
int
line
)
__attribute__
((
weak
,
alias
(
"runtime_assert"
)));
__attribute__
((
weak
,
alias
(
"runtime_assert"
)));
/* Instances of assertions shared accross different memory models */
/* Instances of assertions shared accross different memory models */
/* Abort the execution if the size of the pointer computed during
/*
! \brief
Abort the execution if the size of the pointer computed during
* instrumentation (_ptr_sz) does not match the size of the pointer used
* instrumentation (
\p
_ptr_sz) does not match the size of the pointer used
* by a compiler (void*) */
* by a compiler (
\p
void*) */
#define arch_assert(_ptr_sz) \
#define arch_assert(_ptr_sz) \
vassert(_ptr_sz == sizeof(void*), \
vassert(_ptr_sz == sizeof(void*), \
"Mismatch of instrumentation- and compile-time pointer sizes: " \
"Mismatch of instrumentation- and compile-time pointer sizes: " \
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment