Commit ca9c296b authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'bugfix/basile/eacsl-rtl-prefix' into 'master'

[eacsl] Fix debug compilation

See merge request frama-c/frama-c!2893
parents c5022645 15a5ef12
......@@ -39,7 +39,8 @@
* otherwise.
int separated2(void * ptr1, size_t size1, void * ptr2, size_t size2) {
DASSERT(valid_read(ptr1, size1, base_addr(ptr1), NULL) && valid_read(ptr2, size2, base_addr(ptr2), NULL));
DASSERT(eacsl_valid_read(ptr1, size1, eacsl_base_addr(ptr1), NULL)
&& eacsl_valid_read(ptr2, size2, eacsl_base_addr(ptr2), NULL));
// Cast pointers to char* to be able to do pointer arithmetic without
// triggering undefined behavior
/* run.config_ci, run.config_dev
COMMENT: Compile RTL with debug and debug verbose informations
STDOPT:#"-e-acsl-debug 1"
MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose
int main() {
return 0;
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int main(void)
int __retres;
__retres = 0;
return __retres;
Supports Markdown
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