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

[tests] ensure oracle compatibility with macOS

parent 49f1a1b1
No related branches found
No related tags found
No related merge requests found
/* run.config /* run.config
NOFRAMAC: testing frama-c-script 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) 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 "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 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); int defined(int a);
......
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 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-wrapper.c (with preprocessing)
[kernel] Parsing make-wrapper2.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 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] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
...@@ -28,19 +24,14 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war ...@@ -28,19 +24,14 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
[eva] Clean up and save partial results. [eva] Clean up and save partial results.
[kernel] Frama-C aborted: invalid user input. [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'. [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 ***** ***** make-wrapper recommendations *****
*** recommendation #1 *** *** recommendation #1 ***
1. Found recursive call at: 1. Found recursive call at:
stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:14 <- 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 <- large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:18 <-
rec :: make-wrapper.c:23 <- rec :: make-wrapper.c:23 <-
main main
Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis. Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis.
*** recommendation #2 *** *** recommendation #2 ***
2. Found function with missing spec: large_name_to_force_line_break_in_stack_msg 2. Found function with missing spec: large_name_to_force_line_break_in_stack_msg
Looking for files defining it... Looking for files defining it...
......
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