From 76b637eca195b2149fa8f6035dc3881eeba8a614 Mon Sep 17 00:00:00 2001
From: DavidCok <cok@frontiernet.net>
Date: Thu, 27 Sep 2018 13:37:53 +0200
Subject: [PATCH] Initial documentation
---
VERSION | 1 +
doc/userman/Makefile | 97 +++
doc/userman/biblio.bib | 154 +++++
doc/userman/cealistlogo.jpg | Bin 0 -> 17028 bytes
doc/userman/changes.tex | 16 +
doc/userman/description.tex | 1146 +++++++++++++++++++++++++++++++++
doc/userman/eacslversion.tex | 2 +
doc/userman/fclangversion.tex | 2 +
doc/userman/introduction.tex | 26 +
doc/userman/limitations.tex | 188 ++++++
doc/userman/macros.tex | 295 +++++++++
doc/userman/main.tex | 99 +++
12 files changed, 2026 insertions(+)
create mode 100644 VERSION
create mode 100644 doc/userman/Makefile
create mode 100644 doc/userman/biblio.bib
create mode 100644 doc/userman/cealistlogo.jpg
create mode 100644 doc/userman/changes.tex
create mode 100644 doc/userman/description.tex
create mode 100644 doc/userman/eacslversion.tex
create mode 100644 doc/userman/fclangversion.tex
create mode 100644 doc/userman/introduction.tex
create mode 100644 doc/userman/limitations.tex
create mode 100644 doc/userman/macros.tex
create mode 100644 doc/userman/main.tex
diff --git a/VERSION b/VERSION
new file mode 100644
index 00000000..c042c380
--- /dev/null
+++ b/VERSION
@@ -0,0 +1 @@
+Chlorine+
diff --git a/doc/userman/Makefile b/doc/userman/Makefile
new file mode 100644
index 00000000..197a040a
--- /dev/null
+++ b/doc/userman/Makefile
@@ -0,0 +1,97 @@
+MAIN=main
+
+C_CODE=$(wildcard examples/*.[ci])
+VERSION_FILE=../../../../../VERSION
+ifeq ("$(wildcard $(VERSION_FILE))", "")
+VERSION_FILE=../../VERSION
+FC_VERSION+=Chlorine+
+else
+#internal mode
+FC_VERSION=$(shell cat $(VERSION_FILE))
+endif
+FCLANG_VERSION= $(shell cat $(VERSION_FILE))
+
+DEPS_MODERN=fclangversion.tex biblio.bib macros.tex \
+ introduction.tex \
+ provides.tex \
+ limitations.tex \
+ changes.tex \
+ $(C_CODE) \
+ $(VERSION_FILE)
+
+default: main.pdf
+
+main.pdf: $(DEPS_MODERN)
+
+EACSL_DIR=../..
+DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
+install:
+ mkdir -p $(EACSL_DIR)/doc/manuals/
+ cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
+# cp -f main.pdf \
+ $(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
+
+include $(EACSL_DIR)/doc/support/MakeLaTeXModern
+
+fclangversion.tex: Makefile
+ rm -f $@
+ printf '\\newcommand{\\fclangversion}{$(FCLANG_VERSION)\\xspace}\n' > $@
+ printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
+ chmod a-w $@
+
+%.1: %.mp
+ mpost -interaction=batchmode $<
+
+%.mps: %.1
+ mv $< $@
+
+%.pp: %.tex pp
+ ./pp -utf8 $< > $@
+
+%.pp: %.c pp
+ ./pp -utf8 -c $< > $@
+
+%.tex: %.ctex pp
+ rm -f $@
+ ./pp $< > $@
+ chmod a-w $@
+
+%.bnf: %.tex transf
+ rm -f $@
+ ./transf $< > $@
+ chmod a-w $@
+
+%_modern.bnf: %.tex transf
+ rm -f $@
+ ./transf -modern $< > $@
+ chmod a-w $@
+
+%.ml: %.mll
+ ocamllex $<
+
+%.pdf: %.tex
+ pdflatex $*
+ makeindex $*
+ bibtex $*
+ pdflatex $*
+ pdflatex $*
+
+%.cmo: %.ml
+ ocamlc -c $<
+
+pp: pp.ml
+ ocamlopt -o $@ str.cmxa $^
+
+transf: transf.cmo transfmain.cmo
+ ocamlc -o $@ $^
+
+transfmain.cmo: transf.cmo
+
+.PHONY: clean
+
+clean:
+ rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
+ *.haux *.hbbl *.htoc \
+ *.cb* *.cm? *.bbl *.blg *.idx *.ind *.ilg \
+ transf trans.ml pp.ml pp
+ rm -f fclangversion.tex
diff --git a/doc/userman/biblio.bib b/doc/userman/biblio.bib
new file mode 100644
index 00000000..3a444b97
--- /dev/null
+++ b/doc/userman/biblio.bib
@@ -0,0 +1,154 @@
+@manual{userman,
+ title = {Frama-C User Manual},
+ author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
+ André Maroneze and Virgile Prevosto and
+ Armand Puccetti and Julien Signoles and
+ Boris Yakobowski},
+ note = {\url{http://frama-c.cea.fr/download/user-manual.pdf}}
+}
+
+@manual{plugin-dev-guide,
+ author = {Julien Signoles and Loïc Correnson and Matthieu Lemerre and
+ Virgile Prevosto},
+ title = {{Frama-C Plug-in Development Guide}},
+ note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
+}
+
+@manual{eva,
+ author = {David B\"uhler and Pascal Cuoq and Boris Yakobowski and
+ Matthieu Lemerre and André Maroneze and Valentin Perelle and
+ Virgile Prevosto},
+ title = {{EVA} -- The Evolved Value Analysis plug-in},
+ note = {\mbox{\url{http://frama-c.cea.fr/download/value-analysis.pdf}}},
+}
+
+@manual{acsl,
+ author = {Baudin, Patrick and Filli\^{a}tre, Jean-Christophe and
+ March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
+ Prevosto, Virgile},
+ title = {{ACSL: ANSI/ISO C Specification Language.}},
+}
+
+@manual{acsl-implem,
+ author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe
+ and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
+ Prevosto, Virgile},
+ title = {ACSL: ANSI/ISO C Specification Language. ---
+ Frama-C Silicon implementation.},
+}
+
+@manual{eacsl,
+ author = {Julien Signoles},
+ title = {E-ACSL: Executable ANSI/ISO C Specification Language.},
+ note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
+}
+
+@manual{eacsl-implem,
+ author = {Julien Signoles},
+ title = {E-ACSL. Implementation in Frama-C Plug-in E-ACSL},
+ note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
+}
+
+@inproceedings{sac13,
+ author = {Micka\"{e}l Delahaye and Nikolai Kosmatov and Julien Signoles},
+ title = {Common Specification Language for Static and Dynamic Analysis of
+ {C} Programs},
+ booktitle = {the 28th Annual ACM Symposium on Applied Computing ({SAC})},
+ publisher = {ACM},
+ year = 2013,
+ month = mar,
+ pages = {1230--1235},
+}
+
+
+@inproceedings{rv13tutorial,
+ author = {Nikolaï Kosmatov and Julien Signoles},
+ title = {A Lesson on Runtime Assertion Checking with {Frama-C}},
+ booktitle = {International Conference on Runtime Verification ({RV 2013})},
+ publisher = {Springer},
+ series= {LNCS},
+ volume= {8174},
+ pages= {386--399},
+ year = 2013,
+ month = sep,
+}
+
+@manual{wp,
+ author = {Patrick Baudin and François Bobot and Loïc Correnson
+ and Zaynah Dargaye},
+ title = {{Frama-C}'s {WP} plug-in},
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-wp-manual.pdf}}},
+}
+
+@manual{rte,
+ author = {Philippe Herrmann and Julien Signoles},
+ title = {Annotation Generation: {Frama-C}'s {RTE} plug-in},
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-rte-manual.pdf}}},
+}
+
+@article{fac15,
+year={2015},
+month={jan},
+journal={Formal Aspects of Computing},
+title={{Frama-C: A Software Analysis Perspective}},
+publisher={Springer},
+keywords={Formal verification; Static analysis; Dynamic analysis; C},
+author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and
+Signoles, Julien and Yakobowski, Boris},
+pages={1-37},
+}
+
+@article{runtime-assertion-checking,
+ author = {Lori A. Clarke and
+ David S. Rosenblum},
+ title = {A historical perspective on runtime assertion checking in
+ software development},
+ journal = {ACM SIGSOFT Software Engineering Notes},
+ volume = {31},
+ number = {3},
+ year = {2006},
+ pages = {25-37},
+}
+
+@inproceedings{rv13,
+ author = {Nikolaï Kosmatov and Guillaume Petiot and Julien Signoles},
+ title = {An Optimized Memory Monitoring for Runtime Assertion Checking of
+ {C} Programs},
+ booktitle = {International Conference on
+ Runtime Verification ({RV 2013})},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {8174},
+ pages = {167--182},
+ year = 2013,
+ month = sep,
+}
+
+@inproceedings{jfla15,
+ title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
+ editor = {David Baelde and Jade Alglave},
+ year = {2015},
+ month = jan,
+ note = {In French},
+}
+
+@article{scp16,
+ title = {{Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring
+for C}},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ journal = {Science of Computer Programming},
+ publisher = {Elsevier},
+ pages = {226-246},
+ language = {English},
+ year = {2016},
+ month = oct,
+}
+
+@article{pldi16,
+ title = {{Shadow State Encoding for Efficient Monitoring of Block-level
+Properties}},
+ author = {Kostyantyn Vorobyov and Julien Signoles and Nikolai Kosmatov},
+ note = {Submitted for publication},
+}
diff --git a/doc/userman/cealistlogo.jpg b/doc/userman/cealistlogo.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..966be5a8ff6d50d9a7f50759633ca144c4c5db1c
GIT binary patch
literal 17028
zcmbum1yEeiwl_MsySux)LvRc3?(Ph3!QFy8!QCaeOK^90g1bXL@;~Q%_ug0as@|*H
zQ#G}F_Uc}1_wHH!TlQ!9&o%&AMnYNw00II6kox=p{;UB+0brni+uv`n&jt<&{<lFx
zLP9{oK*PeqK*PYm!Xv@M!Xd)Jz#yO?AR-|nqaee=qoScAqkUc@|D6Qn??^Ck=+A-3
za4>M6zyAMhe|i8Y(0~$9RWJ}z04NFw7z)Ur0RRC21ON*5DJ}@$KMe#F3K|9s5**_5
zwk0wE1oV?F7z_+F92^t^;2&~u2oy*t5@=KwVHh+ebW&C$C%1scc?@haE^dkM$wgQq
z${Nmjbq$zooRY>s*My|r860v7HT9t2{QB7)N-B0y^Tat0F>w`BGnc@Sg2KM5PfqwC
z01$An|B~WU8gK|mC=gIE=+C>-D1YSufrNsGgn{^n=&#tHa*#lNN}=Qgg~o0a@VyQl
z1Cx}MO~g4NarTN*Sw%H(hK!tpQ&bI@zk?-a+<RUBXB7bd$pjPy3<V$rILRO-fs<%H
zTvgz$cjqkQwqRr_X+>YD<OB7iM*<d6auu|ho5lLwSt>YQ8r5pzS@rE#xjo*Wt31uV
zB4(bQUV44)5~LQi9DUi}oex3G&4?XIZK@$Qu+m@Lex;yhYh|HeVIzaM1cETSP@>9B
zlBcZSRo-8ou9jREJrHoM%xx_-DeTFf@j5hA!v4r4_g!Ioh&`n>+t!!+#u#v6^hPH@
z(DqP9)RnsIvSp#h=XS0t<SSJByKAzRhJOL(F!n6{Rnj$iVg)DBVC;u?={MLZ3;Xl(
z;meZ0voFYRys9H@sr)lNqymSsdY`??Il-a^mZ_WE9{^LpMcx~o;OiS_)tj|%nB0S_
z%Foz^?ihuC=0~9o-mqw=6r9;Gb8?g1Ke~A$JR$09c<dgtz8tFgD~_Vu?P`nPOSjRS
zZ?++-ZMj^E*!u7)Uu8Ap2!1xv8Sy{jZ2kerRSaKNJz#LH%zMAP)xO#IhJ3QB*}tVN
z+^}dn{D%P#MPj#O&_()Hl|P@iozWOaS6}ffZ_v-KMY6}GSJ=;$Hi&9RM_Y|OP5b-2
z<NG-ZzI{k-7Jbc7Th~pgdpc*d4h^MzK6a);zTaxgx+a_M+UtY`Dg+i-KG%~jeS|;v
zHJZp}D#RA6`^ZL6tLCpbb6dAfxqAj@v=$9jK8$CI4I54$t$&HX{)d>T`_zVMXn0w5
z%0lV#Wp(QMa~#{sVwW!E4PUj%X-<6;4_)FPfYU#c2R**qSv@Vk!ls}7{v@8euKS0$
z^Af#P()Ft^a8bPrc3N-`YJ+V@2j;&KJfC4?u0&+>2x$)Tq=x&hl*{aDMfzaBkANDu
z>DAZQ*l-!v#c;Z4WPbPcScY>ZJZf?!%HP`m0|@88&b+4~-;<5QBp<R_m#UkUscuoq
zQ!Zrnohdvp>i6?@vca7zu>@2Nh>26^TZ)N^pr9ZJi;0n-pg{kxJGzs<S)ZPMJQvWN
zCPpb^uHB{k_$d0!B;St=mcb$^9Vl#ep7z#UB!%4#TZt>%7bc5%lFQic{>UsxEgDY9
z<4+OUKBA^Pf!PmUQOuF0;mZmxPc)?*Ev)o!;TeUgFB2&J+_0X>_1i}zpBn|HtxO<X
z7k~eg;31Dwjq=n+%NdxI>PD?7mn?m*r7N2p6&RIJuDARnL9vlh#W8dACy2zO@kC0<
z=n@TZwaht{x_-#H{zO5%X5<ywbC2spSvDoAOb_!L)tT^7(pH%?6|Yp|uXQ!EzPXx2
z`}>vEpExM!MV@;9St`{;7ZNQDMsMY#CTI<D*_`>-a}kW0&z>;lo^mkLzn4?|0A&)Y
z(;&gCf=njW=Um1Mz609$G6Iv>M0;~qx*lS~9}W?y$(Ci?{UeHC>gYmtj-%AP7(4Zv
zw*Wp@zT#H)oFsmZC6ft?%dvg)1E6XYHz{*Qv6s8kUPg7%LZs^&lBnd<iNsthL79Hx
z!xLS4FO|}*LB)s2vT;sQyyJ_ft80&#!`j*!Ymr3X&PvbSB^sb#`omGVNhhC_1Ufui
zgp?FHJUp26e{^UQ?DPM5EU>_&fA0+}wzmJS*_z)e4T#W**v)*Movhj7D4<GjN-p*9
zx0m1(;y=>PX<-gO-xm3eDg~(u6$bc<_gq;rZO5FcmFjc)N@}1Eq&8gs05Mzw?zD8R
zK~`o>)##fOm46-lg0i1-9wGPvty|iyLMG}QbMOG^WIevf5@hSoZix0TROnj*nDo?0
zK9EQJU`F{z#?Q-1w0ktMRe~}6tKP=<h?%TY$YQc<j$Lc*O9$RH<D;%3<Zh$=@##Jm
zBByHzwOP7G7Y>&JHWwF<OFMQR^hN0_TNLTs+7zS=pw^k(Hoyh*G!^D8kUn#saP8NA
z6nt$Yf^GcM4u2Peb{LCAoZhGW)R==S{sWN;sxS)Xy8)W=c-!_&SafI<QqhxT!i^{7
z{MyErxRAwd%$(Nv+p6qP?B%;+Fr{)BAj)ia;dSNoPWj4DuBKQn-e!6sI_U~k3iFae
zD<F_{mH{a}1`=%Z7Xm-rItT(Tfn4fuH`GC+o2!jb+MQcRJvPQUGR*5Aje0ZKT;7NN
z!i-p;rx!PuJlkf6M1z{vl1O54Oc6xLtSsrE^o49xJd7Kg50f4j#R*b%HoEk1L78`n
zIuc42)|aINdB!xHa?|A0w~(0{Av7!?H?b++L`*of(w5#uXYbobS`&4b5DzvaDS>*i
z`x(}GYNqb2=uOM)_&Y%Vh4O*yhvr&!i~!N9N%0U!^*8}sav(x&I-=GE6BEQZ0>D}q
zcb8#+{d=#rJN&MU5A>YMlV1q~sJ4*vPz0_#84e<6ScMY<NX@)^iJk}jSZH%rkf=R=
zYD}P^SV-8Gth)}xRXPhZ1-S)<-l7=uNQB=RqNQ&?7@VzW<4w^y6J$VGzEPVSMid*k
zI)SFC=ST|ncY=*s6%lxex`1r03)Wd&kVPCTkZPL;_+ZK8C-OR4jsVn&WX%3KT!afR
z=KkDtqt+~ea0+uG8aB~V;W(HHlO3_-@TI0nBM*o|UDO_3C}x;#tfY6$2AP!PtTJUP
zGhzj{s^lm_y{i?16e!PFN08kCYo-CW$_e>Z5s?5kH9I~;HQI!Go)#5K4!;saKYL``
zto>G7?qcMVv)^Nlji8IQQQ5Z+apU|G`FktTB!tFMLa+p&=_In*sV?J;)%-k`$c8Qb
z459c-{31>iuLBP3j`n#bVD<#D`@%V8g50K7K8rf?j+76bRTcQ`HBn_oFHNkqFX)~c
zV%hdP$lE?N9zd{Fop$fQC9wSKFv&_u<Y-vcGhrfNIen_<*4F0wM(vWf)5A}KC7l2*
z3uHS8l5k*iNS4x-R+6hg{LbXBv8mRL>1AJAZnN*C>?tT9)9Iy-PYm?XmT%Z({6^cf
z!CZ6Xv<>x1FN2f?GH8k8EJcRDnt{$30|ImIlURYc00v%yee(w1m1P6-D%psfGAEFY
zslCI-?^z7l&iG8R(a^lTt92EYYClJYOGOJ5+SIk8qj0%XJi}n(uuQT}wetD{D2Ee-
z`<DZ)trC>)c%!w#<9s+p!st+@fN9f5?ChWVVtbbd6lS_|1<&fm#|n0Ub36Rz`w9EA
zmZc*FEh&DS_UKnn=uTV0%G6$`G#~RmaQpbh^#GUTRr5HSa4XkvZ0$NoG~-EmwLI1m
zh>Zn8bMPeW__a>(i=K_|Ms-hLjxIUQ>8<##9Y4Cal|_{+OkS#MD%lS=H#`jf0Mu~<
zg6dr6X{2Ub)a!7P;U3BIen~i{)so+va&=FmZEk&0px7Y`WnoY@m7a6Fm$&C@8xu)Q
zj6ykb^#8c8qUt0ETbAlfQR!ck5bLihU^PGxOA8VU2{#%W{W_m7?k_IgUTM|sqXVr=
z_{6iFtu427zyFX^!dao2nbWs`23vD+<-If6>tgA5JS8&$%C&=uC3;~ub`f<6g)mF+
z|I2M~D{z)Vq;gi&ECBmO)TS!r0Wv3(9{iyVFN$z>i9KEzllX!5(v2n#B`*50pNRn&
zfp^hf<;&=qGu!bPxt|NX(r8uko2_upGqcI6aawIlpE0}f9U%0Sdr3+-2t08Y4;#5f
z_B`M^VU-?D9+lXw(8t*D$#SorTxf+3FM=B@{nvRCHN--?jaFkps9j@rfTg&t$R1MB
zk<cogsiS3wCOSc{BT`@<eb$&1Vs5Ul4`;TsiqF~MKjVhxAoHx?$2q4VblafBdlLZn
z2Y}$?<_7X;K1{j#+Q}*O8seh}rpJ?PF(xg`3kMTcYOMx-AYzw@WMhm6>Uvu_`d-JG
zxj}BeplCI!kMw~nWJ^%|3vjrg3Wp%pfim{g6xz6B@_RcLpULJa)o&-|m1RD`eG+(%
zq&;?IQ&og-f3{f_^&$F=*?9Do`kW+3bIMYeETm4tZ2rV0{V7pzjt0NBncB8dgd5;O
zOhnx_pFisp#d#(VSd9X0jN$#g7I!BVLH?EnIoc5#5ZaS6S8|v?-fy#uXJCB>hHzQ+
zR8d}w%%QIKqgUsoBo5=bxR_+Lo_xTv51-m@6PRT?4Iock20-{#*m&1$@6n1KxWg`%
zHa=~rj^7I!>%(2zEysmw_kTm724F#ELjc2%IAVb={*5Y@lkuw^GD(XVzqBIUWJKUi
zbw!?hO~z&8j~(*_LW;LScC~$@8mL%U&gP}p&7!TFJZ3WRkR{SdY5)Mn#gz`g?AY^i
z3G`AeBuQ2uceMz8jC%Yn6CvKJu;1_6@IH^aVI}*8x6X|(o_yo856vAzk(2T9i7CPG
zoa^!BxY;t!#%#fonxLi2%<0?pI0tSa0y=W-i<*ut%F>)vk*Odyu`~k!ND%f!AC1cB
z`3*|ujAHq5>A}v&gFRjpLb+L{-&$)7ZYxvk?WM9^4ya-ScP*HqCw9_pm;k=T0R%?K
z)fjb9Bd&QZ&5Ne?7=Zq6@6V;X(;kq4!a3Ahb3BUxI}Zxh+q#3SIhdix>2{R_t(BnL
zDd;bQnj$U(>l;A=j8}&PNogAp)9d&UZ<1+sTF7`Y=aS)7(#H=YZx$)bkVOWAwfVn3
zM)vx%5{p|GnYST1^6Az__K_IRQ&t-R3~S|;M?3vNtjCUWs~ElVQJDM%#*&y$8u;j?
z_5m_d47R9uV&X~v6GV{)^+GFd%lp?1DrN=9r^E>Hu`i?EOpj~U04s5O7<D}Xe5cQ#
zkKwx;7jH4*XFP65GP5z=&B^uz1>F?2YPzg7YN5Ux5#Z3-W0X7g)o(esdH7#wz9v;l
zuY~r76-di1;4G>fY!JM-Km<6cZ}EwKjM$JN8m~aR6i<zFN>>*PJ0XKhLRyPYd7H&^
z8mztwvC;8gZNd&dCCFIEDPIJzAY$<1bGgUsKCDa-R7kIG3|+t>Y(PUk{A40%(X-GC
z7xlee=I>bEwBDN8rCDF#REID4Wll`HD^bCL>zg;#lf0B>ni6Qw$Ye62r%WV7^G<ux
z2D`i&9$x>~rU3F4PVH?59Y)tw%QJ{mWvt~SD#Up~{{hsqcC~Uhp$sPk&3mdm)_7jo
z`$b57`|6eqUXEIrtp?L3f!=!{%&F?MUn!G6`t{R7phX+8jg>ni%GPQiVG5@zI&jQJ
zHOnW*$*A>+BgEN0c0R}3M=52Z2e*cSGo*RP<Ti@OrETq2kHg)#Eh=NqWBnjLYWZ+!
z!w@v517?i#LRr_8ualcjkg}x4vBM34v-2!&YD0H(T(mAKP>6UkybWw%+{y(XrwMWG
zh)3B!K*%R)&iXi!h;e=xFJ>LA;PJ8YX5%3nzkoMRz`{%PxvFP#F5jF3vv4=I-HloI
z{o&Feeqo7e;e?Z38vQgdUQJDH70?MM9+_b8*v7S=mG8lam^`gy{4`bSowRbv-NYw-
zo<c{9vGYYr6tm8^+^lPuDfCQgGz<-JS7WaWLFuJ*jrv_A&1-c_%9G`llL6zC1Mr56
zd-k!waTZN2)y(R!={8y`xnz?%PA7TsG{^RIg+i8St24w1l!12;4`aeePcGRmO3X>A
z^H_dtHC%3br|T~KFOs)1I-4UE25i?v8G(f8^|}M&7dctOYkvUAQzG_1GU;b>_{fd~
zMMPXxFs8Ss6oUp>w2B5;4z#6fQ5eB?&>SIOzmPAZ)>aoTgG%ow2;$|nbL<Yv7M3d~
zbCVj&5PKum+6z6V!yKwfpXo@Z3J~Cl?v*lIW3=MxBPT>oU!8PJ9KtEEfFc6}uK61)
zcf^nL3R%JQ!htz%>?%8)64AfxplY!OorJ!~<o)_OfCVqW?N(YP8jPP^($OEm4)baA
zGQMd;ziIGB)CWrIAq*0rE5H9bPGjRXepDpb$E~7vbr9r^&vp9)U>Q@mZ7_dZ`$h90
zYYvIeTv$wKG`e6$v^4THXJ`;$-!9@#h<ggRx>{vCGVITU(&BTbSH@!@Rz0v=SP=LJ
zP;NgrjSum{SQpb5b1?|Zi0Vy)<D8kKwkeyWWtCIemOG<&<1--mc~(Xz9N0}+pTvnf
zj9el=|Le3&64E@T{kfyGG_vG%ey)=g9x2~3^l!VXBmap}zhache;<jOfz%Vqc~`>i
z&3P~G;JJGd<Jz}N?IC^XdMvg(^{`u0V~DShb|r}_+<a%bjAv5u{oo7nV`n5I;t$Ib
zd9X+jV^AgML@h>db%*6lz0z8aKY;s&t}+zEtA^NtZd!h%XW(WT3Q6gWW@bX01%1dV
zV>gGES`KV|1;(n9(s_4$MR|K5a$U96*<+Gc&+_E32dliB)6K^CXpqsx*S@d;$U)pF
z0+D%LgP8!{=U;U<r)-9zNsJvlG93;10tLgEIG5G-J}5)0+3KT*n~Pd{2`wKgpnFdX
zFj9&2@HrtIh?)bz)5o#qg^pJm56l;HtxysBYXWi;y1YhhM{ew=h6DB;t2fXuXpMz~
z5=yOCQQ-?A^M20i$y~_w%y##?jm9<w76L_^JCLm*=KkBqK$OgHqUny^?A?-(e#7DJ
zC)~~e{@t(q0e37e>=x=u19%hT<DA<bC`us?52;DIHzN^_7wzn|16+uF3*4fA04od_
zqs3F_Qa<<v1W>OjG0MCw4V320kKQcDsER=xE?JG5mz&+OeT(OCrZ<^JS>MN`6wOam
zC5<yWs93q&)vB;XA~%FX;1L$1PD|;|>G)L79)&G*xH1}{t1XvWi@_bn*D7UW+N4-H
z11L}_vBOjc62A(ZL8DIk&$=%8zGyi|u&L!bL?g7NdZ4mvK_OA`sZA`d2%B(;isC{U
z&Rc3Ug&BWP!q&j61s^Y`$+iJ1q-3X{<sF?uN&9UcrE&2bn9hR-4pR~klPQc4Eg7bZ
zP%trng_j;_Z(A#dFgjvEc!q&hUxOHR7I3EbwhQe%%+tm^%Ga?U*2^b?GTT}%aWZ|t
ziBDWEx6Wl|8Xvh?sTmKvC(7-#$r@a-pNNeFEJT4=3|Jw0wovI~{RCuN-C0G35}U`A
z#g-T(6+gudu7RGs>kt^8@jt>oFc!>>$%SWRhr!1k@qDAVkWfZ(N`KOg-EuYj*3puz
zT()521aCc|Z(saKu=~3#OoIGbSLV$e9M#@X^utmihyup}m!|6g-%V?<3pq^t!i<RZ
z3X`-nQV$Gw`b5RS{?<@to<uxcn>%|kL1T_R!6SJj+n-p(e)i6J`72h*grns?yPl~P
z)?B*MOJR`J_0tcBz{Hty`?9h0K!%v)OFIrpWR5zzQEQ`w=`CD(b&=5Cj>pd4DjUxP
z`3!(M#lV`D?R)V4Ykf)jeE9a2X`vG#$sfRh1$ZbvbzN=fTGAdaKQ-tzK}P+@6Mkxv
z$3*DtV+YF*Cq~dM`IPG_+Ht`|dMw$rD4LWORv>aH<f^?jmvb-p4e?{Y%Aj?Q!?{D&
zb3X?z{0C`T{!EsvIBPP_^h$eA)1?)GW#`jYq(|b&^GM>00y?mm=Bzj&#cFrb^H9gA
z33AiLmUd(vA(2h-B>8Yt-?@IsVQemoyXoh9J!P9S1aPuKsa(BWMXh}O&FUoh%;M|#
z_%K%#E?rCKaN{39ub&8*_p~(b^>t=`rpoVltBGs5jV6sInGUat3%Sfvs(U#4qdH`p
z=A7QVp2SYBlR8XzEk5(Co*!oRZblvM5nI?QG?Qs4(U7T~?N@{|o3Vn(dKMW^2~#%g
zD~=_d@rOGDp4Y;IZmw}woZvOG0YF!O);&A?qzQZrih$Z8kuua0MMP#XYab~&zWgJV
z{3%<vtGd|_zVbGDtX|G=`f4rDG&WIQkQROabv=}303a$su?Ph@WPI`yG(;k0`~w+~
zb8PI}<o?UQE=esQnJnb>7zPD(oE7)!R#c-B7qP{N!;nP(F1x9w>&Y;D{IJrOn&!GP
zzBV+!C^zGHHfC0qP?zojWZQ;Hi-nTpM5ZTpWO97NBj9T3oPwB#B`|vxxbq%0#uY|g
zkXm+4R3t?pq@rbkJX4_Ky^`Dq-;)a-9%Lc)qzAvJZ4ZGhT(4rq;LWkawI(wHtAw)p
z1ITMhzQ)rye^u^ldOrL4>#4qTNx{45gyX4p4W}|1AsbdJwq4q4dccu%J2ZwXB~{%m
zV2bu`uf#gNGn#bJsoPsC4x!-JA~#3D0KfnO<zSK#7!|>rV6PD4nV5e>=*-^VkaZCw
z%stJ@7?W6Em6{s3#0{^%4VUGbpkUZT-x|XCb5#g($W%t&e(4Yg{$oKomTKqwN;|%g
z0!51CxLpT}pyPhgH`)d?D3uK%Wz)Kp3Kjih2AiF)qET1zL>(OPq-T!vPju?i^<{MM
z8PSU=VR(c&3$r#9mJKW`?7z*Sqa7WA5?1YULkvyVxCnjA=i$x3<f+QBD85LFY%G`^
zxBkpB(RrAbYO1o7mTiKzBi_}E+8C|?9j2y>wQJ|V{I{$T94lxJFH=g{sd+I-UI^9+
zy!xA~sup98=2qgS3@(?<i$4GZV-~WcHJrs;8FEP1y7#4;K}OsG+Xg*YJpNpO-Lp85
zv_>trYW|2$O)GU=L6vMEBR%@oT`US^aLVaA6;=6>e?*p9w0CMC$4>MpTSNJV`DTme
zuwWk2r6X^5xqm<PMJ&c6HWwWqB6Z%__V>iN0r&HnTzXng0mk7`b-Bd4LqsJag5@;;
z^sz7fF`FCL9{&(y0$+~w$rJ@%HGd%Rax?_FHI|TcwhO^7Wdsj?7ydAYDh@~pKS2Z*
z23?z%*`Hn!Fp9<PsKDJJHIo}WuZV-o|Api;0Kz-J*vcZFC&f$uioGlfXCD1+7tdCD
zWhrpuJqbvMa!wRa+K`EDuS|AiGNEjaq}0x&mSTzEqF;Fo7L_v$vU$lepyR*q#uT5o
zll7}gxy(tAL$XMN((E9gV{M4OktU3z5N#lZ-MWphnRB5<gXGGjo{e&Y3Jev8h4}E7
z|1vv_$iy0)C0R-)ONWl{qwldh<49|po^m*%DcuoI0qPGQyg3u*i3RR1N^qcu;{zAI
zXDuh5tC3mjbMCBXCU+>k6@6|0T?ZM7^Rf!cGF6GJ2bg<oS%x#bYd3V2*8tyFJBWzA
zHUSeJCm)eL=U*I}^;g5+<D;|%KulOYAs%sL6FgJ1pZty1+xk^7uqzoZ(i5+o>tlp`
zacM3!xtFc??C;R>WqyZWZy4_?O#Ucxq(+C&^*3gP=j15B;s*87J<T2b_6_n}uTdQ$
zJB&wc;!GM{)a^R8bh6D0ER5M`c+0LMMUZ0-AsZ<CYG~RilbhM9fvFDeVXSO-ZKl6!
zrxgo1Q>6Rxgqd<`>`u_8eLF^UK-i~+*YJ*Z5tfUws^;gHGlR?Sm6-_{M}9HXAMpyT
z`N6{EOW&h0b!Z@cfmpC>ZI3_7&q}N6fi`<pjuG*|3r|K($}Wal3z5BT;Ci_Mhyw)w
zW?Yhv{++r^Bq>u~AIe{?F|b>2ufTK0wbwHay1eb!&2hcVQANFKLQcykWWJyQ7?+4(
zQE0HRLUV%1W}!gNsmxho4`W$;Jw)pXi5vlO`Br2DJu<O_50f@Ky=pwBFkC1Wxz!zl
zi=~HnREy0-b~Ac--Xqr#F9tnnI8&zONu(X2TOgbnbFdudVAb^Ea#!I%-Kw^E_7^2e
zvn^bBYpAx-ekf>$P4RRqeb+5-J=aq`E`Js<CgMMQmk{Ss9zF$gQd@#$>{4i7a<E<>
z5K}fg{CC7i`~WLpF5zC^$p<yY$np<>yqfGt%V8rGzv*Xp`>j{*9_&*)isK&8^&x$k
z3z&+J^#0EE($~fGbF?Z#fqA08PC0SCnDTZt{Kq<bt2FU3sA59t29=_^({eOQ6D1VX
z)lsK1Y41x6V}skkYri!=tT66iHqi&USY*M7vAwKSM;qo<JLrrddU^93lJO^mUHpt@
zg^bH5JhWfjip^hSalk3ul~yQiz@k-kB82uhfz{b<NyiNrfq%ljp_l%}f@E{0XE<IA
zK7G#8t~HswFzD-0m>Vh;sPN#8Z-E#WD$XQ$tB?;{s>dQ0lYDA;pwKPInmkV=lrR@k
zyPwEfUMP+3=a?_|isv|Ygk|5-6V)Gp@&P(vNym62t((wnoj(g;Ciod47wC!K`2*;$
z^NoD!$aHd3HJtr6z)DnV{3@<Gd|SP#w!?6!)j~?jDBG6T)mCZN$mt-n@1~)43&{^T
zA(>>$?Ob0I(LyHSy}B4E(Y&PNti^E@7XchAyu}?C8^BgzA~7fpVnD6JhdSQXYZ;4m
zqi>P@oe=0{RU3P^q?ygi8XLVaCVzd%H?Wc(X>nc6QqJpEq8NT8Mln#2=K=i{DhQWv
z8Zrg$iErSRQ&IkUlQ*%PPPh_z$i@XiUOe)6iiOaLrazFBp;|+L&iDcFEITWdc=)-9
zaFx-ZZ#>m<XCODJh2N+?L&)`5T3W-iYQ9Mwwf5?vQhrl>OV>^jP_XL5Lcn4n^@F}r
z#~+QT%U=;U-SP?=tIu}REpOADt7vGz2h-vx2=S>6mpg~>{J~~5NIQ?#WSNnj^DDK7
zdADF7FR@6Ex-rjXZk*Yn86r)%!9o&rt5V|#uA(6mSlarl8Hu4#ZMj^}y1{|6F_RUW
zeiGK{0&HJ%1CLc$opPCQ@mlK1@U?dau842-u>{JkrTl2y>a6NyQS!v05)z`cjF{e-
z#`Alg?z<7K?Yj$v`(4*Hl+d%dq%z9nQ?Tw)w_9I3n>Cp%tr&G!S}(?J)b*E(dhFPO
z;j)A~9EH+*U7!86Pg8VA_p5DYfRAuXr#QYEi6v59bbAw$q1cOoV+a~5X#h*W<|^$U
z01at>4Er3CaU-iTycB97zl}139SRiqS6JnLKu>j|LtMsR(9_P{^cVEJ$bI}Pso-pP
zo{Cyr^e^af_y_cq^2vl8?p7ZhdK6mg-u$={6lqgxqW0PB!B#hy+63pd$BjU957Sr>
z{rrDwHUTxWeWFU!@hGSoWBW{)@Ys+xpwU~FeJ%-zCq`R%RoiPdW!rzrxD@}4MlnKQ
zwE8(EQ`({sNlvOlTgShSeLi^zWgy<R#1Ns%uW??fT&{{+c!1eJhAHnS!go+ywENTb
z%D8T@#w3gsn#2#(MQ(It%BBY>*Q+QuT6Eu5$4g6ux<Tcs$2L~NTQn0P0Gl=Y6z@1;
z6=%b}k*GBG2e1JCxp<|?S#laFc}6Fy8!`m~=prde$$`gpCj3`6n$yyB#o729Ymv>4
z)!SKeqS<ET^X3N!1w(;{J()=v!MsELPMChDFVm;G2-{ut@&WZ1JuU1D#k=h4=G!SS
z;jaxG8F~0xFm3j%4=wilEXCJdMK|O%t|B4mEgX42P(4#~_gO1?t+VAbA>j(Xip3s@
z+BkK&PEx7Wc42KqV3(N7$9V~&1VOR7MPATEq^rB@(t=CHxMZbSZk|$+8n}_zRcj)t
zGi+g95sk0r7K&&q!!PQcU2^t`e(hMKG@<`xXsJa$%W-xZUi;eP;<2Px#5p!z^`n?{
zrft~hjd*Dj0aKkuz!6IF>i{N8cF)B!vz7U}1A&i|^sYQBnn${@QRS(S5T`P&y`<bi
zai+%T&+zY1iO`<SK$IUjwi2@kzqz>B1lTa0osG#ot~ZbCj0ZivcLjznfLX5O3DQ)`
z8Ug%)3C%)A@0qdQhrzU=G=<~hy&fL!W)ft1Ey7vR&?ozkPkIBF{9wLAEmj?{;;?x6
z9V{6#nG5C4cUIhqiIn4p-TP2H(^%7I$+g9#lMkbN<2?~<BE1m3S74B58=7E$04h#b
zj_t<r4!!<QqE-#xZ1BTYpb)dlM&WtnOP8#+>l!10KPkxbwFhsVLdNoe4DI=N?t?!e
zOg7pdhRY2jerE-YtkgK0lmB3aur8yqbV#vDgEOOu`es8C(msXTyi-*NUJVorKWb_H
z1jiBNiOw=kK5kN*=v|D9mt#j&>dx$1XDvYM<Ri?nETdk?zSXGM_SnR6W-Tyo;3+$B
zw)JAsc-L~S4=<|7)aVU8D~&%-nBdf9&ST>!GjcdAs3Yu-gj0*o{H-E)()M@X6Q;V>
zHAOL1-uQeDo)e@5TF_ocj^6PG*6vXwQ0~FSLPwgmH~hCYe`eNVs7UCnErdTn&tX`q
z61$dDv=6yB!|PbBT-2a*fLm%9>b6=BZMCg)HXh8)p%?%F!<4pKdB0?D74n<!DrR7@
zH~g`VBQ}+HWas?{@LT>yxBN4up;hjrhf)3WXjVTiedgc&*U{{p^O^Tyke|7K9qx0R
zd5?p>CwuUDR3E_%-9dRxoa<zTN6K`p{|^__5Le)(<nJ#xfwNTc?u_I|MpV2k6Zd}r
zNE08mHBtNu$-dQYZ!RWNn8cayMh2KZRCLBF<7|#+s#!<Wem4c-b=w8P!!xF^9*#1o
zrdX|=DR#>R2a*BbVzck1qF@}i8|(*(X!+sZY%j~jq{{hIDEF(=$4I=!Y8kdG%Qp#=
z&D80dP|yjXMGm>7le;dG2%qAfxwkaE=5wI@9>F5l{1TB7J*VxVE}Xh*@5`V<THWYa
z<9=yPmyP}boMT;5SM+-{S{DYjNvYU)d6Xz;NQ5v!zC4k8$PV#E6_K?>5ms*%d8ImV
zIbMC5=3_OWToxMd6_Uqp2eU|7_V;UNspJQUu;eF}sJMRsX~wTcy*?5$Z;IP-`!GoJ
zEWRyj{KMI9H`OcuU=tbAsE|QwHAmd1C3-JODzU|x=%m_@yB{*Ozn|p8F9hS;GL8_o
zXNHwqiGI3~d>_D*-G!Pv4E9ic*3!a?XKKepXVqVOmR5LX9sj-SnWRCNn@)_^SP5`=
z>>D0)QDl1T8^FV$?ZL&+cNFKeYd?xY<kjB%J_xXCa41`_7m~b~YGGrY_(ph$h##hw
zTs$tETr8ZisCC&8t$gU{3C<OMn5ZCEF98#|-<(T=T7WGQYTJcp2(1)4+vt%G_Q)6L
z)P9H-#1Arl+}6=^@n}H%{3hh@sE+GHz3dG$YgK2+To;#|6b3U6ZVh4y4)(k>!`as_
zt~+lLA|iy#Nv9nr=gO+lx^C~_UEsehiB^6K)CTjnYzj@eu901TQPb;rQSsn~b#(+c
znQRHlwA+}V*Pk?Q<$F0|N^EMRJ7sgpZR=uQ`por`_iGy4Pi~+)#A$J(6|tG>_Ed3n
zQ7Yx6kkKTN)?0#5N7bo`vAvXxM_h#^yy|{pHMBX_9yVl$Gk@V{xC{w%Cwfa~c>xtx
z?Ng@QKad>q!amYdG^GrbvV@z5gQGUYoExevp9yc(pay9}LBUj4`ilW`665~w0SbSu
z<2mbeeJgw`qOoLwnfLGW(*R1S%~|lrIc+s>IUQeM-gW|w&1l|sGoA5!@k%`QrT`b(
zK;#)w_!!B&JFdRz9+wnQ&T`%##-?Y!F_2LkWJ!aG)m1M~+yyH<dKQhqK9No@AwnU`
zZl^=@9Jd$$Gf=&x&KbCT%HWoj5|rKohcc>Mu>g$_K3e$$4V6R6P%D($Xkifm9m7@I
z5L5}6=N*=$oW1)!EGsojjiD*WiH6z~Zfiu)9F4tmM=zYh^PIWDgE2YQ0aPrK?R>o^
zzgV9APB7jE{^ii%=?mDN)@1IiO(S_yOAv>2Z^I<$hOM@(Irq~qQ^Tzv;D^UIDw2Y9
zvU=64f?gO(3?gIEX%<eid;M`BE$m_~K#2)W1br4fz;vf$jfA?lI$7<m_9Axw%@W?h
zoI_?bR7Ct*n=ccbsq>>@Rd&6)?1NE;TDWEcc{mEG+)}>i=hh_4Rq~zN4}Xk9U4WOK
z<!J15hTEPyxx+<#BJ<0Zw(=k(BbcGD#pE9E=oycgQ5tR;t<#U4m4$y>+ifP=XU<+k
zLi_S1jsgtZmXZHO&<m4v+IhA8g*WSzScF%M7#PQKCA99&7=6ej&8cJ<dCvxKHUTL}
zQ8f0oFGw*b)d48`B^h!OwTc+K8Z0#0JOj;FaE`kkj-q+Jw{hGzgyk!?8l~+0XF3G&
z3|2?iBXGQr92NHntwmOU7_GDw>btx^#fkGPCmRtht$n50CTrPrv9V6oh2~-yHX<lF
zo0}L|-2@#&SsTR~^ZH@74wuheH5xy5Ur96ikixJFPMZ65mOat8s!|s?9njfkIMh2U
zI|8X}A6z=-4KMxoeJkrUe_0>f=*8uy06{fdu9@^kJ!7M)s=<DAY_7{KHf5G|sEAt4
z(_9)@>Q2f`DdiuW5F&_ZmE3UHb1pyoz2mG-j9I!*YNo<@W!+LL`dnyThOqNe;h+=P
zvmfI~VxNL;N$39n=!Q1Jrgm$;&69E`4tOo!zctx5Yu#DzPl5!qVA>gbMyozc+|L*d
zlIF^VLKb#FVYMLbh#~N=)}t4%tkD`)8cB?tv4odRlk4hHuZ)_ulgyM|5Q1}w+of9&
zaHZk*$gS@TIyW!_3pg6&nRL=LKYr?3y4@Pe$?>%=d+R_nhi-|AJSC{_{#fRgWd@mw
z5aJt^`ami^<%&vTtByRygWO)s{$a^^XybX&7StpuImecXDSw!vwp)g4W?qX&=p~WY
zVMduB3bG^`1<&2j2+*}}Ej)p9?J84k<87|`9(nA%jGL`!A{Q*Jy<UCV5lFUtS;*u+
zhEU#cOI2hv=O}2RN~}VBJnFJ+x?cfhLNbJiJiKpTIic`dVwF}NIgCrZmu<lJP21Lu
z``Mi=;0~PUMrqQ!*NWG!;3&_ENnwl^pM{PF72QLwxAhSbU<tW+PIt9K7=2z?F;}}|
zOk)j+lT5WkCa;>wyuImNnYy(pNP74zvL20=`V2L5p2D_VfV|{gU8iUm#-<cK6tP;U
zezKyaN&HyZ+I391iMC+~J;yIOYtcApuXl6z>&ZA!m!5R)x6U=*KFb!e!E{pto;f7P
zxYznu@z`rQ`F7=SF7JFVqZ!@B4>;kOm=CxwgcK>`va%*1h3!`Jt&%^?D3w+*oY_cv
zI>$&hFPife4&51Z@A4&39;^$8K>H|Z;~kfpwN0xPDhJcov@G<U40&uj#=i<vsTGaN
z^=5yDwSYf*VwdC79=N)LaiKT7Yn;maLpGv<_ua<D_we#ZZplg;a0KKoXcFKWvV4@K
z>Y5t;i?^vauc?(B6INv4l7B{?42#orO<_k(N&odA6m7y)2%v|)^6fGSP=0z4xaXk$
zdJrCA>^mVg8@$zzNl6o!c>bMx$b{X6LP+v%v*Iyu6&L?an<FI5lgfEl-!o?Ya=3XK
zUzDrlxvz`jM^vE0pl`Eh0<fL%xu56Lhd_B`K%+iTlJ-v&>_QFA^IVOSIL5(G=5YEK
zRgmqT-yrxhfL#*GTHieY^STHI)qyLf<)lG=hy{!@x5q+JkAr!F-?>g5v(_~V+m_#k
z#P$y$jz-HYYgvWJ7}{xq@jLh9_&xGi&f-7_D&f_Vjzi+Hv_;x+!juUoMbdE~`Z`zl
z2!vZHiXCI6PleXnELww!5y!O?gIsXT?i}%zHpku_Moz6cQ{i4EgWTXe^>-o?^;FaO
z_I&2LA-s@Y;wv>DEzMe%@L7yuP%nMcRkYqigRReO0xNJ`8eI{MJRniw@ZMz5;hwM2
zsnY0LY$8$|FIHyEeOQ&Gx*1V?L!L_VAHXWprV<KTnH-sjdq>Nyz6zC}I*TRfbZ)Pg
zCYaNpIve2=Q|J<8YU59R!;g?WEJO#^jgZy}U~~1R>0qd`VVA)+4&1kO7T>DIwwben
z-|(aGT&XVfJW*EIq3Q)vi6JCtt@{I(_Q-2(_)Az($54!1I#dZb&q22raYFjNtoN46
z&TImsdqVWYVO_l&JK$S!)|FJ`1wG#R0>w+T+a;<LCZeX)3fGl<nDUep^#eS&jn!Z)
zC;HheF-6wb6Plg%6Y;4iJ^+}__K=p!wy~6rrPgz8l-W=QhCrd{OrZ)mZQXXtLp(&v
zz@HTpT{2oTIE8fP7ShSA9GK>^w6%r%ywRHWCR8WhRkjT^JFZ@ro|xf_HW=3L>dvit
zSw0IQ1vqmmN;$4k7%#1xnZI{u{6q|#?L88|;nony)b0PSpTF_Qb1qMRsa%lhW2@$*
zV)d4rL7|r`|8gka0{0a22T)sG;^H<<S=!DcJuWW-@2XzJB?KqWys5qT>Fa1UT@(vH
z6b^zPh`<h)Gx2E23=P<8Pql9T)>qSu!xDHkU@3ubMa$n{!XAY=K#%As$Sh45f;AeR
z7mtTzr9vMQG$hx0q^O0?(eY)sxW5jsS0)I=%yjc~{Q9oEJ>af_P%v5J)1+^xvvzT<
zCO$kGie+NJVyKdL__o>VlU+68>*p9VzC0vnpIR-yx&DDOwhzT&E8`hzPZ0S%<Mwh>
z`Ef?PY7n$`TRAveWF;q#6>@qS1gxw0tDk>UatEg2iULQe7DtxLxKX5$xE;ZnPty1R
zXDT)&aRa_XQNa9Kf~1m3zN|pZa_a0ZEBYD{miUs1@EPn<?RK3lLy<F4g~?Xtvh_j!
zV{Ry;x1BH6<5jHv!H`gHjC^m};diZc|6WXT8lK_-dLz!(pE2r)DbYhmJfXch=UJ)V
z{wBR`ufo0PqU4Rb1dJTw1IDODreazmhmz7$!xK;wFa~;A+QA+SoxgdWp8v@zZ-`RN
z%HtqZeLvmcCm_mC_zT`*Rh{d0OFasWWcAe)Fb+NFa^M!_KSOn^zltXW`J8nqc^8xs
zFmrJWm|;vQTR&ri1MIrXMnEI~wzsgrg487$CF<{0i-TZqw;~_o%_w~=c8lX6-`>me
zsG>N35h~KA;S27M%OO(=Og}AhI^Q~vvpzuq27YRBIousWyi?<trF<8%&3P3M;2Nlr
z6`5Uf{g(XmWhb#_22!Y<2)9@MQ?{zmkfdkj>#cdg`Ot1v{+v;$CpEPD4)){~E%FKa
zZyL|SJ30R6$R@9K*9^A2<peS-ho;S6+xyChs*P&Q_d}&WFLSH&s;L;r@rvRezKzab
z^@_TMD|H53GiXsLCO7qy-f&-+6IJif!H4~77%KPc2yWy7$`b}FnEKhI@7RZb3&C3^
zLY<#ggV}H1x`6vmw5M`^Mvem!KOCd_?hRwoKWceL>Me8t<fog7yDIPo+trR%pwNf2
z|Jde%``{2V5Rur26mC6-thAMadJ}*lB%Jdr{5$#g9p#t@CErg$L_QPu>mN%+LqNTZ
z;lVs?BOhuv-;bTZ^lffw+T|S~G>x8nxJk(K%iN7a>gSVfLKeCr$$Yb~v2qgq3P@YU
zKa&kxXG9ztnn`bG9p+6{LfEG6FaSH`o57b_ofR(MQKXi#XZ}^IfEBEB(ejkqcKyvq
zf$UwXGhDkJGrlD~C-8YI&L5uz{qj_|i+DZJM*EcNoG*-)TSv&LF+|y*Jc30zLa@KW
zeMh_@D2!}}-Vo3p_L&|ZMQ5zI35LXcrdssHe0%`^s0ks1@k^^Blbwtc?iH+ppL^yH
z8W9P0(kKKM+$b-OkGZ?Drbg<JsG4J=bpf8pYX~Mdl_;?ZYqJDodnOBkwVwk1SdH&=
zKcDar`})!Z!$L_|0vgMGI#NC8w}L_!t?n2#Y#BoIBHa@DcgaamwG$b*lw+4fH_bAU
zT>W!E1}}_=;%(d3$8_zl=BYVVzgi61wk$-}vGVG$f)yh+m^s<Nk!;6o=dGg~$)&P-
zebx56U<XCQ|HqIv`k@mrYeB_6e$dZ0nHsZxT`C|;dO@%xX6v5NbAeR{rB*V21t3SA
zY5zu<^;|(4`SzO<VKjFXBvaAzh*mPVaPvhAoeEgQ2Ik}{sD=rSEJ;YKWMo+C8PO&c
zt}RvD?&5CPO(55I7COe`1Vvvj3UBl%)gQq9tUfWB;`?TqeLr$&`$bTEgubP3u4RsB
z=ZsF?pLD2Pl~@F5=Uppi<vJYEK0MtX#Q=)mL9Kk1hWkqn!RAXX01gfUX*6x0C1KAi
z$JDeGn9J<WWaP;GkesJS-F>GE|1E^;#i;6@|9rWTt_bTRBA}br;jaJd9lka5i^_xY
z&ew?PM${uEKQpxSn<RBU7uu9XZqj(}QUmWq9J-i>DJ+pbO+ghGz;U80c8tIj89Wjq
z$xk0wOhew|#u!}ucJ5zoSkj&zi7cWdR$4^H^eJJPt=*t`ssV@;NH7=kB{-;fIh17j
z(|J}uNP8E#=F}ET87%EGP1>EF7rB4=r1!57q|U$Lh=)Ovdnm4+1Yd=<qPiJx+({x*
z)f&Wun1)6HFzhsPIbaeb6WHmT!{pFc6p@l#Dq_$}cZ)b;V1A2-8DGcR&O+fasSMO`
zS21E8y~~nGX^UZ5!G*UDI%R536RNFjE%Eqx{o)f<EV;UH-J{i$*Snc{pHGX`+^I;%
zc^!8Y6hSI7dBkg3)^xu4kMAb>6liXY2wbgL%?rM`R#!6Q2G4VZ#o4X^6>i}aDCc%m
z4k=SZ2%ULVahLQGZ$X@H<C!T+O=zs_sx%kfjy<iONT;>~0_cMP-}BCZ*){vIgOlN?
zi7GQYBO@X##pZ;|$VOaIo3Bj;zx4`N9zn(qx)gS7DTxKqEzyrz%(edjpuh4v40Ol&
zPQIYq(3s;vYKq{_x04s?5n2v)ftb1hZ~<K6q>Gq4Bj_kv8LIiD$gOd+!0Y?}*z0_e
zYnzF=apg!EsDJ(8FzfS_d84_V-UUGgcgm9U1Vu`USG2={1uf(OvV^4vB2v6~bgiB_
zbToAHSnXGldB8Z<!iRE<rUZ?aQbu<xRYupAGIt0`hQP18d6Vwe1z8shjH>+Vwu#)O
zz{r9u)g0QA$Yt^xHDF|!Q(NMoVvY?l`2{W9Cm7f+)wM6ov5qoK<j!-t_Ju84b$&rU
zDVMJ>M0Ll2E!>ceqfoZ3Z%GJVQB6=aXcDF{12U@X=^y7l^BFS<n17;SXHVCleDD3!
z@Q(YxF1wwtx9<>NJS4gD+7}(HH`v9LDUJsIRgNVt<&UR}IOvKA6)u8VYZp*2+wg&(
zL(zAy<>f|EB<w;7eI@&2Qk3#tXPqC-4}5b>j*=60)mpE8vbXUmV>z6|l2I`8dr6*a
zVWWfoR{9sqeTHKN*5r{gPIKm+$%5MzJ}M!!XvaF;4Evr;g=~4`g3o+$ZLHT(-)%m5
z{jEA{Q7FTT&-|#!Q^u3*nQ=Y$s}y%jX?~RWBi#%FqF1@ZHs%dtj|p|62fEm}s^aIJ
z7m`1Klj%QzI@c%{1c0I@OlR119E^oqum>5*WD}b)L%LIrSnojcxZiJX4(qYJ-Vg@H
zYmD0MJ}g8QD7@5m@n+@=?3sZWrnNm~ZEpLxJSoht4QwowyJ_Fq%fOS8c(6s#1wf>x
zX~cAuo1z<T$(bj845i00!nGCz{s7>}ID6a=%mJ7B(1J(+oe4_}hk{(8LRuvXtHdPj
zjs|y83%;US-pM<I4$||wmOF!t6TZBrfdr72GsQ)n0Gd&m3J%iQWee~b#eC`cSQqo%
zR!uMdhsX_JdtgilH{yj=+xMA+M)9e~7_2a!?Y5G3Ut9FhwUC6%zmK@K9UaDdpzz4w
z93k`^gZ1K}@;)Vy5BTXg(_O;hstU@7=JxhQGPt2#<nID%Q`D;urajU(d^H&#Pbmp!
zZ&kSfnjLbjQ{qc8a?VNQ(0OIdb$4*n*#l0Ot@_1D`~7K(ot??=<XI_`9u-RZiu-qe
z9Mi&(v{f<xMj7MxO>=(YXd#20QvaHy74{Xz((IthT^&H@V#}?iQDI4b5##e&z2N3&
zR#~{VzXv^i7t(l^N%aF8g&kw)H$ehtR8Go8IFAW`5BqxTL%-)uP_M5a!7`K;?7pS%
zMp#*6ghxi&9NU?b;ag}_b)7v(4+LW9-?y8yYsSCU2q>7Y7nIIX8=bBMn~9-d5@O;>
z#|eIku5FDXlk-0o?r*5-x}tNbr3C5YaSb(N&Oyi@n=5m+BgMzI+m&twMl4KzMkW>y
zd~r-7wxMAsF!wVk%h6Oqud|)%1V)q($bH7>-3oB0H=tsq0FD6S85xPJ@1H(COjyFj
zl=v^i6{N^b8aBSM6u>@~VQx+@?aU}c5#)UAogw%$PJi6t<;Q9OfMCSR)HmYcdupk7
ziX(IcwkA})8(yCFRw!gejdzf@htmzQAwJr8k(;$rmL@j>tbkBrLgKZ@FdTuKZoFIX
zt6U~ZU}0F)2DibYeJ4(>`JCx#5c!u6m4J_%Q$7FLt#s&XqCDEG9AG**4-u(+(@2Xq
z$T{=J>jQ(VC4aU`kkd!~&kiW7xEtfd`$DG2R84n~#RD#(VD&E4$#du{5y@;I9rXj^
z6t20IQN|E+v5G16U3pTIh&>zC&JabdG1LVl-1WTEVVfB=D3cAGBkfl<zv;>$NH8Ot
zr$p6v5dra?8CR+dJ4OVCqIee!^W$k0$N*IKL-hZrHvQ3_v3Bv_v?;`=HZAz8O*4bK
zH>8Oa-I7Inl}3*O3lhE*#pzo_=4tS&AweXipM-sSNUJ?)`2sg6yb6*D2DL`RB7aF|
zm3!2104Ef$bik8O%0u)#bKpLeV|fm2SYX|D=|Oy=fZ95S0tBO)^9rSt8ZT`H->07b
zt9i@I6*w5T%RT6;8EHRDIXRW(k}<#N>Z-0+*WStdWIJKyG~|5ZLS8AjN&z(US6*Ww
z0SkdoZ-R=?AAqnTBMQQC?0x3yPc;<u5XJwuD#rg&()j<m1E;__uzbnJ88kj>&eoee
z&O$*!Ard4Tfmp`Df=ClN5)mF8fCx8qab|w%y-vW57KkK4>6@Fq4EEx4S)WgN+}P?d
z#e$D8#amCKOM8HUD?=ctHom(P1=omXcT!RSCxkS42J$ZGzJj430qK{Uz4Glo__Cgq
zfp3bg_P%I1RJT+xQy}2EJSXbxLx}I@58xDL%T!GO%kxe0qMPZXHv2(L%sofP=v12!
zyFTl;w}5}S7h}WQ+vV70C6(`Y)jM4~fS-ri<04wuukeP=2)nQ<AU~5C%iYQugvyLv
zBgpekYPY8RD{0wr<0^RWMyUR~5#L#O_~qB;{>3JKh69qj^uLs5jVS*`S-Xn3)sEls
z(&xQ`g6TcSP<vm61p6%EOX&@wdZ%Fr^`Uuiw1~F(>&KnC9kk@dFq2?y&R;pp4gSiB
zeiQui^+BZUxO^4;?PjdI(xUTIPStaGKTor*MYheqa<=-0Ratr{j)MJWTY)Xf&$TqU
z9b@dO%Xtu2nUQVec|J%r(46unCFNUU`pX=q>Gn6*3M`U1<qXtOj-IcHz?pSPew5{B
z-3O!J=O}jZoCn!60UOaiHIEm$zr25}lE2-K<$m&x5kAgcrT$L`h2SjUb4CT|`~JT(
zmgKuz7TnG;3Vu$)LA0K=%JkMa7Wa1)ibZEF&&y&-u=dJb=2_{-{^HEHgJRvktZm$z
ziC2zrZ5NU;Y~f<dU8H|MpNSGyAyQECYu1Wkjme52P||bTZ*KbEe6hkL(<er84Wfbt
rYgj4bRC8`C(n@7*5HtU*O=)BZ5fdwu_)KH@cZ$vbx+vS=&&vM+0!~4C
literal 0
HcmV?d00001
diff --git a/doc/userman/changes.tex b/doc/userman/changes.tex
new file mode 100644
index 00000000..cf26227b
--- /dev/null
+++ b/doc/userman/changes.tex
@@ -0,0 +1,16 @@
+\chapter{Changes}\label{chap:changes}
+
+This chapter summarizes the changes in this documentation between each \fclang
+release, with the most recent releases first.
+
+\begin{itemize}
+\item New section \textbf{Additional Verifications}.
+\item Update each section with respect to the changes introduced since \eacsl
+ Sulfur-20180101.
+\end{itemize}
+
+\section*{Frama-C Chlorine-20180101}
+
+\begin{itemize}
+\item First release of this manual.
+\end{itemize}
diff --git a/doc/userman/description.tex b/doc/userman/description.tex
new file mode 100644
index 00000000..57288d32
--- /dev/null
+++ b/doc/userman/description.tex
@@ -0,0 +1,1146 @@
+The \fclang plug-in intends to provide a full translation of C++ and ACSL++ into the \framac internal representation, and from there be able to be analyzed by other \framac plug-ins. This is a work in progress. The following sections describe the limitations of the current implementation.
+\begin{itemize}
+ \item The plug-in aims for the TBD version of C++
+ \item \acslpp is described in the companion \acslpp reference manual, also a part of the \framac release.
+\end{itemize}
+
+
+Notes
+\begin{itemize}
+ \item Which version of Clang?
+ \item Clang (8) support C++98 (except exported templates, later removed) and C++11 and current draft standard for C++1y
+ \item see https://clang.llvm.org/docs/UsersManual.html\#cxx for supported features in clang C++
+\end{itemize}
+
+\chapter{Installation}
+
+TBD - installation instructions
+
+\chapter{Running the plug-in}
+
+TBD - including command-line options
+
+\chapter{Current implementation details and limitations}
+
+\section{Preprocessing}
+
+As a refresher, the C/C++ preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onlinedocs/cpp/}) conceptually implements the following operations on a C++ source file:
+\begin{itemize}
+ \item The input is read and broken it into a sequence of physical lines according to the line terminators (ASCII character sequences \\r, \\n, or \\r\\n).
+ \item Each C trigraph is replaced by its corresponding character.
+ \item Any backslash-whitespace-line-terminator sequence is removed and the line that it ends is combined with the following line.
+ \item Comments are replaced by single spaces. This requires tokenizing the input to avoid recognizing comment markers within strings as indicating a comment. Note that this allows block comments to hide line terminations.
+ \item The input text is divided into preprocessing tokens grouped in logical lines. Each preprocessor token becomes a compiler token (except where \#\# concatenation occurs). However, \acslb tokens are slightly different, as described below.
+ \item The source text is transformed according to any preprocessing directives contained within it. Each preprocessing directive must be contained within one logical line
+
+\end{itemize}
+The result is a sequence of preprocessing tokens that is passed on to the
+remaining compiler phases.
+
+\subsection{Trigraphs}
+
+TBD - are these supported by clang?
+
+\subsection{Preprocessor tokens}
+Preprocessor tokens (per CPP) belong to one of five categories. White space (space, tab, TBD) serves only to separate tokens; it is not needed between tokens whose concatenation is not a single token. Line terminators also separate tokens and also delineate certain features: preprocessing directives and string literals do not extend over more than one (logical) line.
+\begin{itemize}
+ \item identifiers: character sequences that match the regular expression \texttt{[a-zA-Z\_][a-zA-Z\_0-9]*} . Dollar signs are allowed as non-digit identifier characters if the clang option \texttt{-fdollars-in-identifiers} is used. (TBD - on by default?)
+ \item number: character sequences that match the regular expression \texttt{[.]?[0-9]([0-9a-zA-Z.]|[eEpP][+-]))*} . (TBD - dollar signs also allowed?)
+ \item string literals: character sequence enclosed in " " or ' ' or < >, with \textbackslash " for " in a double-quoted literal (that is not a header file name) and \' for ' in a single-quoted literal.
+ \item punctuator: all single non-alphanumeric printable characters except \@, \# and `, and all multi-punctuation sequences that meaningful to C/C++ (e.g. >>>= ), but not an arbitrary multi-punctuation character sequence.
+ \\item other tokens: \@, \#, ` and all non-ASCII single characters.
+\end{itemize}
+TBD - unicode characters
+Note that not all preprocessor tokens are valid C/C++ parser tokens. Tokens in the other category have no meaning to C/C++ and the \texttt{number} category allows many sequences that are not legal C/C++ numeric tokens. These tokens will generally provoke compiler errors. For example in C/C++, 0..2 is one token and is not interpreted as two consecutive numeric tokens.
+
+\acsl and \acslpp have slightly different tokens than the above, so the preprocessor tokens need to be re-tokenized in some cases:
+\begin{itemize}
+ \item The \@ token is a whitespace character in \acslb.
+ \item There are some \acslb multi-character punctuator tokens that are not
+ preprocessor tokens:
+ \begin{itemize}
+ \item[] $==>$ (logical implies)
+ \item[] $-->$ (bit-wise implies)
+ \item[] $<==>$ (logical equality)
+ \item[] $<-->$ (bit-wise equality)
+ \item[] TBD any more?
+ \end{itemize}
+ These ACSL/ACSL++ tokens need to be assembled from multiple CPP tokens (and those CPP tokens must not be separated by white space)
+ \item A CPP numeric token that contains .. will not be a legal C/C++ number, but may be multiple legal \acslb tokens with the .. representing the range operator. For example, the single CPP token \texttt{0..last} is retokenized for \acslb as if it were written \texttt{0 .. last} .
+ \item \acslb allows certain built-in non-ASCII symbols, namely
+ \begin{itemize}
+ \item[] $\forall$ (unicode 0x2200) - universal quantifier
+ \item[] $\exists$ (unicode 0x2203) - existential quantifier
+% \item[] $\equal$ (unicode 0x2261) - equality
+% \item[] $\notequal$ (unicode 0x2262) - inequality
+ \item[] $\leq$ (unicode 0x2264) - less than or equal
+ \item[] $\geq$ (unicode 0x2265) - greater than or equal
+% \item[] $\minus$ (unicode 0x2212) - minus
+% \item[] $\implies$ (unicode 0x21D2) - implies
+% \item[] $\equiv$ (unicode 0x21D4) - equivalence
+ \item[] $\bigwedge$ (unicode 0x2227) - logical and
+ \item[] $\bigvee$ (unicode 0x2228) - logical or
+ \item[] $\neg$ (unicode 0x00AC) - logical negation
+% \item[] $\logicalxor$ (unicode 0x22BB) - logical inequivalence
+ \item[] $\subset$ (unicode 0x2208) - subset
+% \item[] $\Boolean$ (unicode 0x1D539) - set of booleans
+% \item[] $\Integer$ (unicode 0x2124) - set of integers
+% \item[] $\Real$ (unicode 0x211D) - set of reals
+ \item TBD - more - ensure unicode equivalent
+ \end{itemize}
+\end{itemize}
+
+\subsection{Preprocessor directives}
+A preprocessing directive consists of a line (after the previous preprocessing phaseshave been completed) that begins with optional white space, the '\#' character, additional optional white space, and a preprocessor directive identifier.
+The preprocessing language contains a fixed set of preprocessing directive identifiers:
+\begin{itemize}
+ \item \texttt{define}, \texttt{undef}
+ \item \texttt{if}, \texttt{ifdef}, \texttt{ifndef}, \texttt{elif}, \texttt{else}, \texttt{endif}
+ \item \texttt{warning}, \texttt{error}
+ \item \texttt{include}
+ \item \texttt{line}
+ \item \texttt{pragma}
+\end{itemize}
+In addition, identifiers that have been defined (by a \#define directive) as macros are expanded according to the macro expansion rules (not described here).
+
+Now ACSL/ACSL++ annotations are contained in C/C++ comments.
+Consequently, any directives contained in the annotation are not seen when the source file is processed simply as a C/C++ source file. However, the effect of some directives lasts until the end of the source file.
+Accordingly, ACSL++ imposes constrains on the directives that may be present within annotations:
+\begin{itemize}
+ \item \texttt{define} and \texttt{undef} are not permitted in an annotation
+ \item \texttt{if}, \texttt{ifdef}, \texttt{ifndef}, \texttt{elif}, \texttt{else}, \texttt{endif} are permitted but must be completely nested within the annotation in which they appear (an \#endif and its corresponding \#if/\#ifdef/\#ifndef must be in the same annotation comment.)
+ \item \texttt{warning} and \texttt{error} are permitted
+ \item \texttt{include} is permitted, but will cause errors if it contains, as is almost always the case, either \texttt{define} or \texttt{pragma} directives
+ \item \texttt{line} - TBD
+ \item \texttt{pragma} is not permitted
+\end{itemize}
+
+
+
+\section{ACSL++ constructs}
+
+%This chapter is the core of this manual and describes how to use the \fclang
+%plug-in.
+
+
+%% You can still call the option \shortopt{e-acsl-help} to get the list of
+%% available options with few lines of documentation.
+%First, Section~\ref{sec:simple} shows how to run the plug-in on a toy example,
+%compile the generated code with the \gcc compiler and detect invalid
+%annotations at runtime. Further, Section~\ref{sec:wrapper} describes \eacslgcc\
+%-- a convenience wrapper script around \framac and \gcc. The aim of this script
+%is to simplify instrumentation and compilation of the instrumented code.
+%Section~\ref{sec:exec-env} gives additional details on the execution of the
+%generated code. Next, Section~\ref{sec:incomplete} focuses on how to deal with
+%incomplete programs, \emph{i.e.} in which some functions are not defined or in
+%which there are no main function. Section~\ref{sec:combine} explains how to
+%combine the \eacsl plug-in with other \framac plug-ins. Finally,
+%Section~\ref{sec:custom} introduces how to customize the plug-in, and
+%Section~\ref{sec:verbose} details the verbosing policy of the plug-in.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%\section{Simple Example} % <<<
+%\label{sec:simple}
+%
+%This section is a mini-tutorial which explains from scratch how to use the
+%\eacsl plug-in to detect whether an \eacsl annotation is violated at runtime.
+%
+%% All tool invocations and code listings shown in this section assume a Linux
+%% distribution with system-wide \framac installation.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Running \eacsl}
+%\label{sec:run}
+%
+%Consider the following program containing two \eacsl assertions such that
+%the first assertion is valid, whereas the second one is not.
+%
+%\listingname{first.i}
+%\cinput{examples/first.i}
+%
+%Running \eacsl on \texttt{first.i} consists of adding \shortopt{e-acsl} option
+%to the \framac command line:
+%\begin{shell}
+%\$ frama-c -e-acsl first.i
+%[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
+%[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+%[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+%[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+%[kernel] Parsing first.i (no preprocessing)
+%[e-acsl] beginning translation.
+%<skip a warning when translating the Frama-C libc>
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%Even though \texttt{first.i} has already been pre-processed, \eacsl first asks
+%the \framac kernel to process and combine it against several header files
+%provided by the \eacsl plug-in. Further \eacsl translates the annotated code
+%into a new \framac project named \texttt{e-acsl}\footnote{The notion of
+%\emph{project} is explained in Section 8.1 of the \framac user
+%manual~\cite{userman}.}. By default, the option \shortopt{e-acsl} does nothing
+%more. It is however possible to have a look at the generated code in the
+%\framac GUI. This is also possible through the command line thanks to the
+%kernel options \shortopt{then-last} and \shortopt{print}. The former
+%switches to the last generated project, while the latter pretty prints the \C
+%code~\cite{userman}:
+%
+%\input{examples/instrumented_first.c}
+%
+%As you can see, the generated code contains additional type declarations,
+%constant declarations and global \acsl annotations not present in the initial
+%file \texttt{first.i}. They are part of the \eacsl monitoring library. You can
+%safely ignore them for now. The translated \texttt{main} function of
+%\texttt{first.i} is displayed at the end. After each \eacsl annotation,
+%a call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert} has been added.
+%
+%\begin{minipage}{\linewidth}
+%\begin{ccode}
+% /*@ assert x == 0; */
+% __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
+% /*@ assert x == 1; */
+% __e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
+%\end{ccode}
+%\end{minipage}
+%
+%Each call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert}, function
+%defined by the \eacsl monitoring library, dynamically verifies the validity of
+%the corresponding assertion. In other words, it checks that its first argument
+%(here \texttt{x == 0} or \texttt{x == 1}) is not equal to 0 and fails
+%otherwise. The extra arguments are used to display error reports as shown in
+%Section~\ref{sec:exec}.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Executing the generated code}
+%\label{sec:exec}
+%
+%Using \shortopt{ocode} \framac~\cite{userman} option, the code generated by the
+%\eacsl plug-in can be redirected into a file as follows:
+%\begin{shell}
+%\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c
+%\end{shell}
+%
+%\framac uses architecture-dependent configuration which
+%affects sizes of integer types, endianness and potentially other features. It
+%can be seen that the code generated from \texttt{first.i} (shown in the
+%previous section) defines \C type \texttt{size\_t} as \texttt{unsigned int}, whereas
+%in 64-bit architectures \texttt{size\_t} is typically defined as
+%\texttt{unsigned long}. Architecture used during \framac translation is
+%controlled through \framac \shortopt{machdep} option that specifies the
+%architecture type to use during translation. The default value of
+%\shortopt{machdep} is \texttt{x86\_32} (a generic 32-bit x86 architecture).
+%Note that since code generated by \eacsl is aimed at being compiled it is
+%important that the architecture used by \framac matches the architecture
+%corresponding to your compiler and your system. For instance, in a 64-bit
+%machine you should also pass
+%\shortopt{machdep} \texttt{x86\_64} option as follows:
+%\begin{shell}
+% \$ frama-c -machdep x86_64 -e-acsl first.i -then-last \
+% -print -ocode monitored_first.c
+%\end{shell}
+%
+%This file can be compile with a \C compiler (for instance \gcc), as follows:
+%
+%\lstset{escapechar=£}
+%\begin{shell}
+%\$ gcc -c -Wno-attributes monitored_first.c
+%\end{shell}
+%
+%However, creating an executable through a proper invokation to \gcc is painful
+%and is not documented. Instead, \eacsl comes with a companion wrapper script for
+%this purpose.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{\eacsl Wrapper Script} % <<<
+%\label{sec:wrapper}
+%
+%\begin{important}\index{Gcc}
+% Presently, \eacslgcc is a recommended way of running the \eacsl plug-in.
+% This manual further describes features of the \eacsl plug-in using \eacslgcc
+% as its main driver for source code instrumentation and compilation of the
+% instrumented programs.
+%\end{important}
+%
+%In this section we describe \eacslgcc and provide several examples of its use.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Standard Usage}
+%
+%The default behaviour of \eacslgcc is to instrument an annotated C program
+%with runtime assertions via a run of \framac.
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -omonitored_first.i first.i
+%\end{shell}
+%
+%The above command instruments \texttt{first.i} with runtime assertions and
+%outputs the generated code to \texttt{monitored\_first.i}. Unless the name of
+%the output file is specified via the \shortopt{o} option (i.e.,
+%\shortopt{-omonitored\_first.i} in the above example), the generated
+%code is placed to a file named \texttt{a.out.frama.c}.
+%
+%Compilation and Linking of the original and the instrumented sources
+%is enabled using the \shortopt{c} option. For instance, command
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -omonitored_first.i first.i
+%\end{shell}
+%
+%instruments the code in \texttt{first.i}, outputs it to
+%\texttt{monitored\_first.i} and produces 2 executables: \texttt{a.out} and
+%\texttt{a.out.e-acsl}, such that \texttt{a.out} is an executable compiled from
+%\texttt{first.i}, while \texttt{a.out.e-acsl} is an executable compiled from
+%\texttt{monitored\_first.i} generated by \eacsl.
+%
+%You can execute the generate binaries, in particular \texttt{a.out.e-acsl} which
+%detects at runtime the incorrect annotation.
+%\begin{shell}
+%\$ ./a.out.e-acsl
+%Assertion failed at line 4 in function main.
+%The failing predicate is:
+%x == 1.
+%Aborted
+%\$ echo \$?
+%134
+%\end{shell}
+%The execution aborts with a non-zero exit code (134) and an error message
+%indicating \eacsl annotation that has been violated. There is no output for the
+%valid \eacsl annotation. That is, the run of an executable generated from the
+%instrumented source file (i.e., \texttt{monitored\_first.i}) detects that the
+%second annotation in the initial program is invalid, whereas the first
+%annotation holds for this execution.
+%
+%Named executables can be created using the \shortopt{O} option. This is such
+%that a value supplied to the \shortopt{O} option is used to name the executable
+%generated from the original program and the executable generated from the
+%\eacsl-instrumented code is suffixed \texttt{.e-acsl}.
+%
+%For example, command
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
+%\end{shell}
+%names the executables generated from \texttt{first.i} and
+%\texttt{monitored\_first.i}: \texttt{monitored\_first} and
+%\texttt{monitored\_first.e-acsl} respectively.
+%
+%The \eacslgcc \shortopt{C} option allows to skip the instrumentation step and
+%compile a given program as if it was already instrumented by the \eacsl
+%plug-in. This option is useful if one makes changes to an already
+%instrumented source file by hand and only wants to recompile it.
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
+%\end{shell}
+%
+%The above command generates a single executable named
+%\texttt{monitored\_first.e-acsl}. This is because \texttt{monitored\_first.i} is
+%considered to be instrumented code and thus no original program is provided.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Customising \framac and \gcc Invocations}
+%
+%By default \eacslgcc uses \T{frama-c} and \T{gcc} executables by looking them
+%up in a system's path. If either of the tools are not found the script fails
+%with an appropriate error message. Paths to \framac and \gcc executables can
+%also be passed using \shortopt{I} and \shortopt{G} options
+%respectively, for instance as follows:
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
+%\end{shell}
+%
+%Runs of \framac and \gcc issued by \eacslgcc can further be customized by using
+%additional flags. \framac flags can be passed using the \shortopt{F} option,
+%while \shortopt{l} and \shortopt{e} options allow for passing additional
+%pre-processor and linker flags during \gcc invocations. For example, command
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
+%\end{shell}
+%
+%yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
+%are output using the UTF-8 character set. Further, during the compilation of
+%\texttt{a.out.frama.c} \gcc adds directories \texttt{/bar} and
+%\texttt{/baz} to the list of directories to be searched for header files.
+%
+%It is worth mentioning that \eacslgcc implements several convenience flags for
+%setting some of the \framac options. For instance, \shortopt{E} can be used to
+%pass additional arguments to the \framac pre-processor (see
+%Section~\ref{sec:eacsl-gcc:doc}).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Verbosity Levels and Output Redirection}
+%
+%By default \eacslgcc prints the executed \framac and \gcc commands and pipes
+%their output to the terminal. The verbosity of \framac output can be changed
+%using \shortopt{v} and \shortopt{d} options used to pass values to
+%\shortopt{verbose} and \shortopt{debug} flags of \framac respectively. For
+%instance, to increase the verbosity of plug-ins but suppress the verbosity of
+%the \framac kernel while instrumenting \texttt{foo.c} one can use the following
+%command:
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
+%\end{shell}
+%
+%Verbosity of the \eacslgcc output can also be reduced using the \shortopt{q}
+%option that suppresses any output except errors or warnings issued by \gcc,
+%\framac, and \eacslgcc itself.
+%
+%The output of \eacslgcc can also be redirected to a specified file using the
+%\shortopt{s} option. For example, the following command redirects all
+%output during instrumentation and compilation of \texttt{foo.c} to the
+%file named \texttt{/tmp/log}.
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Architecture Dependency}
+%
+%As pointed out in Section~\ref{sec:exec} the execution of a \C program depends
+%on the underlying machine architecture it is executed on. The program must be
+%compiled on the very same architecture (or cross-compiled for it) for the
+%compiler being able to generate a correct binary.
+%
+%\framac makes assumptions about the machine architecture when analyzing source
+%code. By default, it assumes an X86 32-bit platform, but it can be customized
+%through \shortopt{machdep} switch~\cite{userman}. This option is of primary
+%importance when using the \eacsl plug-in: it must be set to the value
+%corresponding to the machine architecture which the generated code will be
+%executed on, otherwise the generated program is likely to fail to link against
+%the \eacsl library. Note that the library is built using the default
+%machine architecture.
+%
+%One of the benefits of using the wrapper script is that it makes sure that
+%\framac is invoked with the correct \shortopt{machdep} option. By default
+%\eacslgcc uses \shortopt{machdep gcc\_x86\_64} for 64-bit architectures and
+%\shortopt{machdep gcc\_x86\_32} for 32-bit ones. Compiler invocations are
+%further passed \shortopt{m64} or \shortopt{m32} options to generate code using
+%64-bit or 32-bit ABI respectively.
+%
+%At the present stage of implementation \eacsl does not support generating
+%executables with ABI different to the default one.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Documentation}\label{sec:eacsl-gcc:doc}
+%
+%For full up-to-date documentation of \eacslgcc see its man page:
+%
+%\begin{shell}
+% \$ man e-acsl-gcc.sh
+%\end{shell}
+%
+%Alternatively, you can also use the \shortopt{h} option of \eacslgcc:
+%
+%\begin{shell}
+% \$ man e-acsl-gcc.sh -h
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Execution Environment of the Generated Code} %<<<
+%\label{sec:exec-env}
+%
+%The environment in which the code is executed is not necessarily the same as
+%the one assumed by \framac. You should take care of that when running the \eacsl
+%plug-in and when compiling the generated code with \gcc. In this aspect, the
+%plug-in offers a few possibilities of customization.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Runtime Errors in Annotations}
+%\label{sec:runtime-error}
+%\index{Runtime Error}
+%
+%The major difference between \acsl~\cite{acsl} and \eacsl~\cite{eacsl}
+%specification languages is that the logic is total in the former while it is
+%partial in the latter one: the semantics of a logic construct $c$ denoting a \C
+%expression $e$
+%is undefined if $e$ leads to a runtime error and, consequently, the semantics of
+%any term $t$ (resp. predicate $p$) containing such a construct $c$ is
+%undefined as soon as $e$ has to be evaluated in order to evaluate $t$
+%(resp. $p$). The \eacsl Reference Manual also states that \emph{``it is the
+%responsibility of each tool which interprets \eacsl to ensure that an
+%undefined term is never evaluated''}~\cite{eacsl}.
+%
+%Accordingly, the \eacsl plug-in prevents an undefined term from being
+%evaluated. If an annotation contains such a term, \eacsl will report a proper
+%error at runtime instead of evaluating it.
+%
+%Consider for instance the following annotated program.
+%
+%\listingname{rte.i}
+%\cinput{examples/rte.i}
+%
+%The terms and predicates containing the modulo `\%' in the \T{assumes} clause
+%are undefined in the context of the \T{main} function call since the second
+%argument is equal to 0. However, we can generate an instrumented code and
+%compile it using the following command:
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c -omonitored_rte.i -Orte rte.i
+%\end{shell}
+%
+%Now, when \T{rte.e-acsl} is executed, you get the following output indicating
+%that your function contract is invalid because it contains a division by zero.
+%
+%\begin{shell}
+%\$ ./rte.e-acsl
+%RTE failed at line 5 in function is_dividable.
+%The failing predicate is:
+%division_by_zero: y != 0.
+%Aborted
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Libc}\index{Libc}
+%
+%By default, \framac uses its own standard library (\emph{aka} libc) instead of
+%the one of your system. If you do not want to use it, you have to add the option
+%\shortopt{no-framac-stdlib}\optionidx{-}{framac-stdlib} to the \framac command
+%line.
+%
+%It might be particularly useful in one of the following contexts:
+%\begin{itemize}
+%\item several libc functions used by the analyzed program are still not defined
+% in the \framac libc; or
+%\item your system libc and the \framac libc mismatch about several function
+% types (for instance, your system libc is not 100\% POSIX compliant); or
+%\item several \framac lib functions get a contract and you are not interested in
+% verifying them (for instance, only checking undefine behaviors matters).
+%\end{itemize}
+%
+%\begin{important} \index{eacslgcc}
+%Notably, \eacslgcc disables \framac libc by default. This is because most of
+%its functions are annotated with \eacsl contracts and generating code for
+%these contracts results in additional runtime overheads. To enforce default
+%\framac contracts with \eacslgcc you can pass \shortopt{L} option to the wrapper
+%script.
+%\end{important}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Integers}
+%\label{sec:integers}
+%\index{GMP}
+%
+%\eacsl uses an \texttt{integer}\codeidx{integer} type corresponding to
+%mathematical integers which does not fit in any integral \C type. To circumvent
+%this issue, \eacsl uses the \gmp library\footnote{\url{http://gmplib.org}}.
+%Thus, even if \eacsl does its best to use standard integral types instead of
+%\gmp~\cite{sac13,jfla15}, it may generate such integers from time to time. It is
+%notably the case if your program contains \lstinline|long long|, either signed
+%or unsigned.
+%
+%Consider for instance the following program.
+%
+%\listingname{gmp.i}
+%\cinput{examples/gmp.i}
+%
+%Even on a 64-bit machine, it is not possible to compute the assertion with a
+%standard \C type. In this case, the \eacsl plug-in generates \gmp code. Note
+%that E-ACSL library already includes \gmp, thus no additional arguments need to
+%be provided. We can generate and execute the instrumented code as usual via
+%the following command:
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -omonitored_gmp.i -Ogmp gmp.i
+%\$ ./gmp.e-acsl
+%\end{shell}
+%
+%Since the assertion is valid, there is no output in this case.
+%
+%Note that it is possible to use \gmp arithmetic in all cases (even if not
+%required). This option is controlled through \shortopt{g} switch of \eacslgcc
+%which passes the \shortopt{e-acsl-gmp-only} option to the \eacsl
+%plug-in. However it could slow down the execution of the instrumented program
+%significantly.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Memory-related Annotations}
+%\label{sec:memory}
+%
+%The \eacsl plug-in handles memory-related annotations such as
+%\lstinline|\valid|. Consider for instance the following program.
+%
+%\listingname{valid.c}
+%\cinput{examples/valid.c}
+%
+%Even though the first annotation holds, the second annotation (labelled
+%\I{freed}) is invalid. This is because at the point of its execution memory
+%allocated via \texttt{malloc} has been deallocated and \T{x} is a stale pointer
+%referencing unallocated memory. The execution of the instrumented program thus
+%reports the violation of the second annotation:
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c -Ovalid valid.c
+%\$ ./valid.e-acsl
+%Assertion failed at line 11 in function main.
+%The failing predicate is:
+%freed: \valid(x).
+%Aborted
+%\end{shell}
+%
+%To check memory-related predicates (such as \lstinline|\valid|) \eacsl tracks
+%memory allocated by a program at runtime. \eacsl records memory blocks in a
+%meta-storage tracking each block's boundaries (i.e., its base address and
+%length), per-byte initialization and the notion of an address being freeable
+%(i.e., whether it can be safely passed to the \texttt{free} function). During
+%an execution of the instrumented program code injected by \eacsl
+%transformations queries the meta-storage to identify properties of an address
+%in question. For instance, during the execution of the above program the
+%monitor injected by \eacsl first records information about the memory block
+%allocated via a call to \texttt{malloc}. Further, during the execution of the
+%first assertion the monitor queries the meta-storage about the address of the
+%memory location pointed to by \texttt{x}. Since the location belongs to an
+%allocated memory block, the meta-storage identifies it as belonging to the
+%tracked allocation. Consequently, the assertion evaluates to true and the
+%monitors allows the execution to continue. The second assertion, however,
+%fails. This is because the block pointed to by \T{x} has been removed from the
+%meta-storage by a call to \T{free}, and thus a meta-storage query identifies
+%location \T{x} as belonging unallocated memory space.
+%
+%\subsubsection{\eacsl Memory Models}
+%
+%Memory tracking implemented by the \eacsl library comes in two flavours dubbed
+%\I{bittree-based} and \I{segment-based} memory models. With the bittree-based
+%model meta-storage is implemented as a compact prefix trie called Patricia
+%trie~\cite{rv13}, whereas segment-based memory model
+%\footnote{Segment-based model of \eacsl has not yet appeared in the literature.}
+%is based on shadow memory~\cite{pldi16}. The functionality of the provided
+%memory models is equivalent, however they differ in performance. We further
+%discuss performance considerations.
+%
+%The \eacsl models allocate heap memory using a customized version of the
+%\dlmalloc\footnote{\url{http://dlmalloc.net/}} memory allocator replacing
+%system-wide \T{malloc} and similar functions (e.g., \T{calloc} or \T{free}).
+%
+%At the level of \eacslgcc you can choose between different memory models using
+%the \shortopt{m} switch followed by the name of the memory model to link
+%against. For instance, command
+%\begin{shell}
+%\$ e-acsl-gcc.sh -mbittree -c -Ovalid valid.c
+%\end{shell}
+%links a program generated from \T{valid.c} against the library implementing the
+%bittree-based memory model, whereas the following invocation uses shadow-based
+%tracking:
+%\begin{shell}
+%\$ e-acsl-gcc.sh -msegment -c -Ovalid valid.c
+%\end{shell}
+%It is also possible to generate executables using both models as follows:
+%\begin{shell}
+%\$ e-acsl-gcc.sh -msegment,bittree -c -Ovalid valid.c
+%\end{shell}
+%In this case, \eacslgcc produces 3 executables: \T{valid},
+%\T{valid.e-acsl-segment} and \T{valid.e-acsl-bittree} corresponding to an
+%executable generated from the original source code, and the executables
+%generated from the \eacsl-instrumented sources linked against
+%segment-based and bittree-based memory models.
+%
+%Unless specified, \eacsl defaults to the segment-based memory model.
+%
+%\subsubsection{Performance Considerations}
+%\label{sec:perf}
+%
+%As pointed out in the previous section the functionalities provided by both
+%segment-based and bittree-based memory models are equivalent but differ in
+%performance. The bittree-based model uses compact memory representation of
+%metadata. The segment-based model on the other hand uses significantly more
+%memory. You can expect over 2x times memory overheads when using it. However It
+%is often an order of magnitude faster than the bittree-based
+%model~\cite{pldi16}.
+%
+%%[Need ref here with comparison of the performance. Ideally a reference to the PLDI paper].
+%
+%\subsubsection{Maximized Memory Tracking}
+%
+%By default \eacsl uses static analysis to reduce instrumentation and therefore
+%runtime and memory overheads~\cite{scp16}. With respect to memory tracking this
+%means that
+%\eacsl may omit recording memory blocks irrelevant for runtime analysis. It
+%is, however, still possible to systematically instrument the code for handling
+%potential memory-related annotations even when it is not required. This
+%feature can be enabled using the \shortopt{M} switch of \eacslgcc or
+%\shortopt{e-acsl-full-mmodel} option of the \eacsl plug-in.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% \subsection{Debug Libraries}
+%%% \label{sec:runtime-debug}
+%
+%%% \eacsl memory models mentioned in Section~\ref{sec:memory} are optimized for
+%%% performance (via \shortopt{-O2} compiler flag). An \eacsl installation also
+%%% provides unoptimized versions of these libraries (suffixed \T{-dbg.a}) aimed at
+%%% being used during debugging.
+%
+%%% The main difference between unoptimized (debug) and optimized (production)
+%%% libraries is that debug libraries include assertions validating the correctness
+%%% of the RTL itself. For instance, during memory tracking such assertions ensure
+%%% that during a run of a program all tracked memory blocks are disjoint.
+%
+%%% Consider the following program that violates an annotation
+%%% in function \T{foo} via a call \T{bar(p+1)} in the main function:
+%
+%%% \listingname{rte\_debug.i}
+%%% \cinput{examples/rte_debug.i}
+%
+%%% A monitored executable linked against a debug version of \eacsl RTL
+%%% can ge generated using
+%%% \longopt{rt-debug} flag of \eacslgcc as follows:
+%
+%%% \begin{shell}
+%%% \$ e-acsl-gcc.sh --rt-debug -c -omonitored_rte_debug.c -Orte_debug rte_debug.i
+%%% \end{shell}
+%
+%%% A run of the monitored executable shows violation of the \eacsl annotation.
+%%% \begin{shell}
+%%% \$ rte_debug.e-acsl
+%%% Assertion failed at line 2 in function foo.
+%%% The failing predicate is:
+%%% \valid(p).
+%%% /** Backtrace **************************/
+%%% trace at e_acsl_trace.h:45
+%%% - exec_abort at e_acsl_assert.h:58
+%%% - runtime_assert at e_acsl_assert.h:93
+%%% - foo at monitored_rte_debug.c:92
+%%% - bar at monitored_rte_debug.c:102
+%%% - main at monitored_rte_debug.c:119
+%%% /***************************************/
+%%% Aborted
+%%% \end{shell}
+%
+%%% A run of an executable linked against an unoptimized RTL shows a stack trace on
+%%% the instrumented program saved to \T{monitored\_rte\_debug.c}. In the example
+%%% above calls to \T{exec\_abort} and \T{runtime\_assert} belong to the \eacsl
+%%% RTL, whereas calls to \T{foo}, \T{bar} and \T{main} belong to the input
+%%% program.
+%
+%%% It should be noted that because debug versions of \eacsl RTL are compiled
+%%% without compile-time optimizations and execute additional assertions the
+%%% runtime overheads of the instrumented programs linked against the debug
+%%% versions of \eacsl RTL can be up to 10 times greater than those linked against
+%%% the production versions.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Runtime Monitor Behavior}
+%
+%When a predicate is checked at runtime function
+%\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} is called. By
+%default this function does nothing if the predicate is valid, and prints
+%an error message and aborts the execution (by raising an \texttt{ABORT}
+%signal via a call to the \C function \texttt{abort}) if the predicate is invalid.
+%
+%The default behavior of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
+%can be altered using \longopt{fail-with-code=CODE} option of \eacslgcc
+%that uses \texttt{exit(CODE)} instead of \texttt{abort}.
+%
+%For instance, the program generated using the following command
+%exits with code \texttt{5} on a predicate violation.
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
+%\end{shell}
+%
+%Forceful termination of a monitored program can be disabled using
+%\longopt{keep-going} option. If specified, \eacslgcc generates code that
+%reports each property violated at runtime but allows the monitored program to
+%continue execution. \longopt{keep-going} should be used with caution:
+%such unterminated executions may lead to incorrect verification results.
+%
+%\eacslgcc also provides a way to use an alternative definition of
+%\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}.
+%
+%Custom implementation of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
+%should be provided in a separate \C (or object file) and respect the
+%following signature:
+%
+%\cinput{examples/assert_sign.c}
+%
+%Below is an example which prints the validity status of each property but never
+%exits.
+%
+%\listingname{my\_assert.c}
+%\cinput{examples/my_assert.c}
+%
+%A monitored program that uses custom definition of
+%\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} can then be generated
+%as follows using \longopt{external-assert} option of \eacslgcc to replace the
+%default implementation of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
+%with the customized one specified in \texttt{my\_assert.c}
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c first.i my_assert.c -Ofirst --external-assert=my\_assert.c
+%\$ ./first.e-acsl
+%Assertion at line 3 in function main is valid.
+%The verified predicate was: `x == 0'.
+%Assertion at line 4 in function main is invalid.
+%The verified predicate was: `x == 1'.
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Additional Verifications} % <<<
+%
+%In addition to checking annotations at runtime, \eacsl is able to detect a few
+%errors at runtime.
+%
+%\subsection{Format String Vulnerabilities}
+%\index{Format String Vulnerabilities}
+%
+%Whenever option \longopt{validate-format-strings} of \eacslgcc is set, \eacsl
+%detects format-string vulnerabilities in \texttt{printf}-like function. Below is
+%an example which incorrectly tries to print a string through a \texttt{\%d}
+%format.
+%
+%\listingname{printf.c}
+%\cinput{examples/printf.c}
+%
+%This error can be detected by \eacsl as follows.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings printf.c
+%\$ ./printf.e-acsl
+%printf: directive 1 ('%d') expects argument of type 'int' but the corresponding
+%argument has type 'char*'
+%Abort
+%\end{shell}
+%
+%\subsection{Incorrect Usage of Libc Functions}
+%\index{Libc}
+%
+%Whenever option \longopt{libc-replacements} of \eacslgcc is set, \eacsl is
+%able to detect incorrect usage of the following libc functions:
+%\begin{itemize}
+%\item \texttt{memcmp}
+%\item \texttt{memcpy}
+%\item \texttt{memmove}
+%\item \texttt{memset}
+%\item \texttt{strcat}
+%\item \texttt{strncat}
+%\item \texttt{strcmp}
+%\item \texttt{strcpy}
+%\item \texttt{strncpy}
+%\item \texttt{strlen}
+%\end{itemize}
+%
+%For instance, the program below incorrectly uses \texttt{strcpy} because the
+%destination string should contain at least 7 \texttt{char} (and not only 6).
+%
+%\listingname{strcpy.c}
+%\cinput{examples/strcpy.c}
+%
+%This error can be reported by \eacsl as follows.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -Ostrcpy -c --libc-replacements strcpy.c
+%\$ ./strcpy.e-acsl
+%strlen: insufficient space in destination string, at least 7 bytes required
+%Abort
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Incomplete Programs} % <<<
+%\label{sec:incomplete}
+%
+%Executing a \C program requires to have a complete application. However, the
+%\eacsl plug-in does not necessarily require to have it to generate the
+%instrumented code. It is still possible to instrument a partial program with no
+%entry point or in which some functions remain undefined.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Programs without Main}
+%\label{sec:no-main}
+%\index{Program!Without main}
+%
+%The \eacsl plug-in can instrument a program without the \T{main} function.
+%Consider for instance the following annotated program without \texttt{main}.
+%
+%\listingname{no\_main.i}
+%\cinput{examples/no_main.i}
+%
+%The instrumented code is generated as usual, even though you get an additional
+%warning.
+%\begin{shell}
+%\$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
+%<skip preprocessing command line>
+%[e-acsl] beginning translation.
+%[e-acsl] warning: cannot find entry point `main'.
+% Please use option `-main' for specifying a valid entry point.
+% The generated program may miss memory instrumentation.
+% if there are memory-related annotations.
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%This warning indicates that the instrumentation could be incorrect if the
+%program contains memory-related annotations (see
+%Section~\ref{sec:limits:no-main}). That is not the case here, so you can
+%safely ignore it. Now, it is possible to compile the generated code with a \C
+%compiler in a standard way, and even link it against additional files such as
+%the following:
+%
+%\listingname{main.c}
+%\cinput{examples/main.c}
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -C monitored_no_main.i main.c -Owith_main
+%\$ ./with_main.e-acsl
+%x = 65536
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\
+%\subsection{Undefined Functions}
+%\label{sec:no-code}
+%\index{Function!Undefined}
+%
+%Similar to the above section \eacsl is capable of instrumenting a program which
+%has definitions of arbitrary functions missing. Consider for instance the
+%following annotated program for which the implementation of the function
+%\texttt{my\_pow} is not provided.
+%
+%\listingname{no\_code.c}
+%\cinput{examples/no_code.c}
+%
+%The instrumented code is generated as usual, even though you get an additional
+%warning.
+%\begin{shell}
+%\$ e-acsl-gcc.sh -omonitored_no_code.i no_code.c
+%[e-acsl] beginning translation.
+%[e-acsl] warning: annotating undefined function `my_pow':
+% the generated program may miss memory instrumentation
+% if there are memory-related annotations.
+%no_code.c:9:[kernel] warning: No code nor implicit assigns clause for function my_pow,
+%generating default assigns from the prototype
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%Similar to the previous Section the warning indicates that the instrumentation
+%could be incorrect if the program contains memory-related annotations (see
+%Section~\ref{sec:limits:no-code}). That is still not the case here, so you can
+%safely ignore it.
+%
+%\listingname{pow.i}
+%\cinput{examples/pow.i}
+%
+%Similar to the example shown in the previous section you can generate the
+%executable by providing definition of \T{my\_pow}.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i
+%\$ ./no_code.e-acsl
+%Postcondition failed at line 5 in function my_pow.
+%The failing predicate is:
+%\old(n % 2 == 0) ==> \result >= 1.
+%Aborted
+%\end{shell}
+%
+%The execution of the corresponding binary fails at runtime: actually, our
+%implementation of the function \texttt{my\_pow} overflows in case of large
+%exponentiations.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Combining E-ACSL with Other Plug-ins} % <<<
+%\label{sec:combine}
+%
+%As the \eacsl plug-in generates a new \framac project, it is easy to run any
+%plug-in on the generated program, either in the same \framac session (thanks to
+%the option \shortopt{then} or through the GUI), or in another one. The only
+%issue might be that, depending on the plug-in, the analysis may be imperfect if
+%the generated program uses \gmp or the dedicated memory library: both make
+%intensive use of dynamic structures which are usually difficult to handle by
+%analysis tools.
+%
+%Another way to combine \eacsl with other plug-ins is to run \eacsl last. For
+%instance, the \rte plug-in~\cite{rte} may be used to generate annotations
+%corresponding to runtime errors. Then the \eacsl plug-in may generate an
+%instrumented program to verify that there are no such runtime errors during the
+%execution of the program.
+%
+%Consider the following program.
+%
+%\listingname{combine.i}
+%\cinput{examples/combine.i}
+%To check at runtime that this program does not perform any runtime error (which
+%are potential overflows in this case), just do:
+%
+%\begin{shell}
+%\$ frama-c -rte combine.i -then -e-acsl -then-last -print
+% -ocode monitored_combine.i
+%\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.i
+%\$ ./combine.
+%\end{shell}
+%
+%Automatic assertion generation can also be enabled via \eacslgcc directly via
+%the following command:
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all
+%\end{shell}
+%
+%Note the use of \eacslgcc \longopt{rte} option which asks \framac to combine
+%\eacsl with \rte plug-in. This plug-in automatically instruments the input
+%program with runtime
+%assertions before running the \eacsl plug-in on it. \longopt{rte} option of
+%\eacslgcc also accepts a comma-separated list of arguments indicating the types
+%of assertions to generate. Consult the \eacslgcc man page for a detailed
+%list of arguments accepted by \longopt{rte}.
+%
+%The present implementation of \eacslgcc does not fully support combining \eacsl
+%with other \framac plug-ins. However it is still possible to instrument programs
+%with \eacsl directly and use \eacslgcc to compile the generated code.
+%
+%If you run the \eacsl plug-in after another one, it first generates
+%a new temporary project in which it links the analyzed program against its own
+%library in order to generate the \framac internal representation of the \C
+%program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
+%even if the \eacsl plug-in keeps the maximum amount of information, the results
+%of already executed analyzers (such as validity status of annotations) are not
+%known in this new project. If you want to keep them, you have to set the option
+%\shortopt{e-acsl-prepare} when the first analysis is asked for.
+%
+%In this context, the \eacsl plug-in does not generate code for annotations
+%proven valid by another plug-in, except if you explicitly set the option
+%\shortopt{e-acsl-valid}. For instance, \Eva~\cite{eva} is able to
+%prove that there is no potential overflow in the previous program, so the \eacsl
+%plug-in does not generate additional code for checking them if you run the
+%following command.
+%\begin{shell}
+%\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+% -then-last -print -ocode monitored_combine.i
+%\end{shell}
+%The additional code will be generated with one of the two following commands.
+%\begin{shell}
+%\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+% -e-acsl-valid -then-last -print -ocode monitored_combine.i
+%\$ frama-c -rte combine.i -then -val -then -e-acsl \
+% -then-last -print -ocode monitored_combine.i
+%\end{shell}
+%In the first case, that is because it is explicitly required by the option
+%\shortopt{e-acsl-valid} while, in the second case, that is because the option
+%\shortopt{e-acsl-prepare} is not provided on the command line which results in
+%the fact that the result of the value analysis are unknown when the \eacsl
+%plug-in is running.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Customization} % <<<
+%\label{sec:custom}
+%
+%There are several ways to customize the \eacsl plug-in.
+%
+%First, the name of the generated project -- which is \texttt{e-acsl} by default
+%-- may be changed by setting the option \shortopt{e-acsl-project} option of the
+%\eacsl plug-in. While there is not direct support for this option in \eacslgcc
+%you can pass it using \shortopt{F} switch:
+%
+%\listingname{check.i}
+%\cinput{examples/check.i}
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i
+%<skip preprocessing commands>
+%[e-acsl] beginning translation.
+%check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
+% Ignoring annotation.
+%[e-acsl] translation done in project "foobar".
+%\end{shell}
+%
+%Further, the \eacsl plug-in option \shortopt{e-acsl-check} does not generate a
+%new project but verifies that each annotation is translatable. Then it produces
+%a summary as shown in the following example (left or right shifts in annotations
+%are not yet supported by the \eacsl plug-in~\cite{eacsl-implem}).
+%
+%\begin{shell}
+%\$ frama-c -e-acsl-check check.i
+%<skip preprocessing commands>
+%check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
+% Ignoring annotation.
+%[e-acsl] 0 annotation was ignored, being untypable.
+%[e-acsl] 1 annotation was ignored, being unsupported.
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Verbosity Policy} % <<<
+%\label{sec:verbose}
+%
+%By default, \eacsl does not provide much information when it is running. Mainly,
+%it prints a message when it begins the translation, and another one when the
+%translation is done. It may also display warnings when something requires the
+%attention of the user, for instance if it is not able to translate an
+%annotation. Such information is usually enough but, in some cases, you might
+%want to get additional control on what is displayed. As quite usual with
+%\framac plug-ins, \eacsl offers two different ways to do this: the verbosity
+%level which indicates the \emph{amount} of information to display, and the
+%message categories which indicate the \emph{kind} of information to display.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Verbosity Level}
+%
+%The amount of information displayed by the \eacsl plug-in is settable by the
+%option \shortopt{e-acsl-verbose}. It is 1 by default. Below is indicated
+%which information is displayed according to the verbosing level. The level $n$
+%also displays the information of all the lower levels.
+%
+%\begin{center}
+%\begin{tabular}{|l|l|}
+%\hline
+%\shortopt{e-acsl-verbose 0}& only warnings and errors\\
+%\hline
+%\shortopt{e-acsl-verbose 1}& beginning and ending of the translation\\
+%\hline
+%\shortopt{e-acsl-verbose 2}& different parts of the translation and
+% functions-related information\\
+%\hline
+%\shortopt{e-acsl-verbose 3}& predicates- and statements-related information\\
+%\hline
+%\shortopt{e-acsl-verbose 4}& terms- and expressions-related information
+%\\
+%\hline
+%\end{tabular}
+%\end{center}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Message Categories}
+%
+%The kind of information to display is settable by the option
+%\shortopt{e-acsl-msg-key} (and unsettable by the option
+%\shortopt{e-acsl-msg-key-unset}). The different keys refer to different
+%parts of the translation, as detailed below.
+%
+%\begin{center}
+%\begin{tabular}{|l|l|}
+%\hline
+%analysis & minimization of the instrumentation for memory-related annotation
+%(section~\ref{sec:memory}) \\
+%\hline
+%duplication & duplication of functions with contracts
+%(section~\ref{sec:no-code}) \\
+%\hline
+%translation & translation of an annotation into \C code\\
+%\hline
+%typing & minimization of the instrumentation for integers
+%(section~\ref{sec:integers}) \\
+%\hline
+%\end{tabular}
+%\end{center}
+% >>>
diff --git a/doc/userman/eacslversion.tex b/doc/userman/eacslversion.tex
new file mode 100644
index 00000000..921e0d99
--- /dev/null
+++ b/doc/userman/eacslversion.tex
@@ -0,0 +1,2 @@
+\newcommand{\eacslversion}{Chlorine-20180501+dev\xspace}
+\newcommand{\fcversion}{Chlorine\xspace}
diff --git a/doc/userman/fclangversion.tex b/doc/userman/fclangversion.tex
new file mode 100644
index 00000000..b542d412
--- /dev/null
+++ b/doc/userman/fclangversion.tex
@@ -0,0 +1,2 @@
+\newcommand{\fclangversion}{Chlorine+\xspace}
+\newcommand{\fcversion}{Chlorine+\xspace}
diff --git a/doc/userman/introduction.tex b/doc/userman/introduction.tex
new file mode 100644
index 00000000..809a738b
--- /dev/null
+++ b/doc/userman/introduction.tex
@@ -0,0 +1,26 @@
+\chapter{Introduction}
+
+\framac~\cite{userman,fac15} is a modular analysis framework for the C
+programming language which supports the \acsl specification
+language~\cite{acsl}. This manual documents the \fclang plug-in of \framac,
+version \fclangversion.
+The \fclang plug-in supports the \acslpp extension of \acsl for C++ programs and specifications;
+it is built on the Clang\footnote{https://clang.llvm.org/} compiler infrastructure and uses Clang for
+parsing C++.
+
+%The \fclang version you are using is indicated by the
+%command \texttt{frama-c -e-acsl-version}\optionidx{-}{e-acsl-version}. \fclang
+%automatically translates an annotated C program into another program that fails
+%at runtime if an annotation is violated. If no annotation is violated, the
+%behavior of the new program is exactly the same as the one of the original
+%program.
+
+
+%This manual does \emph{not} explain how to install the \eacsl plug-in. For
+%installation instructions please refer to the \texttt{INSTALL} file in the
+%\eacsl distribution. \index{Installation} Furthermore, even though this manual
+%provides examples, it is \emph{not} a full comprehensive tutorial on
+%\framac or \eacsl.
+
+% You can still refer to any external
+% tutorial~\cite{rv13tutorial} for additional examples.
diff --git a/doc/userman/limitations.tex b/doc/userman/limitations.tex
new file mode 100644
index 00000000..29097433
--- /dev/null
+++ b/doc/userman/limitations.tex
@@ -0,0 +1,188 @@
+\chapter{Known Limitations}
+
+The development of the \fclang plug-in is still ongoing.
+%First, the \eacsl
+%reference manual~\cite{eacsl} is not yet fully supported. Which annotations can
+%already be translated into \C code and which cannot is defined in a separate
+%document~\cite{eacsl-implem}. Second, even though we do our best to avoid them,
+%bugs may exist. If you find a new one, please report it on the bug tracking
+%system\footnote{\url{http://bts.frama-c.com}} (see Chapter 10 of the \framac
+%User Manual~\cite{userman}). Third, there
+%are some additional known limitations, which could be annoying for the user in
+%some cases, but are tedious to lift. Please contact us if you are interested in
+%lifting these limitations\footnote{Read \url{http://frama-c.com/support.html}
+% for additional details.}.
+
+%\section{Uninitialized Values}
+%\index{Uninitialized value}
+%
+%As explained in Section~\ref{sec:runtime-error}, the \eacsl plug-in should never
+%translate an annotation into \C code which can lead to a runtime error. This is
+%enforced, except for uninitialized values which are values read before having
+%been written.
+%
+%\listingname{uninitialized.i}
+%\cinput{examples/uninitialized.i}
+%
+%If you generate the instrumented code, compile it, and finally execute it, you
+%may get no runtime error depending on your \C compiler, but the behavior is
+%actually undefined because the assertion reads the uninitialized variable
+%\lstinline|x|. You should be caught by the \eacsl plug-in, but that is not
+%the case yet.
+%\begin{shell}
+%
+%\$ e-acsl-gcc.sh uninitialized.i -c -Omonitored_uninitialized
+%monitored_uninitialized.i: In function 'main':
+%monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function
+%[-Wuninitialized]
+%\$ ./monitored_uninitialized.e-acsl
+%\end{shell}
+%
+%This is more a design choice than a limitation: should the \eacsl plug-in
+%generate additional instrumentation to prevent such values from being evaluated,
+%the generated code would be much more verbose and slower.
+%
+%If you really want to track such uninitializations in your annotation, you have
+%to manually add calls to the \eacsl predicate
+%\lstinline|\initialized|~\cite{eacsl}.
+%
+%\section{Incomplete Programs}
+%
+%Section~\ref{sec:incomplete} explains how the \eacsl plug-in is able to handle
+%incomplete programs, which are either programs without main, or programs
+%containing undefined functions (\emph{i.e.} functions without body).
+%
+%However, if such programs contain memory-related annotations, the generated code
+%may be incorrect. That is made explicit by a warning displayed when the \eacsl
+%plug-in is running (see examples of Sections~\ref{sec:no-main} and
+%\ref{sec:no-code}).
+%
+%\subsection{Programs without Main}
+%\index{Program!Without main}
+%\label{sec:limits:no-main}
+%
+%The instrumentation in the generated program is partial for every program
+%without main containing memory-related annotations, except if the option
+%\optionuse{-}{e-acsl-full-mmodel} or the \eacsl plug-in (of \shortopt{M} option
+%of \eacslgcc) is provided. In that case, violations of such annotations are
+%undetected.
+%
+%Consider the following example.
+%
+%\listingname{valid\_no\_main.c}
+%\cinput{examples/valid_no_main.c}
+%
+%You can generate the instrumented program as follows.
+%\begin{shell}
+%\$ e-acsl-gcc.sh -ML -omonitored_valid_no_main.i valid_no_main.c
+%<skip preprocessing commands>
+%[e-acsl] beginning translation.
+%<skip warnings about annotations from the Frama-C libc
+% which cannot be translated>
+%[kernel] warning: no entry point specified:
+% you must call function `__e_acsl_memory_init' by yourself.
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%The last warning states an important point: if this program is linked against
+%another file containing \texttt{main} function, then this main function must
+%be modified to insert a call to the function \texttt{\_\_e\_acsl\_memory\_init}
+%\index{e\_acsl\_memory\_init@\texttt{\_\_e\_acsl\_memory\_init}} at the very
+%beginning. This function plays a very important role: it initializes metadata
+%storage used for tracking of memory blocks. Unless this call is inserted the
+%run of a modified program is likely to fail.
+%
+%While it is possible to add such intrumentation manually we recommend using
+%\eacslgcc. Consider the following incomplete program containing \T{main}:
+%
+%\listingname{modified\_main.c}
+%\cinput{examples/modified_main.c}
+%
+%Then just compile and run it as explained in Section~\ref{sec:memory}.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
+%\$ e-acsl-gcc.sh -C -Ovalid_no_main monitored_modified_main.i monitored_valid_no_main.i
+%\$ ./valid_no_main.e-acsl
+%Assertion failed at line 11 in function f.
+%The failing predicate is:
+%freed: \valid(x).
+%Aborted
+%\end{shell}
+%
+%Also, if the unprovided main initializes some variables, running the
+%instrumented code (linked against this main) could print some warnings from the
+%\eacsl memory library\footnote{see
+% \url{https://bts.frama-c.com/view.php?id=1696} for an example}.
+%
+%\subsection{Undefined Functions}
+%\label{sec:limits:no-code}
+%\index{Function!Undefined}
+%
+%The instrumentation in the generated program is partial for a program $p$ if and
+%only if $p$ contains a memory-related annotation $a$ and an undefined function
+%$f$ such that:
+%\begin{itemize}
+%\item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
+%\item or $a$ is one of the post-conditions of $f$.
+%\end{itemize}
+%A violation of such an annotation $a$ is undetected. There is no workaround yet.
+%
+%Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
+%undefined functions. There is also no workaround yet.
+%
+%\section{Recursive Function}
+%\index{Function!Recursive}
+%
+%Programs containing recursive functions have the same limitations as the ones
+%containing undefined functions (Section~\ref{sec:limits:no-code}) and
+%memory-related annotations.
+%
+%%% JS: this issue should have been fixed:
+%%% Also, even though there is no such annotations, the generated code may call a
+%%% function before it is declared. When this behavior appears remains
+%%% unspecifed. The generated code is however easy to fix by hand.
+%
+%\section{Variadic Functions}
+%\index{Function!Variadic}
+%
+%Programs containing undefined variadic functions with contracts
+%are not yet supported. Using the \variadic plug-in of \framac could be a
+%solution in some cases, but its generated code cannot always be compiled.
+%
+%\section{Function Pointers}
+%\index{Function!Pointer}
+%
+%Programs containing function pointers have the same limitations on
+%memory-related annotations as the ones containing undefined or recursive
+%functions.
+%
+%\section{Requirements to Input Programs}
+%\index{Function!Input}
+%
+%\subsection{\eacsl Namespace}
+%While \eacsl uses source-to-source transformations and not binary
+%instrumentations it is important that the source code provided at input does
+%not contain any variables or functions prefixed \T{\_\_e\_acsl\_}. \eacsl
+%reserves this namespace for its transformations, and therefore an input program
+%containing such symbols beforehand may fail to be instrumented or compiled.
+%
+%\subsection{Memory Management Functions}
+%Programs providing custom definitions of \T{syscall}, \T{mmap} or
+%\T{sbrk} should be rejected. Also, an input programs should not modify
+%memory-management functions namely \T{malloc}, \T{calloc}, \T{realloc},
+%\T{free}, \T{cfree}, \T{posix\_memalign} and \T{aligned\_alloc}. \eacsl relies
+%on these functions in order to track heap memory. Further, correct heap memory
+%monitoring requires to limit allocation and deallocation of heap memory to
+%POSIX-compliant memory management functions
+%listed above. Monitoring of programs that allocate memory using non-standard or
+%obsolete functions (e.g., \T{valloc}, \T{memalign}, \T{pvalloc}) may not work
+%correctly.
+%
+%\section{Limitations of E-ACSL Monitoring Libraries}
+%\index{Function!Libraries}
+%
+%\eacsl monitoring library implementing segment-based memory model is fairly
+%recent and presently has very limited support for 32-bit architectures. When
+%using a 32-bit machine we recommend using the bittree-based memory model
+%instead.
diff --git a/doc/userman/macros.tex b/doc/userman/macros.tex
new file mode 100644
index 00000000..e92cba83
--- /dev/null
+++ b/doc/userman/macros.tex
@@ -0,0 +1,295 @@
+%%% Environnements dont le corps est suprimé, et
+%%% commandes dont la définition est vide,
+%%% lorsque PrintRemarks=false
+
+\usepackage{comment}
+
+\newcommand{\framac}{\textsc{Frama-C}\xspace}
+\newcommand{\acsl}{\textsc{ACSL}\xspace}
+\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
+
+\newcommand{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
+\newcommand{\rte}{\textsc{RTE}\xspace}
+\newcommand{\C}{\textsc{C}\xspace}
+\newcommand{\jml}{\textsc{JML}\xspace}
+\newcommand{\Eva}{\textsc{Eva}\xspace}
+\newcommand{\variadic}{\textsc{Variadic}\xspace}
+\newcommand{\wpplugin}{\textsc{Wp}\xspace}
+\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
+\newcommand{\gcc}{\textsc{Gcc}\xspace}
+\newcommand{\gmp}{\textsc{GMP}\xspace}
+\newcommand{\dlmalloc}{\textsc{dlmalloc}\xspace}
+
+\newcommand{\nodiff}{\emph{No difference with \acsl.}}
+\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
+\newcommand{\limited}[1]{\emph{Limited to #1.}}
+\newcommand{\absent}{\emph{No such feature in \eacsl.}}
+\newcommand{\absentwhy}[1]{\emph{No such feature in \eacsl: #1.}}
+\newcommand{\absentexperimental}{\emph{No such feature in \eacsl, since it is
+ still experimental in \acsl.}}
+\newcommand{\absentexcept}[1]{\emph{No such feature in \eacsl, but #1.}}
+\newcommand{\difficultwhy}[2]{\emph{#1 is usually difficult to implement, since
+ it requires #2. Thus you would not wonder if most tools do not support it
+ (or support it partially).}}
+\newcommand{\difficultswhy}[2]{\emph{#1 are usually difficult to implement,
+ since they require #2. Thus you would not wonder if most tools do not
+ support them (or support them partially).}}
+\newcommand{\difficult}[1]{\emph{#1 is usually difficult to implement. Thus
+ you would not wonder if most tools do not support it (or support
+ it partially).}}
+\newcommand{\difficults}[1]{\emph{#1 are usually difficult to implement. Thus
+ you would not wonder if most tools do not support them (or support
+ them partially).}}
+
+\newcommand{\changeinsection}[2]{\textbf{Section \ref{sec:#1}:} #2.}
+
+\newcommand{\todo}[1]{{\large \textbf{TODO: #1.}}}
+
+\newcommand{\markdiff}[1]{{\color{blue}{#1}}}
+\newenvironment{markdiffenv}[1][]{%
+ \begin{changebar}%
+ \markdiff\bgroup%
+}%
+{\egroup\end{changebar}}
+
+% true = prints remarks for the ACSL working group.
+% false = prints no remark for the distributed version of ASCL documents
+\newboolean{PrintRemarks}
+\setboolean{PrintRemarks}{false}
+
+% true = prints marks signaling the state of the implementation
+% false = prints only the ACSL definition, without remarks on implementation.
+\newboolean{PrintImplementationRq}
+\setboolean{PrintImplementationRq}{true}
+
+% true = remarks about the current state of implementation in Frama-C
+% are in color.
+% false = they are rendered with an underline
+\newboolean{ColorImplementationRq}
+\setboolean{ColorImplementationRq}{true}
+
+%% \ifthenelse{\boolean{PrintRemarks}}%
+%% {\newenvironment{todo}{%
+%% \begin{quote}%
+%% \begin{tabular}{||p{0.8\textwidth}}TODO~:\itshape}%
+%% {\end{tabular}\end{quote}}}%
+%% {\excludecomment{todo}}
+
+\ifthenelse{\boolean{PrintRemarks}}%
+ {\newenvironment{remark}[1]{%
+ \begin{quote}\itshape%
+ \begin{tabular}{||p{0.8\textwidth}}Remarque de {#1}~:}%
+ {\end{tabular}\end{quote}}}%
+ {\excludecomment{remark}}
+
+\newcommand{\oldremark}[2]{%
+\ifthenelse{\boolean{PrintRemarks}}{%
+ %\begin{quote}\itshape%
+ %\begin{tabular}{||p{0.8\textwidth}}Vieille remarque de {#1}~: #2%
+ %\end{tabular}\end{quote}%
+}%
+{}}
+
+\newcommand{\highlightnotreviewed}{%
+\color{blue}%
+}%
+
+\newcommand{\notreviewed}[2][]{%
+\ifthenelse{\boolean{PrintRemarks}}{%
+ \begin{changebar}%
+ {\highlightnotreviewed #2}%
+ \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
+ \end{changebar}%
+}%
+{}}
+
+\ifthenelse{\boolean{PrintRemarks}}{%
+\newenvironment{notreviewedenv}[1][]{%
+ \begin{changebar}%
+ \highlightnotreviewed%
+ \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
+ \bgroup}%
+ {\egroup%
+ \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}}%
+{\excludecomment{notreviewedenv}}
+
+%%% Commandes et environnements pour la version relative à l'implementation
+\newcommand{\highlightnotimplemented}{%
+\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
+ {\ul}%
+}%
+
+\newcommand{\notimplemented}[2][]{%
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{changebar}%
+ {\highlightnotimplemented #2}%
+ \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
+ \end{changebar}%
+}%
+{#2}}
+
+\newenvironment{notimplementedenv}[1][]{%
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{changebar}%
+ \highlightnotimplemented%
+ \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
+ \bgroup
+}{}}%
+{\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \egroup%
+ \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}{}}
+
+%%% Environnements et commandes non conditionnelles
+\newcommand{\experimental}{\textsc{Experimental}}
+
+\newsavebox{\fmbox}
+\newenvironment{cadre}
+ {\begin{lrbox}{\fmbox}\begin{minipage}{0.98\textwidth}}
+ {\end{minipage}\end{lrbox}\fbox{\usebox{\fmbox}}}
+
+
+\newcommand{\keyword}[1]{\lstinline|#1|\xspace}
+\newcommand{\keywordbs}[1]{\lstinline|\\#1|\xspace}
+
+\newcommand{\integer}{\keyword{integer}}
+\newcommand{\real}{\keyword{real}}
+\newcommand{\bool}{\keyword{boolean}}
+
+\newcommand{\assert}{\keyword{assert}}
+\newcommand{\terminates}{\keyword{terminates}}
+\newcommand{\assume}{\keyword{assume}}
+\newcommand{\requires}{\keyword{requires}}
+\newcommand{\ensures}{\keyword{ensures}}
+\newcommand{\exits}{\keyword{exits}}
+\newcommand{\returns}{\keyword{returns}}
+\newcommand{\breaks}{\keyword{breaks}}
+\newcommand{\continues}{\keyword{continues}}
+\newcommand{\assumes}{\keyword{assumes}}
+\newcommand{\assigns}{\keyword{assigns}}
+\newcommand{\reads}{\keyword{reads}}
+\newcommand{\decreases}{\keyword{decreases}}
+
+\newcommand{\boundseparated}{\keywordbs{bound\_separated}}
+\newcommand{\Exists}{\keywordbs{exists}~}
+\newcommand{\Forall}{\keywordbs{forall}~}
+\newcommand{\bslambda}{\keywordbs{lambda}~}
+\newcommand{\freed}{\keywordbs{freed}}
+\newcommand{\fresh}{\keywordbs{fresh}}
+\newcommand{\fullseparated}{\keywordbs{full\_separated}}
+\newcommand{\distinct}{\keywordbs{distinct}}
+\newcommand{\Max}{\keyword{max}}
+\newcommand{\nothing}{\keywordbs{nothing}}
+\newcommand{\numof}{\keyword{num\_of}}
+\newcommand{\offsetmin}{\keywordbs{offset\_min}}
+\newcommand{\offsetmax}{\keywordbs{offset\_max}}
+\newcommand{\old}{\keywordbs{old}}
+\newcommand{\at}{\keywordbs{at}}
+
+\newcommand{\If}{\keyword{if}~}
+\newcommand{\Then}{~\keyword{then}~}
+\newcommand{\Else}{~\keyword{else}~}
+\newcommand{\For}{\keyword{for}~}
+\newcommand{\While}{~\keyword{while}~}
+\newcommand{\Do}{~\keyword{do}~}
+\newcommand{\Let}{\keywordbs{let}~}
+\newcommand{\Break}{\keyword{break}}
+\newcommand{\Return}{\keyword{return}}
+\newcommand{\Continue}{\keyword{continue}}
+
+\newcommand{\exit}{\keyword{exit}}
+\newcommand{\main}{\keyword{main}}
+\newcommand{\void}{\keyword{void}}
+
+\newcommand{\struct}{\keyword{struct}}
+\newcommand{\union}{\keywordbs{union}}
+\newcommand{\inter}{\keywordbs{inter}}
+\newcommand{\typedef}{\keyword{typedef}}
+\newcommand{\result}{\keywordbs{result}}
+\newcommand{\separated}{\keywordbs{separated}}
+\newcommand{\sizeof}{\keyword{sizeof}}
+\newcommand{\strlen}{\keywordbs{strlen}}
+\newcommand{\Sum}{\keyword{sum}}
+\newcommand{\valid}{\keywordbs{valid}}
+\newcommand{\validrange}{\keywordbs{valid\_range}}
+\newcommand{\offset}{\keywordbs{offset}}
+\newcommand{\blocklength}{\keywordbs{block\_length}}
+\newcommand{\baseaddr}{\keywordbs{base\_addr}}
+\newcommand{\comparable}{\keywordbs{comparable}}
+
+\newcommand{\N}{\ensuremath{\mathbb{N}}}
+\newcommand{\ra}{\ensuremath{\rightarrow}}
+\newcommand{\la}{\ensuremath{\leftarrow}}
+
+% BNF grammar
+\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
+\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
+\newif\ifspace
+\newif\ifnewentry
+\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
+\newcommand{\term}[2]{\addspace\hbox{\lstinline|#1|%
+\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
+\newcommand{\nonterm}[2]{%
+ \ifthenelse{\equal{#2}{}}%
+ {\addspace\hbox{\textsl{#1}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}%
+ {\addspace\hbox{\textsl{#1}\footnote{#2}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}}
+\newcommand{\repetstar}{$^*$\spacetrue}
+\newcommand{\repetplus}{$^+$\spacetrue}
+\newcommand{\repetone}{$^?$\spacetrue}
+\newcommand{\lparen}{\addspace(}
+\newcommand{\rparen}{)}
+\newcommand{\orelse}{\addspace$\mid$\spacetrue}
+\newcommand{\sep}{ \\[2mm] \spacefalse\newentrytrue}
+\newcommand{\newl}{ \\ & & \spacefalse}
+\newcommand{\alt}{ \\ & $\mid$ & \spacefalse}
+\newcommand{\is}{ & $::=$ & \newentryfalse}
+\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
+\newcommand{\synt}[1]{$\spacefalse#1$}
+\newcommand{\emptystring}{$\epsilon$}
+\newcommand{\below}{See\; below}
+
+% colors
+
+\definecolor{darkgreen}{rgb}{0, 0.5, 0}
+
+% theorems
+
+\newtheorem{example}{Example}[chapter]
+
+% for texttt
+
+\newcommand{\bs}{\ensuremath{\backslash}}
+
+% Index
+
+\newcommand{\optionidx}[2]{\index{#2@\texttt{#1#2}}}
+\newcommand{\codeidx}[1]{\index{#1@\texttt{#1}}}
+\newcommand{\scodeidx}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}}}
+\newcommand{\sscodeidx}[3]{%
+ \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}}}
+\newcommand{\bfit}[1]{\textbf{\textit{\hyperpage{#1}}}}
+\newcommand{\optionidxdef}[2]{\index{#2@\texttt{#1#2}|bfit}}
+\newcommand{\codeidxdef}[1]{\index{#1@\texttt{#1}|bfit}}
+\newcommand{\scodeidxdef}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}|bfit}}
+\newcommand{\sscodeidxdef}[3]{%
+ \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}|bfit}}
+
+\newcommand{\pragmadef}[1]{\texttt{#1}\index{Pragma!#1@\texttt{#1}}}
+\newcommand{\optiondef}[2]{\texttt{#1#2}\optionidxdef{#1}{#2}}
+\newcommand{\textttdef}[1]{\texttt{#1}\codeidxdef{#1}}
+
+\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
+\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
+\newcommand{\shortopt}[1]{\optionuse{-}{#1}}
+\newcommand{\longopt}[1]{\optionuse{{-}{-}}{#1}}
+% Shortcuts for truetype, italic and bold
+\newcommand{\T}[1]{\texttt{#1}}
+\newcommand{\I}[1]{\textit{#1}}
+\newcommand{\B}[1]{\textbf{#1}}
+
+\definecolor{gris}{gray}{0.85}
+\makeatletter
+\newenvironment{important}%
+{\hspace{5pt plus \linewidth minus \marginparsep}%
+ \begin{lrbox}{\@tempboxa}%
+ \begin{minipage}{\linewidth - 2\fboxsep}}
+{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
diff --git a/doc/userman/main.tex b/doc/userman/main.tex
new file mode 100644
index 00000000..5fe5621a
--- /dev/null
+++ b/doc/userman/main.tex
@@ -0,0 +1,99 @@
+\documentclass[web]{frama-c-book}
+
+\usepackage{graphicx}
+\usepackage{calc}
+\usepackage{datetime}
+\newdateformat{ddMyyyydate}{\THEDAY~\monthname[\THEMONTH]~\THEYEAR}
+
+
+
+\include{macros}
+\newcommand{\fclang}{\textsc{Frama-Clang}\xspace}
+\newcommand{\acslpp}{\textsc{ACSL++}\xspace}
+\newcommand{\acslb}{\acsl/acslpp\xspace}
+\include{fclangversion}
+
+
+\makeindex
+
+\begin{document}
+
+\coverpage{\fclang User Manual}
+
+\begin{titlepage}
+\begin{flushleft}
+\includegraphics[height=14mm]{cealistlogo.jpg}
+\end{flushleft}
+\vfill
+\title{\fclang Plug-in}{Release \fclangversion
+%% \ifthenelse{\equal{\eacslversion}{\fcversion}}{}{%
+%% \\[1em] compatible with \framac \fcversion}
+}
+\author{David R. Cok}
+\begin{center}
+CEA LIST\\ Software Reliability \& Security Laboratory
+\end{center}
+\begin{center}
+ Last modified \ddMyyyydate\today
+\end{center}
+\vfill
+\begin{flushleft}
+ \textcopyright 2013-2018 CEA LIST
+%%
+ %% This work has been supported by the VESSEDIA project).
+\end{flushleft}
+\end{titlepage}
+
+\tableofcontents
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\chapter*{Foreword}
+\markright{}
+\addcontentsline{toc}{chapter}{Foreword}
+
+This is the user manual of the \framac plug-in
+\fclang\footnote{\url{https://frama-c.com/frama-clang.html}}. The contents of this
+document correspond to its version \fclangversion compatible with
+\fcversion version of \framac~\cite{userman,fac15}. The development of
+the \fclang plug-in is still ongoing. Features described by this document may
+evolve in the future.
+
+\section*{Acknowledgements}
+
+We gratefully thank the people who contributed to this document:
+David R. Cok, Virgile Prevosto, Armand Pucetti, Franck Verdrine.
+
+TBD-VESSEDIA
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\include{introduction}
+\include{description}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\appendix
+
+\include{changes}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\bibname}
+\bibliographystyle{plain}
+\bibliography{./biblio}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%% \cleardoublepage
+%% \addcontentsline{toc}{chapter}{\listfigurename}
+%% \listoffigures
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\indexname}
+\printindex
+
+\end{document}
--
GitLab