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

[tests] rewrite test sed filter in Python for better portability

parent 40c40cb3
No related branches found
No related tags found
No related merge requests found
...@@ -18,6 +18,7 @@ mk_tests { ...@@ -18,6 +18,7 @@ mk_tests {
@src/kernel_internals/parsing/tests/ptests @src/kernel_internals/parsing/tests/ptests
dune runtest -j1 --display short \ dune runtest -j1 --display short \
src/plugins/server/tests/batch \ src/plugins/server/tests/batch \
tests/fc_script tests/fc_script \
tests/syntax
''; '';
} }
/* run.config*
FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:[^ ]*[/]__fc_machdep.*\.dir:-ITMP_MACHDEP:g; s:$PWD/::g; s:$(realpath @FRAMAC_SHARE@)/:FRAMAC_SHARE/:g; s:@PTEST_MAKE_DIR@/result@PTEST_CONFIG@/::g; s: -m32::; s: -m64::"
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
OPT: -machdep x86_32 -print-cpp-commands
OPT: -cpp-extra-args-per-file=@PTEST_FILE@:"-DPF=\\\"cp%02d_%.3f\\\"" -cpp-extra-args="-DPF2=\\\"cp%02d_%.3f\\\"" -no-autoload-plugins @PTEST_FILE@ -print
OPT: -cpp-extra-args-per-file=@PTEST_FILE@:"file_extra" -cpp-extra-args="global_extra" -cpp-command "echo 'extra_args: %args'" -no-autoload-plugins @PTEST_FILE@ -print
*/
#include <stdio.h>
void printer(int i, float f) {
printf(PF, i, f);
}
int main() {
printer(1, 1.0);
}
#include <stdio.h>
void printer(int i, float f) {
printf(PF, i, f);
}
int main() {
printer(1, 1.0);
}
#!/usr/bin/env python3
""" Filter for the cpp-command test. Expects $FRAMAC_SHARE as its first argument. """
import re
import sys
FRAMAC_SHARE = sys.argv[1]
for line in sys.stdin:
# Apply several filters:
# - Remove preprocessed filename (randomly generated)
line = re.sub(r"/[^ ]*cpp-command.c......\.i", "<TMPDIR/PP>.i", line)
# - Remove hardcoded path to temporary __fc_machdepXXXXXX.dir
line = re.sub(r"-I.*__fc_machdep......\.dir", "-I<TMP_MACHDEP>", line)
# - Replace occurrence of FRAMAC_SHARE; re.escape is needed if the path
# contains e.g. a '+' character
line = re.sub(re.escape(f"-I{FRAMAC_SHARE}"), "-I<FRAMAC_SHARE>", line)
# Remove spurious '-m32' and '-m64', which are architecture-dependent
line = re.sub("-m32", "", line)
line = re.sub("-m64", "", line)
print(line.strip())
$ FRAMAC_SHARE="$(frama-c-config -print-share-path)"
$ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']" | python3 filter.py "$FRAMAC_SHARE"
[kernel] Parsing cpp-command.c (with preprocessing)
[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [<TMPDIR/PP>.i <TMPDIR/PP>.i <TMPDIR/PP>.i <TMPDIR/PP>.i] [-I<TMP_MACHDEP> -I<FRAMAC_SHARE>/libc -D__FRAMAC__ -dD -nostdinc]
$ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'" | python3 filter.py "$FRAMAC_SHARE"
[kernel] Parsing cpp-command.c (with preprocessing)
%1 = cpp-command.c %2 = <TMPDIR/PP>.i %args = -I<TMP_MACHDEP> -I<FRAMAC_SHARE>/libc -D__FRAMAC__ -dD -nostdinc
$ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
[kernel] Parsing cpp-command.c (with preprocessing)
using \% has no effect : cpp-command.c'
$ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder" | python3 filter.py "$FRAMAC_SHARE"
[kernel] Parsing cpp-command.c (with preprocessing)
%var is not an interpreted placeholder
$ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -print-cpp-commands | python3 filter.py "$FRAMAC_SHARE"
[kernel] Preprocessing command:
gcc -E -C -I<TMP_MACHDEP> -I<FRAMAC_SHARE>/libc -D__FRAMAC__ -dD -nostdinc -Wno-builtin-macro-redefined -Wno-unknown-warning-option '$TESTCASE_ROOT/cpp-command.c' -o '<TMPDIR/PP>.i'
$ frama-c -check -no-autoload-plugins cpp-command.c -cpp-extra-args-per-file=cpp-command.c:"-DPF=\\\"cp%02d_%.3f\\\"" -cpp-extra-args="-DPF2=\\\"cp%02d_%.3f\\\"" -print | python3 filter.py "$FRAMAC_SHARE"
[kernel] Parsing cpp-command.c (with preprocessing)
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
void printer(int i, float f)
{
printf("cp%02d_%.3f",i,(double)f);
return;
}
int main(void)
{
int __retres;
printer(1,(float)1.0);
__retres = 0;
return __retres;
}
$ frama-c -check -no-autoload-plugins cpp-command.c -cpp-extra-args-per-file=cpp-command.c:"file_extra" -cpp-extra-args="global_extra" -cpp-command "echo 'extra_args: %args'" -print | python3 filter.py "$FRAMAC_SHARE"
[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Warning: your preprocessor is not known to handle option `-dD'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing cpp-command.c (with preprocessing)
extra_args: -I<TMP_MACHDEP> -I<FRAMAC_SHARE>/libc -D__FRAMAC__ -dD -nostdinc file_extra global_extra
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
/* Generated by Frama-C */
(cram
(applies_to cpp-command)
(enabled_if %{read:../../python-3.7-available})
)
[kernel] Parsing cpp-command.c (with preprocessing)
[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc]
[kernel] Parsing cpp-command.c (with preprocessing)
%1 = cpp-command.c %2 = TMPDIR/FILE.i %args = -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc
[kernel] Parsing cpp-command.c (with preprocessing)
using \% has no effect : cpp-command.c'
[kernel] Parsing cpp-command.c (with preprocessing)
%var is not an interpreted placeholder
[kernel] Preprocessing command:
gcc -E -C -I. -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc -Wno-builtin-macro-redefined -Wno-unknown-warning-option 'cpp-command.c' -o 'TMPDIR/FILE.i'
[kernel] Parsing cpp-command.c (with preprocessing)
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
void printer(int i, float f)
{
printf("cp%02d_%.3f",i,(double)f);
return;
}
int main(void)
{
int __retres;
printer(1,(float)1.0);
__retres = 0;
return __retres;
}
[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Warning: your preprocessor is not known to handle option `-dD'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing cpp-command.c (with preprocessing)
extra_args: -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc file_extra global_extra
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
/* Generated by Frama-C */
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