diff --git a/Makefile b/Makefile
index 575f86687700f288466ef6356fbe8af78855616b..72ccb1c8b3f0fa89316f53cebc6b93893fb7b13e 100644
--- a/Makefile
+++ b/Makefile
@@ -173,7 +173,7 @@ OPT_LIBS+= $(GEN_OPT_LIBS)
 ICONS:= $(addprefix share/, \
 		frama-c.ico frama-c.gif unmark.png )
 
-FEEDBACK_ICONS:= $(addprefix share/feedback/, \
+FEEDBACK_ICONS_NAMES:= \
 		never_tried.png \
 		unknown.png \
 		surely_valid.png \
@@ -186,7 +186,12 @@ FEEDBACK_ICONS:= $(addprefix share/feedback/, \
 		valid_but_dead.png \
 		inconsistent.png \
 		switch-on.png \
-		switch-off.png )
+		switch-off.png
+
+FEEDBACK_ICONS_DEFAULT:= \
+	$(addprefix share/theme/default/, $(FEEDBACK_ICONS_NAMES))
+FEEDBACK_ICONS_COLORBLIND:= \
+	$(addprefix share/theme/colorblind/, $(FEEDBACK_ICONS_NAMES))
 
 ROOT_LIBC_DIR:= share/libc
 LIBC_SUBDIRS:= . sys netinet linux net arpa
@@ -245,7 +250,7 @@ DISTRIB_FILES:= cil/*/*.ml* cil/*/*.in        				\
 	  $(wildcard $(CIL_PATH)/*/*.ml*))                              \
       bin/*2*.sh							\
       share/frama-c.WIN32.rc share/frama-c.Unix.rc                      \
-      $(ICONS) $(FEEDBACK_ICONS)			 		\
+      $(ICONS) $(FEEDBACK_ICONS_DEFAULT) $(FEEDBACK_ICONS_COLORBLIND)	\
       man/frama-c.1 doc/manuals/*.pdf doc/README			\
       doc/code/docgen_*.ml						\
       doc/code/*.css doc/code/intro_plugin.txt				\
@@ -1943,7 +1948,8 @@ install::
 	$(MKDIR) $(BINDIR)
 	$(MKDIR) $(MANDIR)/man1
 	$(MKDIR) $(FRAMAC_PLUGINDIR)/gui
-	$(MKDIR) $(FRAMAC_DATADIR)/feedback
+	$(MKDIR) $(FRAMAC_DATADIR)/theme/default
+	$(MKDIR) $(FRAMAC_DATADIR)/theme/colorblind
 	$(MKDIR) $(FRAMAC_DATADIR)/libc/sys
 	$(MKDIR) $(FRAMAC_DATADIR)/libc/netinet
 	$(MKDIR) $(FRAMAC_DATADIR)/libc/linux
@@ -1957,7 +1963,8 @@ install::
           share/configure.ac \
 	  $(FRAMAC_DATADIR)
 	$(CP) share/frama-c.rc $(ICONS) $(FRAMAC_DATADIR)
-	$(CP) $(FEEDBACK_ICONS) $(FRAMAC_DATADIR)/feedback
+	$(CP) $(FEEDBACK_ICONS_DEFAULT) $(FRAMAC_DATADIR)/theme/default
+	$(CP) $(FEEDBACK_ICONS_COLORBLIND) $(FRAMAC_DATADIR)/theme/colorblind
 	if [ -d $(EMACS_DATADIR) ]; then \
 	  $(CP) share/acsl.el $(EMACS_DATADIR); \
 	fi
@@ -2164,7 +2171,8 @@ NO_CHECK_HEADERS=tests/*/* doc/manuals/*.pdf \
 		 src/wp/Changelog \
 		 .force-reconfigure \
 		 licenses/* VERSION INSTALL bin/sed* \
-		 share/Makefile.kernel $(ICONS) $(FEEDBACK_ICONS) \
+		 share/Makefile.kernel $(ICONS) $(FEEDBACK_ICONS_DEFAULT) \
+		 $(FEEDBACK_ICONS_COLORBLIND) \
 		 INSTALL_WITH_WHY
 
 .PHONY: check-headers check-headers-xunit
diff --git a/share/theme/colorblind/considered_valid.png b/share/theme/colorblind/considered_valid.png
new file mode 100644
index 0000000000000000000000000000000000000000..41578e0e42bb6ed7d40b8769cfbfe88ff4f04e67
Binary files /dev/null and b/share/theme/colorblind/considered_valid.png differ
diff --git a/share/theme/colorblind/inconsistent.png b/share/theme/colorblind/inconsistent.png
new file mode 100644
index 0000000000000000000000000000000000000000..63cfa07881e918b91ce27cb603025edaeebe2d11
Binary files /dev/null and b/share/theme/colorblind/inconsistent.png differ
diff --git a/share/theme/colorblind/invalid_but_dead.png b/share/theme/colorblind/invalid_but_dead.png
new file mode 100644
index 0000000000000000000000000000000000000000..1bf92e1283e21a08e1a069e593ac03954934d8fe
Binary files /dev/null and b/share/theme/colorblind/invalid_but_dead.png differ
diff --git a/share/theme/colorblind/invalid_under_hyp.png b/share/theme/colorblind/invalid_under_hyp.png
new file mode 100644
index 0000000000000000000000000000000000000000..29d02bb877dfbf75aba36e0f573ddf09a35d2865
Binary files /dev/null and b/share/theme/colorblind/invalid_under_hyp.png differ
diff --git a/share/theme/colorblind/never_tried.png b/share/theme/colorblind/never_tried.png
new file mode 100644
index 0000000000000000000000000000000000000000..7e070040e705574cce349d38b47fd21f0b6dfcf8
Binary files /dev/null and b/share/theme/colorblind/never_tried.png differ
diff --git a/share/theme/colorblind/surely_invalid.png b/share/theme/colorblind/surely_invalid.png
new file mode 100644
index 0000000000000000000000000000000000000000..b3d637ec8130cdedd975668e4e031e123ce35fae
Binary files /dev/null and b/share/theme/colorblind/surely_invalid.png differ
diff --git a/share/theme/colorblind/surely_valid.png b/share/theme/colorblind/surely_valid.png
new file mode 100644
index 0000000000000000000000000000000000000000..ed73864251689f7a1e11424702c0ccdb84c4969b
Binary files /dev/null and b/share/theme/colorblind/surely_valid.png differ
diff --git a/share/feedback/switch-off.png b/share/theme/colorblind/switch-off.png
similarity index 100%
rename from share/feedback/switch-off.png
rename to share/theme/colorblind/switch-off.png
diff --git a/share/feedback/switch-on.png b/share/theme/colorblind/switch-on.png
similarity index 100%
rename from share/feedback/switch-on.png
rename to share/theme/colorblind/switch-on.png
diff --git a/share/theme/colorblind/unknown.png b/share/theme/colorblind/unknown.png
new file mode 100644
index 0000000000000000000000000000000000000000..6fb957943cf2e134edd4fe419f0ebe30b6fe3f8f
Binary files /dev/null and b/share/theme/colorblind/unknown.png differ
diff --git a/share/theme/colorblind/unknown_but_dead.png b/share/theme/colorblind/unknown_but_dead.png
new file mode 100644
index 0000000000000000000000000000000000000000..b431c812a668656e342695aa8e7f48d14b2e3144
Binary files /dev/null and b/share/theme/colorblind/unknown_but_dead.png differ
diff --git a/share/theme/colorblind/valid_but_dead.png b/share/theme/colorblind/valid_but_dead.png
new file mode 100644
index 0000000000000000000000000000000000000000..f5bb1bb44c7c81a4fefc996137de7ff019b5e9a4
Binary files /dev/null and b/share/theme/colorblind/valid_but_dead.png differ
diff --git a/share/theme/colorblind/valid_under_hyp.png b/share/theme/colorblind/valid_under_hyp.png
new file mode 100644
index 0000000000000000000000000000000000000000..0a2f61bcdc366577eb386f70cbd87b7446609e7a
Binary files /dev/null and b/share/theme/colorblind/valid_under_hyp.png differ
diff --git a/share/feedback/considered_valid.png b/share/theme/default/considered_valid.png
similarity index 100%
rename from share/feedback/considered_valid.png
rename to share/theme/default/considered_valid.png
diff --git a/share/feedback/inconsistent.png b/share/theme/default/inconsistent.png
similarity index 100%
rename from share/feedback/inconsistent.png
rename to share/theme/default/inconsistent.png
diff --git a/share/feedback/invalid_but_dead.png b/share/theme/default/invalid_but_dead.png
similarity index 100%
rename from share/feedback/invalid_but_dead.png
rename to share/theme/default/invalid_but_dead.png
diff --git a/share/feedback/invalid_under_hyp.png b/share/theme/default/invalid_under_hyp.png
similarity index 100%
rename from share/feedback/invalid_under_hyp.png
rename to share/theme/default/invalid_under_hyp.png
diff --git a/share/feedback/never_tried.png b/share/theme/default/never_tried.png
similarity index 100%
rename from share/feedback/never_tried.png
rename to share/theme/default/never_tried.png
diff --git a/share/feedback/surely_invalid.png b/share/theme/default/surely_invalid.png
similarity index 100%
rename from share/feedback/surely_invalid.png
rename to share/theme/default/surely_invalid.png
diff --git a/share/feedback/surely_valid.png b/share/theme/default/surely_valid.png
similarity index 100%
rename from share/feedback/surely_valid.png
rename to share/theme/default/surely_valid.png
diff --git a/share/theme/default/switch-off.png b/share/theme/default/switch-off.png
new file mode 100644
index 0000000000000000000000000000000000000000..c1e7cb811d5142a530117da7e832017c3ef42e36
Binary files /dev/null and b/share/theme/default/switch-off.png differ
diff --git a/share/theme/default/switch-on.png b/share/theme/default/switch-on.png
new file mode 100644
index 0000000000000000000000000000000000000000..2547a867ca4b1de4ece3ffcf2487f678c3bb81bf
Binary files /dev/null and b/share/theme/default/switch-on.png differ
diff --git a/share/feedback/unknown.png b/share/theme/default/unknown.png
similarity index 100%
rename from share/feedback/unknown.png
rename to share/theme/default/unknown.png
diff --git a/share/feedback/unknown_but_dead.png b/share/theme/default/unknown_but_dead.png
similarity index 100%
rename from share/feedback/unknown_but_dead.png
rename to share/theme/default/unknown_but_dead.png
diff --git a/share/feedback/valid_but_dead.png b/share/theme/default/valid_but_dead.png
similarity index 100%
rename from share/feedback/valid_but_dead.png
rename to share/theme/default/valid_but_dead.png
diff --git a/share/feedback/valid_under_hyp.png b/share/theme/default/valid_under_hyp.png
similarity index 100%
rename from share/feedback/valid_under_hyp.png
rename to share/theme/default/valid_under_hyp.png
diff --git a/src/gui/gtk_helper.ml b/src/gui/gtk_helper.ml
index a3720bd0bca2894f44612c8f42bda9455e2418bc..789623a016197dc1ca9faa8f5ba3679f96ba6ed2 100644
--- a/src/gui/gtk_helper.ml
+++ b/src/gui/gtk_helper.ml
@@ -58,23 +58,31 @@ module Icon = struct
 
   module F = Property_status.Feedback
 
+  type theme_file =
+  | ThemeSpecific of string
+  | ThemeGeneric of string
+
   let builtins =
-    [(Frama_C,"frama-c.ico");
-     (Unmark,"unmark.png");
-     (Feedback F.Never_tried,"feedback/never_tried.png");
-     (Feedback F.Unknown,"feedback/unknown.png");
-     (Feedback F.Valid,"feedback/surely_valid.png");
-     (Feedback F.Invalid,"feedback/surely_invalid.png");
-     (Feedback F.Considered_valid,"feedback/considered_valid.png");
-     (Feedback F.Valid_under_hyp,"feedback/valid_under_hyp.png");
-     (Feedback F.Invalid_under_hyp,"feedback/invalid_under_hyp.png");
-     (Feedback F.Invalid_but_dead,"feedback/invalid_but_dead.png");
-     (Feedback F.Unknown_but_dead,"feedback/unknown_but_dead.png");
-     (Feedback F.Valid_but_dead,"feedback/valid_but_dead.png");
-     (Feedback F.Inconsistent,"feedback/inconsistent.png");
+    [(Frama_C,                      ThemeGeneric "frama-c.ico");
+     (Unmark,                       ThemeGeneric "unmark.png");
+     (Feedback F.Never_tried,       ThemeSpecific "never_tried.png");
+     (Feedback F.Unknown,           ThemeSpecific "unknown.png");
+     (Feedback F.Valid,             ThemeSpecific "surely_valid.png");
+     (Feedback F.Invalid,           ThemeSpecific "surely_invalid.png");
+     (Feedback F.Considered_valid,  ThemeSpecific "considered_valid.png");
+     (Feedback F.Valid_under_hyp,   ThemeSpecific "valid_under_hyp.png");
+     (Feedback F.Invalid_under_hyp, ThemeSpecific "invalid_under_hyp.png");
+     (Feedback F.Invalid_but_dead,  ThemeSpecific "invalid_but_dead.png");
+     (Feedback F.Unknown_but_dead,  ThemeSpecific "unknown_but_dead.png");
+     (Feedback F.Valid_but_dead,    ThemeSpecific "valid_but_dead.png");
+     (Feedback F.Inconsistent,      ThemeSpecific "inconsistent.png");
     ]
 
-  type icon = Filename of string | Pixbuf of GdkPixbuf.pixbuf
+  let get_file_in_theme = function
+    | ThemeSpecific x -> "theme/" ^ (Gui_parameters.Theme.get()) ^ "/" ^ x
+    | ThemeGeneric x -> x
+
+  type icon = Filename of theme_file | Pixbuf of GdkPixbuf.pixbuf
 
   let h = Hashtbl.create 7
 
@@ -87,19 +95,21 @@ module Icon = struct
 
   let get k =
     try match Hashtbl.find h k with
-      | Filename f ->
-	  let p =
-	    try GdkPixbuf.from_file (Config.datadir ^ "/" ^ f)
-	    with Glib.GError _ ->
-              Gui_parameters.warning ~once:true
-		"Frama-C images not found. Is FRAMAC_SHARE correctly set?";
-	      default ()
-	  in
-	  Hashtbl.replace h k (Pixbuf p); p
+      | Filename f' ->
+	let f = get_file_in_theme f' in
+	let p =
+	  try GdkPixbuf.from_file (Config.datadir ^ "/" ^ f)
+	  with Glib.GError _ ->
+            Gui_parameters.warning ~once:true
+	      "Frama-C images not found. Is FRAMAC_SHARE correctly set?";
+	    default ()
+	in
+	Hashtbl.replace h k (Pixbuf p); p
       | Pixbuf p -> p
     with Not_found -> assert false
       
-  let register ~name ~file = Hashtbl.replace h (Custom name) (Filename file)
+  let register ~name ~file = Hashtbl.replace h (Custom name)
+    (Filename (ThemeGeneric file))
 
 end
 
diff --git a/src/gui/gui_parameters.ml b/src/gui/gui_parameters.ml
index c6e6f75cd9f02707e33c35858b927c3c598f53e8..adea7764a1ddb8bc4f333bc100b51843a9d414f9 100644
--- a/src/gui/gui_parameters.ml
+++ b/src/gui/gui_parameters.ml
@@ -47,6 +47,16 @@ module Undo =
       let help = "possible to click on the `undo' button (set by default)"
      end)
 
+module Theme =
+  String
+    (struct
+      let option_name = "-gui-theme"
+      let arg_name = "s"
+      let help =
+	"choose the theme <s> of the GUI (available: 'default', 'colorblind')"
+      let default = "default"
+     end)
+
 (*
 Local Variables:
 compile-command: "make -C ../.."
diff --git a/src/gui/gui_parameters.mli b/src/gui/gui_parameters.mli
index ae50e8b1c16255106f3ac165a2ff413ef110c0eb..36fffdbde442ed2050228b1fe711e30e9f66adfd 100644
--- a/src/gui/gui_parameters.mli
+++ b/src/gui/gui_parameters.mli
@@ -30,6 +30,9 @@ module Project_name: Parameter_sig.String
 module Undo: Parameter_sig.Bool
 (** Option -undo. *)
 
+module Theme: Parameter_sig.String
+(** Option -gui-theme. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../.."