diff --git a/x509-parser/.frama-c/GNUmakefile b/x509-parser/.frama-c/GNUmakefile
index f928199fa2ba487f7cfd25892f0ae2d31d52e83b..c26544af9cd67db6b78ffe1323138abf02cc0c67 100644
--- a/x509-parser/.frama-c/GNUmakefile
+++ b/x509-parser/.frama-c/GNUmakefile
@@ -37,6 +37,32 @@ TARGETS = x509-parser.eva
 x509-parser.parse: \
   ../src/x509-parser.c \
 
+## The following E-ACSL target relies on some errors deliberately introduced
+## in the code, and triggered at runtime. Note that, depending on your
+## configuration, the execution of the non-instrumented code may terminate
+## succesfully, without any indication that a buffer overflow took place.
+eacsl: ../x509-parser.stack.exe ../x509-parser.heap.exe
+
+EACSL_FLAGS = \
+  -M \
+  --rte=mem \
+  -F "-no-annot" \
+  -F "-rte-verbose 0 -variadic-verbose 0" \
+  -c \
+  -E -D__FC_EACSL__ \
+
+EACSL_SCRIPT:=$(shell dirname $(shell which $(FRAMAC)))/e-acsl-gcc.sh
+
+../x509-parser.stack.exe: ../src/x509-parser.c ../src/main.c
+	$(EACSL_SCRIPT) $(EACSL_FLAGS) \
+	-E -DEACSL_STACK_OVERFLOW \
+	$^ -O $@ -o x509-parser.stack.frama.c
+
+../x509-parser.heap.exe: ../src/x509-parser.c ../src/main.c
+	$(EACSL_SCRIPT) $(EACSL_FLAGS) \
+	-E -DEACSL_HEAP_OVERFLOW \
+	$^ -O $@ -o x509-parser.stack.frama.c
+
 ### Epilogue. Do not modify this block. #######################################
 include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################
diff --git a/x509-parser/.gitignore b/x509-parser/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..15d8a19dae35c25a61faf5e72d59c0aa9673580c
--- /dev/null
+++ b/x509-parser/.gitignore
@@ -0,0 +1,5 @@
+*.exe
+*.exe.e-acsl
+# it would be useful to store the instrumented source, but each version
+# has over 70k lines and 3.5 MB, so for now we ignore them
+.frama-c/*.frama.c
diff --git a/x509-parser/google.com.der b/x509-parser/google.com.der
new file mode 100644
index 0000000000000000000000000000000000000000..9a24d4afe0afc83d0c8ca2b227a587de66ed7fb3
Binary files /dev/null and b/x509-parser/google.com.der differ
diff --git a/x509-parser/src/main.c b/x509-parser/src/main.c
index c1ec0cabd8f425591f882a663d8d19236bcab94c..ef7958c56a9b0ad92f6e9a7f01a1a10cb5496190 100644
--- a/x509-parser/src/main.c
+++ b/x509-parser/src/main.c
@@ -23,7 +23,21 @@ static void usage(char *argv0)
 
 int main(int argc, char *argv[])
 {
+  // To illustrate E-ACSL on this code, we deliberately change the buffer
+  // declaration to introduce errors during execution
+#ifndef __FC_EACSL__
+	// Original (bug-free) declaration
 	u8 buf[ASN1_MAX_BUFFER_SIZE];
+#else
+# ifdef EACSL_STACK_OVERFLOW
+	// Buffer size too small: a stack overflow will happen
+	u8 buf[ASN1_MAX_BUFFER_SIZE/64];
+# endif
+# ifdef EACSL_HEAP_OVERFLOW
+	// Buffer size too small: a heap overflow will happen
+	u8 *buf = malloc(sizeof(u8) * ASN1_MAX_BUFFER_SIZE/64);
+# endif
+#endif
 	off_t pos, offset = 0;
 	char *path = argv[1];
 	u16 rem, copied, eaten;
diff --git a/x509-parser/src/x509-parser.c b/x509-parser/src/x509-parser.c
index f5542e95f09eaea4bcebe9caa137237fbe8b9f30..c3e71471c6f4c20601b2db6b2c5cf0e8add084f0 100644
--- a/x509-parser/src/x509-parser.c
+++ b/x509-parser/src/x509-parser.c
@@ -9222,7 +9222,7 @@ out:
 	return ret;
 }
 
-#if defined(__FRAMAC__)
+#if defined(__FRAMAC__) && !defined(__FC_EACSL__)
 
 /* This dummy main allows testing */