Skip to content
Snippets Groups Projects
Commit 9589568f authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Added test case checking initialization of memory layout

parent e21964f5
No related branches found
No related tags found
No related merge requests found
/* run.config
COMMENT: Malloc executed by a library function
*/
#include <limits.h>
#include <stdlib.h>
int main(int argc, const char **argv) {
/* If the second argument of `realpath` is NULL it uses malloc.
Make sure that memory layout has been initialized. */
char *cwd = realpath(".", NULL);
return 0;
}
/* Generated by Frama-C */
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
/*@ assigns \result, *((char *)x_1 + (0 ..));
assigns \result \from *(x_0 + (0 ..)), *((char *)x_1 + (0 ..));
assigns *((char *)x_1 + (0 ..))
\from *(x_0 + (0 ..)), *((char *)x_1 + (0 ..));
*/
extern int ( /* missing proto */ realpath)(char const *x_0, void *x_1);
void __e_acsl_globals_init(void)
{
__gen_e_acsl_literal_string = ".";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("."));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
return;
}
int main(int argc, char const **argv)
{
int __retres;
int tmp;
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
tmp = realpath(__gen_e_acsl_literal_string,(void *)0);
char *cwd = (char *)tmp;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
}
tests/runtime/hidden_malloc.c:11:[kernel] warning: Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
tests/runtime/hidden_malloc.c:11:[kernel] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/hidden_malloc.c:11:[value] warning: Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
Ignoring.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment