diff --git a/bin/frama-c-script b/bin/frama-c-script index 022f9b140965db5b7d07cff1ccfba1ff712386b2..a85fadf00fe3f4adbdc6816b343ad0e2b3056f6e 100755 --- a/bin/frama-c-script +++ b/bin/frama-c-script @@ -37,6 +37,11 @@ usage() { echo " and non-POSIX external libraries." echo " (run 'frama-c -machdep help' to get the list of machdeps)." echo "" + echo " - creduce <args>" + echo " Use the external tool C-Reduce to minimize C files when" + echo " debugging crashes and fatal errors. Run without arguments for" + echo " more details." + echo "" echo " - estimate-difficulty file..." echo " Applies several heuristics to try and estimate the difficulty" echo " of analyzing the specified files with Frama-C." @@ -259,6 +264,10 @@ case "$command" in shift; "${FRAMAC_SHARE}"/analysis-scripts/normalize_jcdb.py "$@"; ;; + "creduce") + shift; + ${FRAMAC_SHARE}/analysis-scripts/creduce.sh "$@"; + ;; *) echo "error: unrecognized command: $command"; exit 1