From 2c88a55a2284c81376d44213768a8cbbf5509b8d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Sat, 1 May 2021 00:14:03 +0200
Subject: [PATCH] [tests] ensure oracle compatibility with macOS
---
tests/fc_script/make-wrapper.c | 4 ++--
tests/fc_script/oracle/make-wrapper.res | 9 ---------
2 files changed, 2 insertions(+), 11 deletions(-)
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c
index b52d6c74e87..ff8453e32a8 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 8370fe5e494..30db8dfd928 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...
--
GitLab