Skip to content
Snippets Groups Projects
Commit c5aa8c33 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'kostyantyn/feature/bts2192' into 'master'

BTS test cases

- added test case for resolved bts1292 
- added missing COMMENT header to bts1291 

See merge request !79
parents 7f0bf785 426884d8
No related branches found
No related tags found
No related merge requests found
/* run.config
COMMENT: bts #2191, issue with unrolling types of struct members
*/
struct ST { struct ST {
char *str; char *str;
int num; int num;
......
/* run.config
COMMENT: bts #2292, failures due to unregistered RTL functions
*/
#include <stdlib.h>
int a;
char *n = "134";
int main(int argc, char **argv) {
a = argc = atoi(n);
}
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `atoi':
the generated program may miss memory instrumentation
if there are memory-related annotations.
FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
...@@ -44,7 +44,7 @@ int main(int argc, char **argv) ...@@ -44,7 +44,7 @@ int main(int argc, char **argv)
} }
else __gen_e_acsl_and = 0; else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
(char *)"\\valid_read(_G[0].str)",18); (char *)"\\valid_read(_G[0].str)",22);
} }
__retres = 0; __retres = 0;
__e_acsl_delete_block((void *)(_G)); __e_acsl_delete_block((void *)(_G));
......
/* Generated by Frama-C */
int a;
char *n = (char *)"134";
int main(int argc, char **argv)
{
int __retres;
{ /* sequence */
argc = __gen_e_acsl_atoi((char const *)n);
a = argc;
}
__retres = 0;
return __retres;
}
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