From ce08950f1e4fe7b30bfccf12bfda4b5c3bd03db5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr> Date: Tue, 29 Sep 2020 12:38:46 +0200 Subject: [PATCH] [TESTS] use add-symbolic-path for a tests Could be done automatically in ptests --- tests/slicing/oracle/variadic.0.res.oracle | 18 +++++++++--------- tests/slicing/oracle/variadic.1.res.oracle | 18 +++++++++--------- tests/slicing/oracle/variadic.2.res.oracle | 18 +++++++++--------- tests/slicing/oracle/variadic.3.res.oracle | 18 +++++++++--------- tests/slicing/oracle/variadic.4.res.oracle | 18 +++++++++--------- tests/slicing/variadic.c | 10 +++++----- 6 files changed, 50 insertions(+), 50 deletions(-) diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle index 5db81403d65..601275105a3 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 d7485ec33c9..3c686905b1f 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 9e85774a6e5..9b5a8a3007b 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 e4cedf8c754..7b22f34440d 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 e4cedf8c754..7b22f34440d 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 440eff0a6ce..6aa73a66ef0 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" -- GitLab