Skip to content
Snippets Groups Projects
Commit 87eddd2d authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[tests] restore ./tests from master

parent 7ad28b92
No related branches found
No related tags found
No related merge requests found
Showing
with 169 additions and 221 deletions
[kernel] Parsing log-file.i (no preprocessing) [kernel] Parsing tests/misc/log-file.i (no preprocessing)
[eva] Analyzing a complete application starting at main [eva] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva] computing for function f <- main. [eva] computing for function f <- main.
Called from log-file.i:20. Called from tests/misc/log-file.i:20.
[eva] using specification for function f [eva] using specification for function f
[eva] Done for function f [eva] Done for function f
[eva] computing for function g <- main. [eva] computing for function g <- main.
Called from log-file.i:21. Called from tests/misc/log-file.i:21.
[eva] using specification for function g [eva] using specification for function g
[eva] Done for function g [eva] Done for function g
log-file.i:22:[eva] starting to merge loop iterations tests/misc/log-file.i:22:[eva] starting to merge loop iterations
[eva] Recording results for main [eva] Recording results for main
[eva] done for function main [eva] done for function main
log-file.i:20:[kernel:annot:missing-spec] warning: Neither code nor specification for function f, generating default assigns from the prototype tests/misc/log-file.i:20:[kernel:annot:missing-spec] warning: Neither code nor specification for function f, generating default assigns from the prototype
...@@ -2,15 +2,15 @@ ...@@ -2,15 +2,15 @@
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva] computing for function f <- main. [eva] computing for function f <- main.
Called from log-file.i:20. Called from tests/misc/log-file.i:20.
[eva] using specification for function f [eva] using specification for function f
[eva] Done for function f [eva] Done for function f
[eva] computing for function g <- main. [eva] computing for function g <- main.
Called from log-file.i:21. Called from tests/misc/log-file.i:21.
[eva] using specification for function g [eva] using specification for function g
log-file.i:17:[eva] warning: no 'assigns \result \from ...' clause specified for function g tests/misc/log-file.i:17:[eva] warning: no 'assigns \result \from ...' clause specified for function g
[eva] Done for function g [eva] Done for function g
log-file.i:22:[eva] starting to merge loop iterations tests/misc/log-file.i:22:[eva] starting to merge loop iterations
[eva] Recording results for main [eva] Recording results for main
[eva] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
log-file.i:17:[eva] warning: no 'assigns \result \from ...' clause specified for function g tests/misc/log-file.i:17:[eva] warning: no 'assigns \result \from ...' clause specified for function g
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[kernel] Parsing log-file.i (no preprocessing)
[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] computing for function f <- main.
Called from log-file.i:20.
[kernel:annot:missing-spec] log-file.i:20: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] Done for function f
[eva] computing for function g <- main.
Called from log-file.i:21.
[eva] using specification for function g
[eva] log-file.i:17: Warning:
no 'assigns \result \from ...' clause specified for function g
[eva] Done for function g
[eva] log-file.i:22: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
r ∈ [--..--]
__retres ∈ {0}
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
[from] Computing for function g <-main
[from] Done for function g
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
\result FROM \nothing
[from] Function g:
\result FROM ANYTHING(origin:Unknown)
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
r; i; __retres
[inout] Inputs for function main:
\nothing
[kernel] Parsing log-file.i (no preprocessing)
[kernel:foo-category] result with dkey
[kernel] result
[kernel:foo-category] feedback with dkey
[kernel] feedback
[kernel:foo-category] debug (level 0) with dkey
[kernel] debug (level 0)
[kernel] Warning: warning
[report] Monitoring events [report] Monitoring events
[kernel] User Error: option `-foobar' is unknown. [kernel] User Error: option `-foobar' is unknown.
use `frama-c -help' for more information. use `bin/toplevel.opt -help' for more information.
[report] User Error: Invalid action ("JAZZ") [report] User Error: Invalid action ("JAZZ")
[kernel] Plug-in report aborted: invalid user input. [kernel] Plug-in report aborted: invalid user input.
[kernel] Parsing log-file.i (no preprocessing) [kernel] Parsing tests/misc/log-file.i (no preprocessing)
[kernel:foo-category] result with dkey [kernel:foo-category] result with dkey
[kernel] result [kernel] result
[kernel:foo-category] feedback with dkey [kernel:foo-category] feedback with dkey
......
This file present the tests in ppc/test/pdg that deal with the This file present the tests in ppc/test/pdg that deal with the
Program Dependence Graph computation. Program Dependence Graph computation.
** dpds_intra.c ** tests/pdg/dpds_intra.c
many small tests for the PDG. many small tests for the PDG.
The function "test_ctrl_dpd_multiple" is a case where some The function "test_ctrl_dpd_multiple" is a case where some
PDG nodes should have more than one control dependencies, PDG nodes should have more than one control dependencies,
but it cannot be tested because the value analysis doesn't work on that case. but it cannot be tested because the value analysis doesn't work on that case.
** simple_call.c ** tests/pdg/simple_call.c
tests for the PDG of function calls. tests for the PDG of function calls.
** calls_and_implicits.c ** tests/pdg/calls_and_implicits.c
test the PDG for dependencies between global variables in calls. test the PDG for dependencies between global variables in calls.
Check if inputs and outputs are not mixed up. Check if inputs and outputs are not mixed up.
** calls_and_struct.c ** tests/pdg/calls_and_struct.c
test the PDG for dependencies with structures. test the PDG for dependencies with structures.
In the function 'asgn_struct' we see that the precision could be better. In the function 'asgn_struct' we see that the precision could be better.
** decl_dpds.c ** tests/pdg/decl_dpds.c
test the PDG with pointers and global variables. test the PDG with pointers and global variables.
** globals.c ** tests/pdg/globals.c
Some tests to have more information about value analysis results. Some tests to have more information about value analysis results.
Some of the results seem strange... Some of the results seem strange...
** inter_alias2.c ** tests/pdg/inter_alias2.c
Test the PDG with pointers. Test the PDG with pointers.
Show that the alias analysis merge the contexts and the precison problem. Show that the alias analysis merge the contexts and the precison problem.
** inter_alias.c ** tests/pdg/inter_alias.c
Test the PDG with pointers. Test the PDG with pointers.
** multiple_calls.c ** tests/pdg/multiple_calls.c
Test the PDG for call through function pointer. Test the PDG for call through function pointer.
** no_body.c ** tests/pdg/no_body.c
Test the PDG for call to a function that has no body. Test the PDG for call to a function that has no body.
It is strange that the result of the function doesn't depend on the inputs, It is strange that the result of the function doesn't depend on the inputs,
but it is the behaviour of the whole tool. but it is the behaviour of the whole tool.
** pb_infinite_loop.c ** tests/pdg/pb_infinite_loop.c
Infinite loop => no post-dominator computation (not defined in this case). Infinite loop => no post-dominator computation (not defined in this case).
Not-Implemented-Yet ! Not-Implemented-Yet !
We should over-approximate the control dependencies in the loop We should over-approximate the control dependencies in the loop
so that every statement depend on every test. so that every statement depend on every test.
** variadic.c ** tests/pdg/variadic.c
Test a call to a function with a variable number of arguments. Test a call to a function with a variable number of arguments.
The PDG of the variadic function is not computed -> TOP. The PDG of the variadic function is not computed -> TOP.
** dyn_dpds.c + dyn_dpds.ml ** tests/pdg/dyn_dpds.c + tests/pdg/dyn_dpds.ml
Test for the dynamic dependencies. Test for the dynamic dependencies.
** call.c ** tests/pdg/call.c
A very simple example to generate graph for the documentation. A very simple example to generate graph for the documentation.
** doc_dot.c ** tests/pdg/doc_dot.c
A very simple example to show the different kinds of nodes and link A very simple example to show the different kinds of nodes and link
in a .dot file (also for the documentation). in a .dot file (also for the documentation).
...@@ -11,8 +11,8 @@ ...@@ -11,8 +11,8 @@
STDOPT: +"-fct-pdg main" STDOPT: +"-fct-pdg main"
STDOPT: +"-fct-pdg multiple_global_inputs" STDOPT: +"-fct-pdg multiple_global_inputs"
*/ */
/* bin/toplevel.opt -deps -main g dpds_intra.c */ /* bin/toplevel.opt -deps -main g tests/slicing/dpds_intra.c */
/* bin/toplevel.opt -fct-pdg test_goto_simple dpds_intra.c -pdg-dot */ /* bin/toplevel.opt -fct-pdg test_goto_simple tests/slicing/dpds_intra.c -pdg-dot */
extern int G; extern int G;
...@@ -81,7 +81,7 @@ int test_goto_else (void) { ...@@ -81,7 +81,7 @@ int test_goto_else (void) {
} }
/* ne passe pas l'analyse de valeur (bouclage) /* ne passe pas l'analyse de valeur (bouclage)
./bin/toplevel.opt -eva -main test_ctrl_dpd_multiple dpds_intra.c ./bin/toplevel.opt -eva -main test_ctrl_dpd_multiple tests/slicing/dpds_intra.c
* cf. mail Pascal Re: loop_pragma UNROLL_LOOP du 09.05.2006 15:03 */ * cf. mail Pascal Re: loop_pragma UNROLL_LOOP du 09.05.2006 15:03 */
int test_ctrl_dpd_multiple (void) { int test_ctrl_dpd_multiple (void) {
int x = 0; int x = 0;
......
...@@ -3,8 +3,8 @@ ...@@ -3,8 +3,8 @@
* STDOPT: +"-fct-pdg main -inout " * STDOPT: +"-fct-pdg main -inout "
*/ */
/* /*
* ledit bin/toplevel.top no_body.c -fct-pdg main * ledit bin/toplevel.top tests/slicing/no_body.c -fct-pdg main
* #use "select.ml";; * #use "tests/slicing/select.ml";;
* test "loop" (select_data "G");; * test "loop" (select_data "G");;
*/ */
......
...@@ -24,6 +24,34 @@ ...@@ -24,6 +24,34 @@
[eva] Done for function swap [eva] Done for function swap
[eva] Recording results for main [eva] Recording results for main
[eva] done for function main [eva] done for function main
[inout] InOut (internal) for function f:
Operational inputs:
G
Operational inputs on termination:
G
Sure outputs:
G; __retres
[inout] InOut (internal) for function f2:
Operational inputs:
G
Operational inputs on termination:
G
Sure outputs:
G2; __retres
[inout] InOut (internal) for function swap:
Operational inputs:
G; G2
Operational inputs on termination:
G; G2
Sure outputs:
G; G2; tmp
[inout] InOut (internal) for function main:
Operational inputs:
\nothing
Operational inputs on termination:
\nothing
Sure outputs:
t{[0]; [2]}; G; G2; __retres
[pdg] computing for function main [pdg] computing for function main
[from] Computing for function f [from] Computing for function f
[from] Done for function f [from] Done for function f
...@@ -88,31 +116,3 @@ ...@@ -88,31 +116,3 @@
-[--d]-> 17 -[--d]-> 17
{n19}: OutRet {n19}: OutRet
-[--d]-> 18 -[--d]-> 18
[inout] InOut (internal) for function f:
Operational inputs:
G
Operational inputs on termination:
G
Sure outputs:
G; __retres
[inout] InOut (internal) for function f2:
Operational inputs:
G
Operational inputs on termination:
G
Sure outputs:
G2; __retres
[inout] InOut (internal) for function swap:
Operational inputs:
G; G2
Operational inputs on termination:
G; G2
Sure outputs:
G; G2; tmp
[inout] InOut (internal) for function main:
Operational inputs:
\nothing
Operational inputs on termination:
\nothing
Sure outputs:
t{[0]; [2]}; G; G2; __retres
...@@ -38,6 +38,39 @@ ...@@ -38,6 +38,39 @@
C FROM \nothing C FROM \nothing
\result FROM S \result FROM S
[from] ====== END OF DEPENDENCIES ====== [from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function asgn_struct:
s; __retres
[inout] Inputs for function asgn_struct:
S
[inout] InOut (internal) for function asgn_struct:
Operational inputs:
S
Operational inputs on termination:
S
Sure outputs:
s; __retres
[inout] Out (internal) for function f:
S.a; A; __retres
[inout] Inputs for function f:
S.b; A
[inout] InOut (internal) for function f:
Operational inputs:
S.b; A; s{.a; .b}
Operational inputs on termination:
S.b; A; s{.a; .b}
Sure outputs:
S.a; A; __retres
[inout] Out (internal) for function main:
S.a; A; B; C; a; tmp_0
[inout] Inputs for function main:
S; A
[inout] InOut (internal) for function main:
Operational inputs:
S
Operational inputs on termination:
S
Sure outputs:
S.a; A; B; C; a; tmp_0
[pdg] computing for function asgn_struct [pdg] computing for function asgn_struct
[pdg] done for function asgn_struct [pdg] done for function asgn_struct
[pdg] computing for function f [pdg] computing for function f
...@@ -140,36 +173,3 @@ ...@@ -140,36 +173,3 @@
-[--d]-> 33 -[--d]-> 33
{n35}: In(S.b) {n35}: In(S.b)
{n36}: In(S) {n36}: In(S)
[inout] Out (internal) for function asgn_struct:
s; __retres
[inout] Inputs for function asgn_struct:
S
[inout] InOut (internal) for function asgn_struct:
Operational inputs:
S
Operational inputs on termination:
S
Sure outputs:
s; __retres
[inout] Out (internal) for function f:
S.a; A; __retres
[inout] Inputs for function f:
S.b; A
[inout] InOut (internal) for function f:
Operational inputs:
S.b; A; s{.a; .b}
Operational inputs on termination:
S.b; A; s{.a; .b}
Sure outputs:
S.a; A; __retres
[inout] Out (internal) for function main:
S.a; A; B; C; a; tmp_0
[inout] Inputs for function main:
S; A
[inout] InOut (internal) for function main:
Operational inputs:
S
Operational inputs on termination:
S
Sure outputs:
S.a; A; B; C; a; tmp_0
...@@ -67,6 +67,18 @@ ...@@ -67,6 +67,18 @@
G3.M2 FROM G1.M2; G4; G5 G3.M2 FROM G1.M2; G4; G5
\result FROM \nothing \result FROM \nothing
[from] ====== END OF CALLWISE DEPENDENCIES ====== [from] ====== END OF CALLWISE DEPENDENCIES ======
[inout] Out (internal) for function F1:
G3.M2
[inout] Inputs for function F1:
G2.M2; G5
[inout] Out (internal) for function F2:
G1.M1; V1
[inout] Inputs for function F2:
G4
[inout] Out (internal) for function main:
G1.M1; G2; G3.M2; V2
[inout] Inputs for function main:
G1; G2.M2; G4; G5
[pdg] computing for function F1 [pdg] computing for function F1
[pdg] done for function F1 [pdg] done for function F1
[pdg] computing for function F2 [pdg] computing for function F2
...@@ -154,15 +166,3 @@ ...@@ -154,15 +166,3 @@
{n30}: In(G5) {n30}: In(G5)
{n31}: In(G1.M2) {n31}: In(G1.M2)
{n32}: In(G4) {n32}: In(G4)
[inout] Out (internal) for function F1:
G3.M2
[inout] Inputs for function F1:
G2.M2; G5
[inout] Out (internal) for function F2:
G1.M1; V1
[inout] Inputs for function F2:
G4
[inout] Out (internal) for function main:
G1.M1; G2; G3.M2; V2
[inout] Inputs for function main:
G1; G2.M2; G4; G5
...@@ -39,6 +39,14 @@ ...@@ -39,6 +39,14 @@
[from] entry point: [from] entry point:
\result FROM G \result FROM G
[from] ====== END OF CALLWISE DEPENDENCIES ====== [from] ====== END OF CALLWISE DEPENDENCIES ======
[inout] Out (internal) for function f1:
a; b; __retres
[inout] Inputs for function f1:
G; a; b
[inout] Out (internal) for function main:
a; b; __retres
[inout] Inputs for function main:
G
[pdg] computing for function f1 [pdg] computing for function f1
[pdg] done for function f1 [pdg] done for function f1
[pdg] computing for function main [pdg] computing for function main
...@@ -138,11 +146,3 @@ ...@@ -138,11 +146,3 @@
{n30}: OutRet {n30}: OutRet
-[--d]-> 29 -[--d]-> 29
{n31}: In(G) {n31}: In(G)
[inout] Out (internal) for function f1:
a; b; __retres
[inout] Inputs for function f1:
G; a; b
[inout] Out (internal) for function main:
a; b; __retres
[inout] Inputs for function main:
G
...@@ -47,6 +47,27 @@ ...@@ -47,6 +47,27 @@
G4 FROM c; d (and SELF) G4 FROM c; d (and SELF)
\result FROM G1; G2; c; d \result FROM G1; G2; c; d
[from] ====== END OF DEPENDENCIES ====== [from] ====== END OF DEPENDENCIES ======
[inout] InOut (internal) for function fct1:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G1; G3; G4
[inout] InOut (internal) for function fct2:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G2; G3
[inout] InOut (internal) for function appel_ptr_fct:
Operational inputs:
G1; G2; c; d
Operational inputs on termination:
G1; G2; c; d
Sure outputs:
G3; a; b; pf; tmp; x; tmp_0; __retres
[pdg] computing for function appel_ptr_fct [pdg] computing for function appel_ptr_fct
[pdg] done for function appel_ptr_fct [pdg] done for function appel_ptr_fct
[pdg] PDG for appel_ptr_fct [pdg] PDG for appel_ptr_fct
...@@ -157,24 +178,3 @@ ...@@ -157,24 +178,3 @@
-[--d]-> 30 -[--d]-> 30
{n32}: In(G1) {n32}: In(G1)
{n33}: In(G2) {n33}: In(G2)
[inout] InOut (internal) for function fct1:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G1; G3; G4
[inout] InOut (internal) for function fct2:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G2; G3
[inout] InOut (internal) for function appel_ptr_fct:
Operational inputs:
G1; G2; c; d
Operational inputs on termination:
G1; G2; c; d
Sure outputs:
G3; a; b; pf; tmp; x; tmp_0; __retres
...@@ -41,6 +41,27 @@ ...@@ -41,6 +41,27 @@
G4 FROM c; a; b G4 FROM c; a; b
\result FROM c; a; b \result FROM c; a; b
[from] ====== END OF DEPENDENCIES ====== [from] ====== END OF DEPENDENCIES ======
[inout] InOut (internal) for function fct1:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G1; G3; G4
[inout] InOut (internal) for function fct2:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G2; G3
[inout] InOut (internal) for function appel_ptr_fct_bis:
Operational inputs:
c; a; b; d
Operational inputs on termination:
c; a; b; d
Sure outputs:
G3; G4; pf; tmp
[pdg] computing for function appel_ptr_fct_bis [pdg] computing for function appel_ptr_fct_bis
[pdg] done for function appel_ptr_fct_bis [pdg] done for function appel_ptr_fct_bis
[pdg] PDG for appel_ptr_fct_bis [pdg] PDG for appel_ptr_fct_bis
...@@ -130,24 +151,3 @@ ...@@ -130,24 +151,3 @@
-[--d]-> 23 -[--d]-> 23
{n26}: OutRet {n26}: OutRet
-[--d]-> 25 -[--d]-> 25
[inout] InOut (internal) for function fct1:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G1; G3; G4
[inout] InOut (internal) for function fct2:
Operational inputs:
x; y; z
Operational inputs on termination:
x; y; z
Sure outputs:
G2; G3
[inout] InOut (internal) for function appel_ptr_fct_bis:
Operational inputs:
c; a; b; d
Operational inputs on termination:
c; a; b; d
Sure outputs:
G3; G4; pf; tmp
...@@ -31,6 +31,20 @@ ...@@ -31,6 +31,20 @@
[eva] Done for function loop [eva] Done for function loop
[eva] Recording results for main [eva] Recording results for main
[eva] done for function main [eva] done for function main
[inout] InOut (internal) for function loop:
Operational inputs:
G; x
Operational inputs on termination:
G; x
Sure outputs:
tmp
[inout] InOut (internal) for function main:
Operational inputs:
\nothing
Operational inputs on termination:
\nothing
Sure outputs:
G; x
[pdg] computing for function main [pdg] computing for function main
[from] Computing for function f [from] Computing for function f
[from] Done for function f [from] Done for function f
...@@ -68,17 +82,3 @@ ...@@ -68,17 +82,3 @@
-[--d]-> 8 -[--d]-> 8
{n10}: return; {n10}: return;
-[-c-]-> 1 -[-c-]-> 1
[inout] InOut (internal) for function loop:
Operational inputs:
G; x
Operational inputs on termination:
G; x
Sure outputs:
tmp
[inout] InOut (internal) for function main:
Operational inputs:
\nothing
Operational inputs on termination:
\nothing
Sure outputs:
G; x
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