From 9cc260b15cc8675a81192593d61b5c11584f2ec9 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 17 Jan 2019 19:25:53 +0100
Subject: [PATCH] [fc-script] add command for running ./configure
---
bin/frama-c-script | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/bin/frama-c-script b/bin/frama-c-script
index b797957eeb5..e5662b42c11 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -59,6 +59,13 @@ if [ $# -lt 1 ]; then
echo " Monitors and summarizes multiple analyses dispatched by a Makefile"
echo " in the current PWD."
echo " Use $0 summary --help for more informations."
+ echo ""
+ echo " - configure <machdep>"
+ echo " Runs an existing configure script to only consider files"
+ echo " in Frama-C's libc; this will hopefully disable non-essential"
+ echo " and non-POSIX external libraries."
+ echo " <machdep> is necessary to define a required preprocessor symbol"
+ echo " (run 'frama-c -machdep' help to get the list of machdeps)."
exit
fi
@@ -185,6 +192,16 @@ EOF
fi
}
+configure_for_frama_c() {
+ if [ "$#" -eq 0 ]; then
+ echo "error: 'configure' command requires a machdep";
+ exit 1
+ fi
+ MACHDEP="$(echo $1 | tr a-z A-Z)"
+ echo $MACHDEP
+ CPP="gcc -E -nostdinc -fno-builtin -I${FRAMAC_SHARE}/libc -D__FC_MACHDEP_${MACHDEP}" ./configure
+}
+
case "$command" in
"make-template")
shift;
@@ -210,6 +227,10 @@ case "$command" in
shift;
${FRAMAC_SHARE}/analysis-scripts/summary.py "$@";
;;
+ "configure")
+ shift;
+ configure_for_frama_c "$@";
+ ;;
*)
echo "error: unrecognized command: $command"
esac
--
GitLab