Skip to content
Snippets Groups Projects
Commit 1fa9dbe4 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[tests] simpler test for builtin labels

parent c107d973
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/syntax/clabels_builtin_labels.c
+ 19
− 24
View file @ 1fa9dbe4
int x; int x;
void named(void){ void named_1(void){
x = 4; x = 4;
Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: A:; Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: A:;
x = 5; x = 5;
...@@ -10,27 +10,22 @@ Z: T: ; ...@@ -10,27 +10,22 @@ Z: T: ;
x = 7; x = 7;
} }
void post_over_old_1(void){ Old: Post: ;} void named_2(void){
void post_over_old_2(void){ Post: Old: ;} x = 4;
A: Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: ;
void post_over_loop_1(void){ LoopEntry: Post: ;} x = 5;
void post_over_loop_2(void){ Post: LoopCurrent: ;} X: Y: ;
x = 6;
void post_over_other_1(void){ Here: Post: ;} Z: T: ;
void post_over_other_2(void){ Post: Pre: ;} x = 7;
void post_over_other_3(void){ Init: Post: Pre: ;} }
void old_over_loop_1(void){ LoopEntry: Old: ;}
void old_over_loop_2(void){ Old: LoopCurrent: ;}
void old_over_other_1(void){ Here: Old: ;}
void old_over_other_2(void){ Old: Pre: ;}
void old_over_other_3(void){ Init: Old: Pre: ;}
void loop_over_other_1(void){ Here: LoopEntry: ;}
void loop_over_other_2(void){ LoopCurrent: Pre: ;}
void loop_over_other_3(void){ Init: LoopEntry: Pre: ;}
void arbitray_other_1(void){ Here: Init: ;} void named_3(void){
void arbitray_other_2(void){ Init: Pre: ;} x = 4;
void arbitray_other_3(void){ Pre: Here: Init: ;} Init: Pre: Old: Post: A: Here: LoopCurrent: LoopEntry: ;
x = 5;
X: Y: ;
x = 6;
Z: T: ;
x = 7;
}
tests/syntax/oracle/clabels_builtin_labels.res.oracle
+ 36
− 172
View file @ 1fa9dbe4
...@@ -13,89 +13,37 @@ ...@@ -13,89 +13,37 @@
LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:5: Warning: [kernel] clabels_builtin_labels.c:5: Warning:
LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:13: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:13: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:14: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:14: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:16: Warning:
LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:16: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:17: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:17: Warning:
LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:19: Warning:
Here is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:19: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:20: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:20: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:21: Warning:
Init is a builtin ACSL label, this C label is hidden in annotations Init is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:21: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:21: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:23: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:23: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:24: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:24: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:26: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
Here is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:26: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:27: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:27: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:28: Warning:
Init is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:28: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:28: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:30: Warning:
Here is a builtin ACSL label, this C label is hidden in annotations Here is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:30: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:31: Warning:
LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:31: Warning: [kernel] clabels_builtin_labels.c:15: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:32: Warning:
Init is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:32: Warning:
LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:32: Warning: [kernel] clabels_builtin_labels.c:25: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:34: Warning:
Here is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:34: Warning:
Init is a builtin ACSL label, this C label is hidden in annotations Init is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:35: Warning: [kernel] clabels_builtin_labels.c:25: Warning:
Init is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:35: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:36: Warning:
Pre is a builtin ACSL label, this C label is hidden in annotations Pre is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:36: Warning: [kernel] clabels_builtin_labels.c:25: Warning:
Old is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:25: Warning:
Post is a builtin ACSL label, this C label is hidden in contracts
[kernel] clabels_builtin_labels.c:25: Warning:
Here is a builtin ACSL label, this C label is hidden in annotations Here is a builtin ACSL label, this C label is hidden in annotations
[kernel] clabels_builtin_labels.c:36: Warning: [kernel] clabels_builtin_labels.c:25: Warning:
Init is a builtin ACSL label, this C label is hidden in annotations LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
[kernel] clabels_builtin_labels.c:25: Warning:
LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
/* Generated by Frama-C */ /* Generated by Frama-C */
int x; int x;
void named(void) void named_1(void)
{ {
x = 4; x = 4;
A: ; A: ;
...@@ -107,111 +55,27 @@ void named(void) ...@@ -107,111 +55,27 @@ void named(void)
return; return;
} }
void post_over_old_1(void) void named_2(void)
{
__fc_user_label_Old: ;
return;
}
void post_over_old_2(void)
{
__fc_user_label_Post: ;
return;
}
void post_over_loop_1(void)
{
__fc_user_label_LoopEntry: ;
return;
}
void post_over_loop_2(void)
{
__fc_user_label_Post: ;
return;
}
void post_over_other_1(void)
{
__fc_user_label_Here: ;
return;
}
void post_over_other_2(void)
{
__fc_user_label_Post: ;
return;
}
void post_over_other_3(void)
{
__fc_user_label_Init: ;
return;
}
void old_over_loop_1(void)
{
__fc_user_label_LoopEntry: ;
return;
}
void old_over_loop_2(void)
{
__fc_user_label_Old: ;
return;
}
void old_over_other_1(void)
{ {
__fc_user_label_Here: ; x = 4;
return; A: ;
} x = 5;
X: ;
void old_over_other_2(void) x = 6;
{ Z: ;
__fc_user_label_Old: ; x = 7;
return;
}
void old_over_other_3(void)
{
__fc_user_label_Init: ;
return;
}
void loop_over_other_1(void)
{
__fc_user_label_Here: ;
return;
}
void loop_over_other_2(void)
{
__fc_user_label_LoopCurrent: ;
return;
}
void loop_over_other_3(void)
{
__fc_user_label_Init: ;
return;
}
void arbitray_other_1(void)
{
__fc_user_label_Here: ;
return;
}
void arbitray_other_2(void)
{
__fc_user_label_Init: ;
return; return;
} }
void arbitray_other_3(void) void named_3(void)
{ {
__fc_user_label_Pre: ; x = 4;
A: ;
x = 5;
X: ;
x = 6;
Z: ;
x = 7;
return; return;
} }
......
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