diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c index b52d6c74e87425c96857b0e0bedbcc77f6085f7e..ff8453e32a8f53fa964378522ca13e4b7f822604 100644 --- a/tests/fc_script/make-wrapper.c +++ b/tests/fc_script/make-wrapper.c @@ -1,7 +1,7 @@ /* run.config NOFRAMAC: testing frama-c-script - COMMENT: we must filter 'make:' output lines, since they differ when run by the CI (e.g. mention to jobserver) - EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -e "s:$PWD:PWD:g" | grep -v "^make.*" | grep -v "recipe for target.*failed" > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva + COMMENT: we must filter 'make:'/'gmake:' output lines, since they differ when run by the CI (e.g. mention to jobserver) + EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -E -e "s:$PWD:PWD:g;/^(real|user|sys)/d;" | grep -E -v "^g?make.*" | grep -v "recipe for target.*failed" | grep -v '^$' > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva */ int defined(int a); diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res index 8370fe5e49498ce18397bc847647adac6ce49eaf..30db8dfd928cbfe5194bba8de7cbadd796f82029 100644 --- a/tests/fc_script/oracle/make-wrapper.res +++ b/tests/fc_script/oracle/make-wrapper.res @@ -1,11 +1,7 @@ - Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -cpp-extra-args= make-wrapper.c make-wrapper2.c - [kernel] Parsing make-wrapper.c (with preprocessing) [kernel] Parsing make-wrapper2.c (with preprocessing) - Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort - [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed @@ -28,19 +24,14 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war [eva] Clean up and save partial results. [kernel] Frama-C aborted: invalid user input. [kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'. - ***** make-wrapper recommendations ***** - *** recommendation #1 *** - 1. Found recursive call at: stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:14 <- large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:18 <- rec :: make-wrapper.c:23 <- main - Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis. - *** recommendation #2 *** 2. Found function with missing spec: large_name_to_force_line_break_in_stack_msg Looking for files defining it...