diff --git a/bin/frama-c-script b/bin/frama-c-script
index b797957eeb5db40710aaf6eb46af17c2ca03c0f0..e5662b42c117dddbb7b26fb64e871bd95236cf63 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