Skip to content
Snippets Groups Projects
Commit 6d3a2081 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Extract value content printing in utility function

parent 20eec67d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
+ 109
− 118
View file @ 6d3a2081
...@@ -45,6 +45,105 @@ void eacsl_print_values(eacsl_assert_data_t *data) { ...@@ -45,6 +45,105 @@ void eacsl_print_values(eacsl_assert_data_t *data) {
} }
} }
/*! Print the given integer to `stream` */
void eacsl_print_int_content(FILE *stream,
eacsl_assert_data_int_content_t *int_content) {
if (int_content->is_enum) {
fprintf(stream, "<enum> ");
}
switch (int_content->kind) {
case E_ACSL_IBOOL:
fprintf(stream, "%d", int_content->value.value_bool);
break;
case E_ACSL_ICHAR:
fprintf(stream, "%d", int_content->value.value_char);
break;
case E_ACSL_ISCHAR:
fprintf(stream, "%hhd", int_content->value.value_schar);
break;
case E_ACSL_IUCHAR:
fprintf(stream, "%hhu", int_content->value.value_uchar);
break;
case E_ACSL_IINT:
fprintf(stream, "%d", int_content->value.value_int);
break;
case E_ACSL_IUINT:
fprintf(stream, "%u", int_content->value.value_uint);
break;
case E_ACSL_ISHORT:
fprintf(stream, "%hd", int_content->value.value_short);
break;
case E_ACSL_IUSHORT:
fprintf(stream, "%hu", int_content->value.value_ushort);
break;
case E_ACSL_ILONG:
fprintf(stream, "%ld", int_content->value.value_long);
break;
case E_ACSL_IULONG:
fprintf(stream, "%lu", int_content->value.value_ulong);
break;
case E_ACSL_ILONGLONG:
fprintf(stream, "%lld", int_content->value.value_llong);
break;
case E_ACSL_IULONGLONG:
fprintf(stream, "%llu", int_content->value.value_ullong);
break;
case E_ACSL_IMPZ:
__gmp_fprintf(stream, "%Zd", int_content->value.value_mpz);
break;
}
}
/*! Print the given real to `stream`. */
void eacsl_print_real_content(FILE *stream,
eacsl_assert_data_real_content_t *real_content) {
switch (real_content->kind) {
case E_ACSL_RFLOAT:
fprintf(stream, "%e", real_content->value.value_float);
break;
case E_ACSL_RDOUBLE:
fprintf(stream, "%le", real_content->value.value_double);
break;
case E_ACSL_RLONGDOUBLE:
fprintf(stream, "%Le", real_content->value.value_ldouble);
break;
case E_ACSL_RMPQ:
__gmp_fprintf(stream, "%Qd", real_content->value.value_mpq);
break;
}
}
void eacsl_print_value_content(FILE *stream, eacsl_assert_data_value_t *value) {
switch (value->type) {
case E_ACSL_INT:
eacsl_print_int_content(stream, &value->content.int_content);
break;
case E_ACSL_REAL:
eacsl_print_real_content(stream, &value->content.real_content);
break;
case E_ACSL_PTR:
fprintf(stream, "%p", value->content.value_ptr);
break;
case E_ACSL_ARRAY:
fprintf(stream, "<array>, address: %p", value->content.value_array);
break;
case E_ACSL_FUN:
fprintf(stream, "<function>");
break;
case E_ACSL_STRUCT:
fprintf(stream, "<struct>");
break;
case E_ACSL_UNION:
fprintf(stream, "<union>");
break;
case E_ACSL_OTHER:
fprintf(stream, "<other>");
break;
default:
fprintf(stream, "<unknown>");
}
}
#ifndef E_ACSL_EXTERNAL_ASSERT #ifndef E_ACSL_EXTERNAL_ASSERT
/*! \brief Return `str` id `cond` is true, an empty string otherwise. */ /*! \brief Return `str` id `cond` is true, an empty string otherwise. */
...@@ -117,125 +216,17 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) { ...@@ -117,125 +216,17 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
#endif #endif
#ifndef E_ACSL_EXTERNAL_PRINT_VALUE #ifndef E_ACSL_EXTERNAL_PRINT_VALUE
void eacsl_print_int_content(const char *name,
eacsl_assert_data_int_content_t *int_content) {
switch (int_content->kind) {
case E_ACSL_IBOOL:
fprintf(stderr, "\t- %s: %s%d\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_bool);
break;
case E_ACSL_ICHAR:
fprintf(stderr, "\t- %s: %s%d\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_char);
break;
case E_ACSL_ISCHAR:
fprintf(stderr, "\t- %s: %s%hhd\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_schar);
break;
case E_ACSL_IUCHAR:
fprintf(stderr, "\t- %s: %s%hhu\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_uchar);
break;
case E_ACSL_IINT:
fprintf(stderr, "\t- %s: %s%d\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_int);
break;
case E_ACSL_IUINT:
fprintf(stderr, "\t- %s: %s%u\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_uint);
break;
case E_ACSL_ISHORT:
fprintf(stderr, "\t- %s: %s%hd\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_short);
break;
case E_ACSL_IUSHORT:
fprintf(stderr, "\t- %s: %s%hu\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_ushort);
break;
case E_ACSL_ILONG:
fprintf(stderr, "\t- %s: %s%ld\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_long);
break;
case E_ACSL_IULONG:
fprintf(stderr, "\t- %s: %s%lu\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_ulong);
break;
case E_ACSL_ILONGLONG:
fprintf(stderr, "\t- %s: %s%lld\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_llong);
break;
case E_ACSL_IULONGLONG:
fprintf(stderr, "\t- %s: %s%llu\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_ullong);
break;
case E_ACSL_IMPZ:
__gmp_fprintf(stderr, "\t- %s: %s%Zd\n", name,
int_content->is_enum ? "<enum> " : "",
int_content->value.value_mpz);
break;
}
}
void eacsl_print_real_content(const char *name,
eacsl_assert_data_real_content_t *real_content) {
switch (real_content->kind) {
case E_ACSL_RFLOAT:
fprintf(stderr, "\t- %s: %e\n", name, real_content->value.value_float);
break;
case E_ACSL_RDOUBLE:
fprintf(stderr, "\t- %s: %le\n", name, real_content->value.value_double);
break;
case E_ACSL_RLONGDOUBLE:
fprintf(stderr, "\t- %s: %Le\n", name, real_content->value.value_ldouble);
break;
case E_ACSL_RMPQ:
__gmp_fprintf(stderr, "\t- %s: %Qd\n", name, real_content->value.value_mpq);
break;
}
}
void eacsl_print_value(eacsl_assert_data_value_t *value) { void eacsl_print_value(eacsl_assert_data_value_t *value) {
switch (value->type) { fprintf(stderr, "\t- %s: ", value->name);
case E_ACSL_INT: if (value->type == E_ACSL_ARRAY) {
eacsl_print_int_content(value->name, &value->content.int_content); // The function `eacsl_print_value_content()` prints the content of an array
break; // on one line to be more generic towards alternative implementation.
case E_ACSL_REAL: // For the default implementation we can override it to print something more
eacsl_print_real_content(value->name, &value->content.real_content); // consistent with the way the name of the value is printed.
break; fprintf(stderr, "<array>\n\t\t- address: %p", value->content.value_array);
case E_ACSL_PTR: } else {
fprintf(stderr, "\t- %s: %p\n", value->name, value->content.value_ptr); eacsl_print_value_content(stderr, value);
break;
case E_ACSL_ARRAY:
fprintf(stderr, "\t- %s: <array>\n\t\t- address: %p\n", value->name,
value->content.value_array);
break;
case E_ACSL_FUN:
fprintf(stderr, "\t- %s: <function>\n", value->name);
break;
case E_ACSL_STRUCT:
fprintf(stderr, "\t- %s: <struct>\n", value->name);
break;
case E_ACSL_UNION:
fprintf(stderr, "\t- %s: <union>\n", value->name);
break;
case E_ACSL_OTHER:
fprintf(stderr, "\t- %s: <other>\n", value->name);
break;
default:
fprintf(stderr, "\t- %s: <unknown>\n", value->name);
break;
} }
fprintf(stderr, "\n");
} }
#endif #endif
src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
+ 11
− 0
View file @ 6d3a2081
...@@ -34,6 +34,7 @@ ...@@ -34,6 +34,7 @@
#define eacsl_runtime_sound_verdict export_alias(sound_verdict) #define eacsl_runtime_sound_verdict export_alias(sound_verdict)
#define eacsl_runtime_assert export_alias(assert) #define eacsl_runtime_assert export_alias(assert)
#define eacsl_print_value export_alias(print_value) #define eacsl_print_value export_alias(print_value)
#define eacsl_print_value_content export_alias(print_value_content)
/*! E-ACSL instrumentation automatically sets this global to 0 if its verdict /*! E-ACSL instrumentation automatically sets this global to 0 if its verdict
becomes unsound. becomes unsound.
...@@ -62,4 +63,14 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) ...@@ -62,4 +63,14 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data)
void eacsl_print_value(eacsl_assert_data_value_t *value) void eacsl_print_value(eacsl_assert_data_value_t *value)
__attribute__((FC_BUILTIN)); __attribute__((FC_BUILTIN));
/*! \brief Utility function that prints the content of the given data value in
* the given stream.
* \param stream Stream where to print the value content.
* \param value Value to print to the stream.
*/
/*@ requires \valid_read(value) && \initialized(value);
@ assigns \nothing; */
void eacsl_print_value_content(FILE *stream, eacsl_assert_data_value_t *value)
__attribute__((FC_BUILTIN));
#endif // E_ACSL_ASSERT_H #endif // E_ACSL_ASSERT_H
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment