From 16f6cd0745e7a24d3099cfaab348eac5150767df Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 21 Oct 2019 11:55:39 +0200
Subject: [PATCH] [Doc] add caveat about libc in Eva
---
doc/value/main.tex | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 1ce3608b29a..a2213900579 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
--
GitLab