Commit 078a1a27 authored by Basile Desloges 's avatar Basile Desloges
Browse files

[eacsl] Add tests for memory models compilation

parent 4774cd29
/* run.config_ci, run.config_dev
COMMENT: Compile RTL with bittree memory model
STDOPT:#"-e-acsl-full-mtracking"
MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model bittree
*/
int main() {
return 0;
}
/* run.config_ci, run.config_dev
COMMENT: Compile RTL with segment memory model
STDOPT:#"-e-acsl-full-mtracking"
MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model segment
*/
int main() {
return 0;
}
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[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;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& __retres),(size_t)4);
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
__e_acsl_delete_block((void *)(& __retres));
__e_acsl_memory_clean();
return __retres;
}
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& __retres),(size_t)4);
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
__e_acsl_delete_block((void *)(& __retres));
__e_acsl_memory_clean();
return __retres;
}
Markdown is supported
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