Skip to content
Snippets Groups Projects
Commit f3557e7c authored by Benjamin Jorge's avatar Benjamin Jorge Committed by Thibault Martin
Browse files

[tests] Add the example from issue 1373 as a test

parent 740ccad3
No related branches found
No related tags found
No related merge requests found
/* run.config
STDOPT:
*/
struct foo { char bar[4]; };
/*@ assigns x->bar[0..3] \from x->bar[0..3]; */
int f(struct foo* x);
void main() {
int a = 0;
//@ assert \subset(a, (0..1));
}
[kernel] Parsing issue-1373-ranges.i (no preprocessing)
/* Generated by Frama-C */
struct foo {
char bar[4] ;
};
/*@ assigns x->bar[0 .. 3];
assigns x->bar[0 .. 3] \from x->bar[0 .. 3]; */
int f(struct foo *x);
void main(void)
{
int a = 0;
/*@ assert \subset(a, (0 .. 1)); */ ;
return;
}
[kernel] Parsing ocode_issue-1373-ranges.c (with preprocessing)
[kernel] Parsing issue-1373-ranges.i (no preprocessing)
[kernel] issue-1373-ranges.i:10: Warning:
def'n of func main at issue-1373-ranges.i:10 (sum 1968) conflicts with the one at ocode_issue-1373-ranges.c:9 (sum 2855); keeping the one at ocode_issue-1373-ranges.c:9.
/* Generated by Frama-C */
struct foo {
char bar[4] ;
};
/*@ assigns x->bar[0 .. 3];
assigns x->bar[0 .. 3] \from x->bar[0 .. 3]; */
int f(struct foo *x);
void main(void)
{
int a = 0;
/*@ assert \subset(a, (0 .. 1)); */ ;
return;
}
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