diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle index 5db81403d65099d71df5e71e22f7a50dd33d02a7..601275105a3e54601c7daab8b1a8b3f3d7572912 100644 --- a/tests/slicing/oracle/variadic.0.res.oracle +++ b/tests/slicing/oracle/variadic.0.res.oracle @@ -6,33 +6,33 @@ [eva:initial-state] Values of globals at initialization [eva] computing for function f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37. + Called from TESTS/pdg/variadic.c:37. [eva] computing for function lib_f <- f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23. -[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: + Called from TESTS/pdg/variadic.c:23. +[kernel:annot:missing-spec] TESTS/pdg/variadic.c:23: Warning: Neither code nor specification for function lib_f, generating default assigns from the prototype [eva] using specification for function lib_f [eva] Done for function lib_f [eva] Recording results for f1 [eva] Done for function f1 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38. + Called from TESTS/pdg/variadic.c:38. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 [eva] computing for function f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39. + Called from TESTS/pdg/variadic.c:39. [eva] computing for function lib_f <- f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31. + Called from TESTS/pdg/variadic.c:31. [eva] Done for function lib_f [eva] Recording results for f3 [eva] Done for function f3 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40. + Called from TESTS/pdg/variadic.c:40. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 diff --git a/tests/slicing/oracle/variadic.1.res.oracle b/tests/slicing/oracle/variadic.1.res.oracle index d7485ec33c9fc39ac7be2572259d7051dae00c03..3c686905b1faa30a6ebbfadc199c8d500d7784fc 100644 --- a/tests/slicing/oracle/variadic.1.res.oracle +++ b/tests/slicing/oracle/variadic.1.res.oracle @@ -6,33 +6,33 @@ [eva:initial-state] Values of globals at initialization [eva] computing for function f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37. + Called from TESTS/pdg/variadic.c:37. [eva] computing for function lib_f <- f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23. -[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: + Called from TESTS/pdg/variadic.c:23. +[kernel:annot:missing-spec] TESTS/pdg/variadic.c:23: Warning: Neither code nor specification for function lib_f, generating default assigns from the prototype [eva] using specification for function lib_f [eva] Done for function lib_f [eva] Recording results for f1 [eva] Done for function f1 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38. + Called from TESTS/pdg/variadic.c:38. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 [eva] computing for function f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39. + Called from TESTS/pdg/variadic.c:39. [eva] computing for function lib_f <- f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31. + Called from TESTS/pdg/variadic.c:31. [eva] Done for function lib_f [eva] Recording results for f3 [eva] Done for function f3 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40. + Called from TESTS/pdg/variadic.c:40. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 diff --git a/tests/slicing/oracle/variadic.2.res.oracle b/tests/slicing/oracle/variadic.2.res.oracle index 9e85774a6e565cc9b02d9e22bc467e69fb2633cc..9b5a8a3007b9d5e57aa1b8b6b442f0bc9de3f60e 100644 --- a/tests/slicing/oracle/variadic.2.res.oracle +++ b/tests/slicing/oracle/variadic.2.res.oracle @@ -6,33 +6,33 @@ [eva:initial-state] Values of globals at initialization [eva] computing for function f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37. + Called from TESTS/pdg/variadic.c:37. [eva] computing for function lib_f <- f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23. -[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: + Called from TESTS/pdg/variadic.c:23. +[kernel:annot:missing-spec] TESTS/pdg/variadic.c:23: Warning: Neither code nor specification for function lib_f, generating default assigns from the prototype [eva] using specification for function lib_f [eva] Done for function lib_f [eva] Recording results for f1 [eva] Done for function f1 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38. + Called from TESTS/pdg/variadic.c:38. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 [eva] computing for function f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39. + Called from TESTS/pdg/variadic.c:39. [eva] computing for function lib_f <- f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31. + Called from TESTS/pdg/variadic.c:31. [eva] Done for function lib_f [eva] Recording results for f3 [eva] Done for function f3 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40. + Called from TESTS/pdg/variadic.c:40. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 diff --git a/tests/slicing/oracle/variadic.3.res.oracle b/tests/slicing/oracle/variadic.3.res.oracle index e4cedf8c754b3f10ec4e5f6cfc1338731d477c1e..7b22f34440daf377e078fb29d668652f23fdda5b 100644 --- a/tests/slicing/oracle/variadic.3.res.oracle +++ b/tests/slicing/oracle/variadic.3.res.oracle @@ -6,33 +6,33 @@ [eva:initial-state] Values of globals at initialization [eva] computing for function f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37. + Called from TESTS/pdg/variadic.c:37. [eva] computing for function lib_f <- f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23. -[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: + Called from TESTS/pdg/variadic.c:23. +[kernel:annot:missing-spec] TESTS/pdg/variadic.c:23: Warning: Neither code nor specification for function lib_f, generating default assigns from the prototype [eva] using specification for function lib_f [eva] Done for function lib_f [eva] Recording results for f1 [eva] Done for function f1 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38. + Called from TESTS/pdg/variadic.c:38. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 [eva] computing for function f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39. + Called from TESTS/pdg/variadic.c:39. [eva] computing for function lib_f <- f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31. + Called from TESTS/pdg/variadic.c:31. [eva] Done for function lib_f [eva] Recording results for f3 [eva] Done for function f3 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40. + Called from TESTS/pdg/variadic.c:40. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 diff --git a/tests/slicing/oracle/variadic.4.res.oracle b/tests/slicing/oracle/variadic.4.res.oracle index e4cedf8c754b3f10ec4e5f6cfc1338731d477c1e..7b22f34440daf377e078fb29d668652f23fdda5b 100644 --- a/tests/slicing/oracle/variadic.4.res.oracle +++ b/tests/slicing/oracle/variadic.4.res.oracle @@ -6,33 +6,33 @@ [eva:initial-state] Values of globals at initialization [eva] computing for function f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37. + Called from TESTS/pdg/variadic.c:37. [eva] computing for function lib_f <- f1 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23. -[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: + Called from TESTS/pdg/variadic.c:23. +[kernel:annot:missing-spec] TESTS/pdg/variadic.c:23: Warning: Neither code nor specification for function lib_f, generating default assigns from the prototype [eva] using specification for function lib_f [eva] Done for function lib_f [eva] Recording results for f1 [eva] Done for function f1 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38. + Called from TESTS/pdg/variadic.c:38. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 [eva] computing for function f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39. + Called from TESTS/pdg/variadic.c:39. [eva] computing for function lib_f <- f3 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31. + Called from TESTS/pdg/variadic.c:31. [eva] Done for function lib_f [eva] Recording results for f3 [eva] Done for function f3 [eva] computing for function f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40. + Called from TESTS/pdg/variadic.c:40. [eva] computing for function lib_f <- f2 <- main. - Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27. + Called from TESTS/pdg/variadic.c:27. [eva] Done for function lib_f [eva] Recording results for f2 [eva] Done for function f2 diff --git a/tests/slicing/variadic.c b/tests/slicing/variadic.c index 440eff0a6cebfe57b5f5a53c5bcc0bb00048bdf3..6aa73a66ef0981906fae62da5f166511139d9155 100644 --- a/tests/slicing/variadic.c +++ b/tests/slicing/variadic.c @@ -1,10 +1,10 @@ /* run.config DEPS: ../../pdg/variadic.c - STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print" - STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print" - STDOPT: +"-slice-return f3 -journal-disable -then-on 'Slicing export' -print" - STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -print" - STDOPT: +"-slice-return main -slicing-level 3 -journal-disable -then-on 'Slicing export' -print" + STDOPT: +"-add-symbolic-path TESTS:../.. -slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print" + STDOPT: +"-add-symbolic-path TESTS:../.. -slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print" + STDOPT: +"-add-symbolic-path TESTS:../.. -slice-return f3 -journal-disable -then-on 'Slicing export' -print" + STDOPT: +"-add-symbolic-path TESTS:../.. -slice-return main -journal-disable -then-on 'Slicing export' -print" + STDOPT: +"-add-symbolic-path TESTS:../.. -slice-return main -slicing-level 3 -journal-disable -then-on 'Slicing export' -print" */ #include "../../pdg/variadic.c"