diff --git a/doc/value/main.tex b/doc/value/main.tex
index 1ce3608b29a8fe3724a3ed8f62e4e49185fb76ae..a221390057992576d1a39bbb6e2d2fa99b6dddee 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -2269,6 +2269,14 @@ a library function is to write C code that models its behavior,
 so that its code is no longer missing from the point of view of the
 analyzer.
 
+Frama-C provides a set of specifications for the most common functions in the C
+standard library and for some POSIX functions, plus a few extensions
+(BSD, GNU, etc.). These specifications allow the analysis of applications which
+use these libraries, but they become part of the {\em trusted computing base}:
+it is the responsibility of the user to verify that these specifications are
+correct with respect to the actual standard library implementation from the
+actual execution environment.
+
 \subsection{Choosing between complete and partial application mode}
 
 This section uses a small example to illustrate the pitfalls that should