Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
Frama Clang
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Stefan Gränitz
Frama Clang
Commits
0655b97c
Commit
0655b97c
authored
3 years ago
by
Stefan Gränitz
Committed by
Virgile Prevosto
2 years ago
Browse files
Options
Downloads
Patches
Plain Diff
Add test for C++14 generic lambda feature
parent
3b060fb9
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
tests/basic/lambda_generic.cpp
+29
-0
29 additions, 0 deletions
tests/basic/lambda_generic.cpp
tests/basic/oracle/lambda_generic.res.oracle
+281
-0
281 additions, 0 deletions
tests/basic/oracle/lambda_generic.res.oracle
with
310 additions
and
0 deletions
tests/basic/lambda_generic.cpp
0 → 100644
+
29
−
0
View file @
0655b97c
/* run.config
OPT: @MACHDEP@ -deps -cpp-extra-args="-std=c++14" -print
*/
int
test_cxx11_lambda
(
int
cap
,
int
i
)
{
auto
lam1
=
[
cap
]
(
long
val
)
{
return
cap
-
val
;
};
return
lam1
(
i
);
}
int
test_cxx14_single_inst
(
int
cap
,
int
i
)
{
auto
lam2
=
[
cap
](
auto
val
)
{
return
cap
-
val
;
};
return
lam2
(
i
);
}
int
test_cxx14_multi_inst
(
int
cap
,
int
i
,
float
f
)
{
auto
lam3
=
[
cap
](
auto
val
)
{
return
cap
-
val
;
};
int
addend
=
1
;
if
(
lam3
(
f
)
<
.5
f
)
addend
=
0
;
return
lam3
(
i
)
+
addend
;
}
// We know argc will be 1, but the compiler doesn't know it.
int
main
(
int
argc
,
char
*
argv
[])
{
int
res1
=
test_cxx11_lambda
(
argc
,
argc
);
int
res2
=
test_cxx14_single_inst
(
argc
,
argc
);
int
res3
=
test_cxx14_multi_inst
(
argc
,
argc
,
static_cast
<
float
>
(
argc
));
return
res1
+
res2
+
res3
;
};
This diff is collapsed.
Click to expand it.
tests/basic/oracle/lambda_generic.res.oracle
0 → 100644
+
281
−
0
View file @
0655b97c
[kernel] Parsing tests/basic/lambda_generic.cpp (external front-end)
Now output intermediate result
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] tests/basic/lambda_generic.cpp:6: Warning:
signed overflow. assert -2147483648 ≤ (long)__fc_closure->cap - val;
[eva:alarm] tests/basic/lambda_generic.cpp:6: Warning:
signed overflow. assert (long)__fc_closure->cap - val ≤ 2147483647;
[eva:alarm] tests/basic/lambda_generic.cpp:11: Warning:
signed overflow. assert -2147483648 ≤ __fc_closure->cap - val;
[eva:alarm] tests/basic/lambda_generic.cpp:11: Warning:
signed overflow. assert __fc_closure->cap - val ≤ 2147483647;
[eva:alarm] tests/basic/lambda_generic.cpp:16: Warning:
signed overflow. assert -2147483648 ≤ __fc_closure->cap - val;
[eva:alarm] tests/basic/lambda_generic.cpp:16: Warning:
signed overflow. assert __fc_closure->cap - val ≤ 2147483647;
[eva:alarm] tests/basic/lambda_generic.cpp:20: Warning:
signed overflow.
assert tmp_0 + addend ≤ 2147483647;
(tmp_0 from
*(lam3.__fc_lambda_overload_3)((struct UlifEUc3capiE_ const *)(& lam3), i))
[eva:alarm] tests/basic/lambda_generic.cpp:28: Warning:
signed overflow. assert -2147483648 ≤ res1 + res2;
[eva:alarm] tests/basic/lambda_generic.cpp:28: Warning:
signed overflow. assert res1 + res2 ≤ 2147483647;
[eva:alarm] tests/basic/lambda_generic.cpp:28: Warning:
signed overflow. assert -2147483648 ≤ (int)(res1 + res2) + res3;
[eva:alarm] tests/basic/lambda_generic.cpp:28: Warning:
signed overflow. assert (int)(res1 + res2) + res3 ≤ 2147483647;
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
15 functions analyzed (out of 15): 100% coverage.
In these functions, 50 statements reached (out of 50): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
11 alarms generated by the analysis:
11 integer overflows
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
[from] Computing for function UliEUc3capiE__body_1
[from] Done for function UliEUc3capiE__body_1
[from] Computing for function UliEUc3capiE__init_1
[from] Done for function UliEUc3capiE__init_1
[from] Computing for function UliEUc3capiE__init_captures
[from] Done for function UliEUc3capiE__init_captures
[from] Computing for function UlifEUc3capiE__body_2
[from] Done for function UlifEUc3capiE__body_2
[from] Computing for function UlifEUc3capiE__body_3
[from] Done for function UlifEUc3capiE__body_3
[from] Computing for function UlifEUc3capiE__init_2
[from] Done for function UlifEUc3capiE__init_2
[from] Computing for function UlifEUc3capiE__init_3
[from] Done for function UlifEUc3capiE__init_3
[from] Computing for function UlifEUc3capiE__init_captures
[from] Done for function UlifEUc3capiE__init_captures
[from] Computing for function UllEUc3capiE__body_0
[from] Done for function UllEUc3capiE__body_0
[from] Computing for function UllEUc3capiE__init_0
[from] Done for function UllEUc3capiE__init_0
[from] Computing for function UllEUc3capiE__init_captures
[from] Done for function UllEUc3capiE__init_captures
[from] Computing for function test_cxx11_lambda
[from] Done for function test_cxx11_lambda
[from] Computing for function test_cxx14_multi_inst
[from] Done for function test_cxx14_multi_inst
[from] Computing for function test_cxx14_single_inst
[from] Done for function test_cxx14_single_inst
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function UliEUc3capiE__body_1:
\result FROM __fc_closure; val; lam2.cap
[from] Function UliEUc3capiE__init_1:
__fc_lambda_tmp_0.__fc_lambda_overload_1 FROM __fc_closure; __fc_func
[from] Function UliEUc3capiE__init_captures:
__fc_lambda_tmp_0.cap FROM __fc_closure; cap
[from] Function UlifEUc3capiE__body_2:
\result FROM __fc_closure; val; lam3.cap
[from] Function UlifEUc3capiE__body_3:
\result FROM __fc_closure; val; lam3.cap
[from] Function UlifEUc3capiE__init_2:
__fc_lambda_tmp_1.__fc_lambda_overload_2 FROM __fc_closure; __fc_func
[from] Function UlifEUc3capiE__init_3:
__fc_lambda_tmp_1.__fc_lambda_overload_3 FROM __fc_closure; __fc_func
[from] Function UlifEUc3capiE__init_captures:
__fc_lambda_tmp_1.cap FROM __fc_closure; cap
[from] Function UllEUc3capiE__body_0:
\result FROM __fc_closure; val; lam1.cap
[from] Function UllEUc3capiE__init_0:
__fc_lambda_tmp.__fc_lambda_overload_0 FROM __fc_closure; __fc_func
[from] Function UllEUc3capiE__init_captures:
__fc_lambda_tmp.cap FROM __fc_closure; cap
[from] Function test_cxx11_lambda:
\result FROM cap; i
[from] Function test_cxx14_multi_inst:
\result FROM cap; i; f
[from] Function test_cxx14_single_inst:
\result FROM cap; i
[from] Function main:
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
/* Generated by Frama-C */
struct UllEUc3capiE_ {
long (*__fc_lambda_overload_0)(struct UllEUc3capiE_ const *, long ) ;
int cap ;
};
struct UliEUc3capiE_ {
int (*__fc_lambda_overload_1)(struct UliEUc3capiE_ const *, int ) ;
int cap ;
};
struct UlifEUc3capiE_ {
int (*__fc_lambda_overload_3)(struct UlifEUc3capiE_ const *, int ) ;
float (*__fc_lambda_overload_2)(struct UlifEUc3capiE_ const *, float ) ;
int cap ;
};
void UllEUc3capiE__init_captures(struct UllEUc3capiE_ const *__fc_closure,
int cap)
{
__fc_closure->cap = cap;
return;
}
void UllEUc3capiE__init_0(struct UllEUc3capiE_ const *__fc_closure,
long (*__fc_func)(struct UllEUc3capiE_ const *,
long ))
{
__fc_closure->__fc_lambda_overload_0 = __fc_func;
return;
}
long UllEUc3capiE__body_0(struct UllEUc3capiE_ const *__fc_closure, long val)
{
long __retres;
/*@ assert
Eva: signed_overflow: -2147483648 ≤ (long)__fc_closure->cap - val;
*/
/*@ assert
Eva: signed_overflow: (long)__fc_closure->cap - val ≤ 2147483647;
*/
__retres = (long)__fc_closure->cap - val;
return __retres;
}
int test_cxx11_lambda(int cap, int i)
{
struct UllEUc3capiE_ lam1;
struct UllEUc3capiE_ const __fc_lambda_tmp;
int tmp;
UllEUc3capiE__init_captures(& __fc_lambda_tmp,cap);
UllEUc3capiE__init_0(& __fc_lambda_tmp,& UllEUc3capiE__body_0);
lam1 = __fc_lambda_tmp;
tmp = (int)(*(lam1.__fc_lambda_overload_0))((struct UllEUc3capiE_ const *)(& lam1),
(long)i);
return tmp;
}
void UliEUc3capiE__init_captures(struct UliEUc3capiE_ const *__fc_closure,
int cap)
{
__fc_closure->cap = cap;
return;
}
void UliEUc3capiE__init_1(struct UliEUc3capiE_ const *__fc_closure,
int (*__fc_func)(struct UliEUc3capiE_ const *, int ))
{
__fc_closure->__fc_lambda_overload_1 = __fc_func;
return;
}
int UliEUc3capiE__body_1(struct UliEUc3capiE_ const *__fc_closure, int val)
{
int __retres;
/*@ assert Eva: signed_overflow: -2147483648 ≤ __fc_closure->cap - val;
*/
/*@ assert Eva: signed_overflow: __fc_closure->cap - val ≤ 2147483647; */
__retres = __fc_closure->cap - val;
return __retres;
}
int test_cxx14_single_inst(int cap, int i)
{
struct UliEUc3capiE_ lam2;
struct UliEUc3capiE_ const __fc_lambda_tmp_0;
int tmp;
UliEUc3capiE__init_captures(& __fc_lambda_tmp_0,cap);
UliEUc3capiE__init_1(& __fc_lambda_tmp_0,& UliEUc3capiE__body_1);
lam2 = __fc_lambda_tmp_0;
tmp = (*(lam2.__fc_lambda_overload_1))((struct UliEUc3capiE_ const *)(& lam2),
i);
return tmp;
}
void UlifEUc3capiE__init_captures(struct UlifEUc3capiE_ const *__fc_closure,
int cap)
{
__fc_closure->cap = cap;
return;
}
void UlifEUc3capiE__init_3(struct UlifEUc3capiE_ const *__fc_closure,
int (*__fc_func)(struct UlifEUc3capiE_ const *,
int ))
{
__fc_closure->__fc_lambda_overload_3 = __fc_func;
return;
}
int UlifEUc3capiE__body_3(struct UlifEUc3capiE_ const *__fc_closure, int val)
{
int __retres;
/*@ assert Eva: signed_overflow: -2147483648 ≤ __fc_closure->cap - val;
*/
/*@ assert Eva: signed_overflow: __fc_closure->cap - val ≤ 2147483647; */
__retres = __fc_closure->cap - val;
return __retres;
}
void UlifEUc3capiE__init_2(struct UlifEUc3capiE_ const *__fc_closure,
float (*__fc_func)(struct UlifEUc3capiE_ const *,
float ))
{
__fc_closure->__fc_lambda_overload_2 = __fc_func;
return;
}
float UlifEUc3capiE__body_2(struct UlifEUc3capiE_ const *__fc_closure,
float val)
{
float __retres;
__retres = (float)__fc_closure->cap - val;
return __retres;
}
int test_cxx14_multi_inst(int cap, int i, float f)
{
int __retres;
struct UlifEUc3capiE_ lam3;
struct UlifEUc3capiE_ const __fc_lambda_tmp_1;
float tmp;
int tmp_0;
UlifEUc3capiE__init_captures(& __fc_lambda_tmp_1,cap);
UlifEUc3capiE__init_3(& __fc_lambda_tmp_1,& UlifEUc3capiE__body_3);
UlifEUc3capiE__init_2(& __fc_lambda_tmp_1,& UlifEUc3capiE__body_2);
lam3 = __fc_lambda_tmp_1;
int addend = 1;
tmp = (*(lam3.__fc_lambda_overload_2))((struct UlifEUc3capiE_ const *)(& lam3),
f);
if ((double)tmp < 0.5) addend = 0;
tmp_0 = (*(lam3.__fc_lambda_overload_3))((struct UlifEUc3capiE_ const *)(& lam3),
i);
;
/*@ assert Eva: signed_overflow: tmp_0 + addend ≤ 2147483647; */
__retres = tmp_0 + addend;
return __retres;
}
int main(int argc, char **argv)
{
int __retres;
int res1 = test_cxx11_lambda(argc,argc);
int res2 = test_cxx14_single_inst(argc,argc);
int res3 = test_cxx14_multi_inst(argc,argc,(float)argc);
/*@ assert Eva: signed_overflow: -2147483648 ≤ res1 + res2; */
/*@ assert Eva: signed_overflow: res1 + res2 ≤ 2147483647; */
/*@ assert Eva: signed_overflow: -2147483648 ≤ (int)(res1 + res2) + res3;
*/
/*@ assert Eva: signed_overflow: (int)(res1 + res2) + res3 ≤ 2147483647;
*/
__retres = (res1 + res2) + res3;
return __retres;
}
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment