Skip to content
Snippets Groups Projects
Commit 4d5d4f62 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[analysis-scripts] add test for estimate-difficulty

parent af462ca5
No related branches found
No related tags found
No related merge requests found
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err
*/
// these includes are not actually used by the compiler
// (this is a preprocessed file), but analyzed by the script
#include <sys/socket.h>
# include <complex.h>
# include <langinfo.h>
#include <sys/socket.h>
void g() {
int g = 42;
}
void f() {
if (v) f();
else g();
}
int main() {
va_arg(); // no warning: it is a macro, not a function
setjmp(); // warning: problematic
strlen(); // no warning
ccosl(); // warning: neither code nor spec
dprintf(); // no warning: neither code nor spec, but handled by Variadic
}
Building callgraph...
Computing data about libc/POSIX functions...
[recursion] found recursive cycle near estimate_difficulty.i:18: f -> f
Estimating difficulty for 7 function calls...
- warning: ccosl (POSIX) has neither code nor spec in Frama-C's libc
- warning: setjmp (POSIX) is known to be problematic for code analysis
Function-related warnings: 2
Estimating difficulty for 3 '#include <header>' directives...
- WARNING: included header <complex.h> is explicitly unsupported by Frama-C
- warning: included header <langinfo.h> not currently included in Frama-C's libc
Header-related warnings: 2
Looking for 'main2' inside 14 file(s)... Looking for 'main2' inside 15 file(s)...
Possible declarations for function 'main2' in the following file(s): Possible declarations for function 'main2' in the following file(s):
for-find-fun.c for-find-fun.c
Possible definitions for function 'main2' in the following file(s): Possible definitions for function 'main2' in the following file(s):
......
Looking for 'main3' inside 14 file(s)... Looking for 'main3' inside 15 file(s)...
Possible declarations for function 'main3' in the following file(s): Possible declarations for function 'main3' in the following file(s):
for-find-fun2.c for-find-fun2.c
Possible definitions for function 'main3' in the following file(s): Possible definitions for function 'main3' in the following file(s):
......
Looking for 'false_positive' inside 14 file(s)... Looking for 'false_positive' inside 15 file(s)...
No declaration/definition found for function 'false_positive' No declaration/definition found for function 'false_positive'
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