diff --git a/share/autocomplete_frama-c b/share/autocomplete_frama-c
index 4ddb075dae72610948da687b1db75983d105dfd3..423c17506bf553560fc19a589a1132391a277883 100644
--- a/share/autocomplete_frama-c
+++ b/share/autocomplete_frama-c
@@ -31,6 +31,9 @@
 # If you want to enable Frama-C completion only for your account, append
 # this file to ~/.bash_completion.
 #
+# For a less verbose completion for options with comma-separated values,
+# put "set show-all-if-ambiguous on" in your "~/.inputrc".
+#
 # Assuming frama-c is in your PATH,
 # you can also put the following line into your .bashrc:
 #
@@ -38,39 +41,109 @@
 #
 # -----------------------------------------------------------------------------
 
+# Remove the colon from the list of completion word break characters
+COMP_WORDBREAKS=${COMP_WORDBREAKS//:}
+
 _frama-c ()
 {
   local cur
 
   local basic_options
   local sub_options
+  local advance_options
 
   COMPREPLY=()   # Array variable storing the possible completions.
   local sub_comp_line="${COMP_LINE[@]:0:(${COMP_POINT})}"
   local sub_comp_set=( $sub_comp_line )
 
-  if [[ ${sub_comp_line: -1} == ' ' ]] ; then
+  compopt +o default
+
+  if [[ ${sub_comp_line: -1} == ' ' ]]
+  then
       cur=""
   else
       cur="${sub_comp_set[@]: -1}"
   fi
 
-  # Generate the completion matches and load them into $COMPREPLY array.
-   case "$cur" in
-       -*-*)
-	   sub_option="$(frama-c -autocomplete | grep -E -o " $cur[^*]+" |sort |uniq)";
-	   COMPREPLY=( $( compgen -W "${sub_option}"  -- $cur ) );;
-      
-       -*)
-	   basic_options="$(frama-c -autocomplete | grep -E -o " \-[^-]+-?" |sort |uniq)" 
-  	   COMPREPLY=( $( compgen -W  "${basic_options}" -- $cur ) );;
-   esac
+
+  # Generate the completion matches for -wp-msg-key and load them into $COMPREPLY array.
+  # Generate the completion matches for -kernel-msg-key and load them into $COMPREPLY array.
+  if [[ "${COMP_WORDS[COMP_CWORD -1]}" == "-wp-msg-key" ]] || [[ "${COMP_WORDS[COMP_CWORD -1]}" == "-kernel-msg-key" ]]
+  then
+      # https://github.com/scop/bash-completion/issues/240
+      local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*},"
+      advance_options="$(frama-c ${COMP_WORDS[COMP_CWORD -1]} help | grep -E -o "    [^*]+" |sort |uniq)"
+
+      # Solution from: https://github.com/scop/bash-completion/commit/021058b38ad7279c33ffbaa36d73041d607385ba
+      # But, if show-all-if-ambiguous is set to off completion for options with comma-separated values loses its prefix:
+      # https://github.com/scop/bash-completion/issues/240.
+      # So we have two ways for completion, depending on the value of show-all-if-ambiguous
+      local ambigous="$(bind -v | grep show-all-if-ambiguous)"
+      ambigous="${ambigous##* }"
+      if [[ "$ambigous" == "on" ]]
+      then
+	  COMPREPLY=( $( compgen -W "${advance_options}" -- "${cur##*,}" ) )
+	  [[ ${#COMPREPLY[@]} -eq 1 ]] && COMPREPLY=( ${COMPREPLY/#/$prefix} )
+      else
+	  COMPREPLY=( $( compgen -P "$prefix" -W "${advance_options}" -- "${cur##*,}" ) )
+      fi
+
+
+  # Generate the completion matches for -wp-prover and load them into $COMPREPLY array.
+  elif [[ "${COMP_WORDS[COMP_CWORD -1]}" == "-wp-prover" ]]
+  then
+      local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*},"
+      advance_options="$(frama-c -wp-detect | grep -E -o " \[.*" | grep -E -o "[^][|]*")"
+      advance_options+=" none script tip native:alt-ergo native:coq native:coqide"
+      local ambigous="$(bind -v | grep show-all-if-ambiguous)"
+      ambigous="${ambigous##* }"
+      if [[ "$ambigous" == "on" ]]
+      then
+	  COMPREPLY=( $( compgen -W "${advance_options}" -- "${cur##*,}" ) )
+	  [[ ${#COMPREPLY[@]} -eq 1 ]] && COMPREPLY=( ${COMPREPLY/#/$prefix} )
+      else
+	  COMPREPLY=( $( compgen -P "$prefix" -W "${advance_options}" -- "${cur##*,}" ) )
+      fi
+
+
+  # Generate the completion matches for -kernel-warn-key and load them into $COMPREPLY array.
+  elif [[ "${COMP_WORDS[COMP_CWORD -1]}" == "-kernel-warn-key" ]]
+  then
+      local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*},"
+      advance_options="$(frama-c -kernel-warn-key help | grep -E -o "    [^*]+[^:] ")"
+
+      local ambigous="$(bind -v | grep show-all-if-ambiguous)"
+      ambigous="${ambigous##* }"
+      if [[ "$ambigous" == "on" ]]
+      then
+	  COMPREPLY=( $( compgen -W "${advance_options}" -- "${cur##*,}" ) )
+	  [[ ${#COMPREPLY[@]} -eq 1 ]] && COMPREPLY=( ${COMPREPLY/#/$prefix} )
+      else
+	  COMPREPLY=( $( compgen -P "$prefix" -W "${advance_options}" -- "${cur##*,}" ) )
+      fi
+
+
+  # Generate the completion matches for -* and load them into $COMPREPLY array.
+  else
+      case "$cur" in
+	  -*-*)
+	      sub_option="$(frama-c -autocomplete | grep -E -o " $cur[^*]+" |sort |uniq)";
+	      COMPREPLY=( $( compgen -W "${sub_option}"  -- $cur ) );;
+
+	  -*)
+	      basic_options="$(frama-c -autocomplete | grep -E -o " \-[^-]+-?" |sort |uniq)"
+  	      COMPREPLY=( $( compgen -W  "${basic_options}" -- $cur ) );;
+	  *)
+	      compopt -o default
+	      COMPREPLY=();;
+      esac
+  fi
 
   return 0
 }
 
-complete -o nospace -f -F _frama-c filename frama-c
-complete -o nospace -f -F _frama-c filename frama-c-gui
+complete -o nospace -F _frama-c frama-c
+complete -o nospace -F _frama-c frama-c-gui
 
 # Local Variables:
 # mode: sh