diff --git a/doc/userman/Makefile b/doc/userman/Makefile
index 5715ebd8a719d259d25ccf05637ab7f6761936b7..433971360454eaafc0c43dccfe11c4a15f044b5e 100644
--- a/doc/userman/Makefile
+++ b/doc/userman/Makefile
@@ -9,7 +9,7 @@ TARGET = userman
###########
-.PHONY: all install clean
+.PHONY: all install clean $(TARGET).pdf
ifneq ($(VERBOSEMAKE),no)
SILENT =
diff --git a/doc/userman/analysis-scripts.graphml b/doc/userman/analysis-scripts.graphml
new file mode 100644
index 0000000000000000000000000000000000000000..2c798633e54136b20090b02b064c625b8167cfdc
--- /dev/null
+++ b/doc/userman/analysis-scripts.graphml
@@ -0,0 +1,516 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:java="http://www.yworks.com/xml/yfiles-common/1.0/java" xmlns:sys="http://www.yworks.com/xml/yfiles-common/markup/primitives/2.0" xmlns:x="http://www.yworks.com/xml/yfiles-common/markup/2.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:y="http://www.yworks.com/xml/graphml" xmlns:yed="http://www.yworks.com/xml/yed/3" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://www.yworks.com/xml/schema/graphml/1.1/ygraphml.xsd">
+ <!--Created by yEd 3.19-->
+ <key attr.name="Description" attr.type="string" for="graph" id="d0"/>
+ <key for="port" id="d1" yfiles.type="portgraphics"/>
+ <key for="port" id="d2" yfiles.type="portgeometry"/>
+ <key for="port" id="d3" yfiles.type="portuserdata"/>
+ <key attr.name="url" attr.type="string" for="node" id="d4"/>
+ <key attr.name="description" attr.type="string" for="node" id="d5"/>
+ <key for="node" id="d6" yfiles.type="nodegraphics"/>
+ <key for="graphml" id="d7" yfiles.type="resources"/>
+ <key attr.name="url" attr.type="string" for="edge" id="d8"/>
+ <key attr.name="description" attr.type="string" for="edge" id="d9"/>
+ <key for="edge" id="d10" yfiles.type="edgegraphics"/>
+ <graph edgedefault="directed" id="G">
+ <data key="d0"/>
+ <node id="n0">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="158.0" x="178.625" y="278.3519359999999"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="78.15992736816406" x="39.92003631591797" xml:space="preserve" y="20.88001251220703">Sources<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n1">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="158.0" x="537.625" y="369.8519359999999"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="128.73983764648438" x="14.630081176757812" xml:space="preserve" y="20.88001251220703">GNUmakefile<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n2">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="158.0" x="178.625" y="369.8519359999999"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="58.479949951171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="155.1798553466797" x="1.4100723266601562" xml:space="preserve" y="7.2600250244140625">Preprocessing
+flags (-I, -D, etc.)<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n3">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="122.0" width="158.0" x="178.625" y="461.3519359999999"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="112.95989990234375" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="129.1798553466797" x="14.410072326660156" xml:space="preserve" y="4.520050048828125">Machdep
+(architecture,
+compiler,
+OS)<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n4" yfiles.foldertype="group">
+ <data key="d4" xml:space="preserve"/>
+ <data key="d5"/>
+ <data key="d6">
+ <y:ProxyAutoBoundsNode>
+ <y:Realizers active="0">
+ <y:GroupNode>
+ <y:Geometry height="214.97755415112294" width="160.4375" x="909.0787925720215" y="172.41297124133297"/>
+ <y:Fill color="#F5F5F5" transparent="false"/>
+ <y:BorderStyle color="#000000" type="dashed" width="1.0"/>
+ <y:NodeLabel alignment="right" autoSizePolicy="node_width" backgroundColor="#EBEBEB" borderDistance="0.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="internal" modelPosition="t" textColor="#000000" verticalTextPosition="bottom" visible="true" width="160.4375" x="0.0" xml:space="preserve" y="0.0"><target>.parse </y:NodeLabel>
+ <y:Shape type="roundrectangle"/>
+ <y:State closed="false" closedHeight="50.0" closedWidth="50.0" innerGraphDisplayEnabled="false"/>
+ <y:Insets bottom="5" bottomF="5.0" left="5" leftF="5.0" right="5" rightF="5.0" top="5" topF="5.0"/>
+ <y:BorderInsets bottom="4" bottomF="4.176845465453994" left="0" leftF="0.0" right="0" rightF="0.0" top="0" topF="0.0"/>
+ </y:GroupNode>
+ <y:GroupNode>
+ <y:Geometry height="237.0" width="295.0" x="1056.0625" y="257.95187343896475"/>
+ <y:Fill color="#F5F5F5" transparent="false"/>
+ <y:BorderStyle color="#000000" type="dashed" width="1.0"/>
+ <y:NodeLabel alignment="right" autoSizePolicy="node_width" backgroundColor="#EBEBEB" borderDistance="0.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="internal" modelPosition="t" textColor="#000000" verticalTextPosition="bottom" visible="true" width="295.0" x="0.0" xml:space="preserve" y="0.0">target.parse</y:NodeLabel>
+ <y:Shape type="roundrectangle"/>
+ <y:State closed="true" closedHeight="237.0" closedWidth="295.0" innerGraphDisplayEnabled="false"/>
+ <y:Insets bottom="5" bottomF="5.0" left="5" leftF="5.0" right="5" rightF="5.0" top="5" topF="5.0"/>
+ <y:BorderInsets bottom="0" bottomF="0.0" left="0" leftF="0.0" right="0" rightF="0.0" top="0" topF="0.0"/>
+ </y:GroupNode>
+ </y:Realizers>
+ </y:ProxyAutoBoundsNode>
+ </data>
+ <graph edgedefault="directed" id="n4:">
+ <node id="n4::n0">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="149.71875" x="914.0787925720215" y="210.92671559558102"/>
+ <y:Fill color="#99CCFF" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="77.54753875732422" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="149.71875" x="0.0" xml:space="preserve" y="-2.2737693786621094">parse.log
+warnings.log
+metrics.log<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n4::n1">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="26.0" width="150.4375" x="914.0787925720215" y="289.5767781566162"/>
+ <y:Fill color="#CCFFCC" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="28.515846252441406" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="150.4375" x="0.0" xml:space="preserve" y="-1.2579231262207031">framac.ast<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n4::n2">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="26.0" width="150.4375" x="914.0787925720215" y="350.9557568007812"/>
+ <y:Fill color="#FFCC99" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="28.515846252441406" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="150.4375" x="0.0" xml:space="preserve" y="-1.2579231262207031">stats.txt<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n4::n3">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="26.0" width="150.4375" x="914.0787925720215" y="320.0767781566162"/>
+ <y:Fill color="#FFFF99" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="28.515846252441406" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="150.4375" x="0.0" xml:space="preserve" y="-1.2579231262207031">framac.sav<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ </graph>
+ </node>
+ <node id="n5" yfiles.foldertype="group">
+ <data key="d4" xml:space="preserve"/>
+ <data key="d5"/>
+ <data key="d6">
+ <y:ProxyAutoBoundsNode>
+ <y:Realizers active="0">
+ <y:GroupNode>
+ <y:Geometry height="254.93886947631842" width="159.0" x="909.7975425720215" y="426.6656832358396"/>
+ <y:Fill color="#F5F5F5" transparent="false"/>
+ <y:BorderStyle color="#000000" type="dashed" width="1.0"/>
+ <y:NodeLabel alignment="right" autoSizePolicy="node_width" backgroundColor="#EBEBEB" borderDistance="0.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="internal" modelPosition="t" textColor="#000000" verticalTextPosition="bottom" visible="true" width="159.0" x="0.0" xml:space="preserve" y="0.0"><target>.eva </y:NodeLabel>
+ <y:Shape type="roundrectangle"/>
+ <y:State closed="false" closedHeight="50.0" closedWidth="50.0" innerGraphDisplayEnabled="false"/>
+ <y:Insets bottom="5" bottomF="5.0" left="5" leftF="5.0" right="5" rightF="5.0" top="5" topF="5.0"/>
+ <y:BorderInsets bottom="0" bottomF="0.0" left="0" leftF="0.0" right="0" rightF="0.0" top="1" topF="1.171266470703074"/>
+ </y:GroupNode>
+ <y:GroupNode>
+ <y:Geometry height="237.0" width="295.0" x="873.25" y="-81.45989990234375"/>
+ <y:Fill color="#F5F5F5" transparent="false"/>
+ <y:BorderStyle color="#000000" type="dashed" width="1.0"/>
+ <y:NodeLabel alignment="right" autoSizePolicy="node_width" backgroundColor="#EBEBEB" borderDistance="0.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="internal" modelPosition="t" textColor="#000000" verticalTextPosition="bottom" visible="true" width="295.0" x="0.0" xml:space="preserve" y="0.0">target.parse</y:NodeLabel>
+ <y:Shape type="roundrectangle"/>
+ <y:State closed="true" closedHeight="237.0" closedWidth="295.0" innerGraphDisplayEnabled="false"/>
+ <y:Insets bottom="5" bottomF="5.0" left="5" leftF="5.0" right="5" rightF="5.0" top="5" topF="5.0"/>
+ <y:BorderInsets bottom="0" bottomF="0.0" left="0" leftF="0.0" right="0" rightF="0.0" top="0" topF="0.0"/>
+ </y:GroupNode>
+ </y:Realizers>
+ </y:ProxyAutoBoundsNode>
+ </data>
+ <graph edgedefault="directed" id="n5:">
+ <node id="n5::n0">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="123.69433229296885" width="149.0" x="914.7975425720215" y="465.51937416674775"/>
+ <y:Fill color="#99CCFF" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="126.57923126220703" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="149.0" x="0.0" xml:space="preserve" y="-1.4424494846191465">alarms.csv
+eva.log
+warnings.log
+metrics.log
+nonterm.log
+<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n5::n1">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="49.75" width="149.0" x="914.7975425720215" y="625.2137064597166"/>
+ <y:Fill color="#FFCC99" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="53.03169250488281" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="149.0" x="0.0" xml:space="preserve" y="-1.6408462524414062">flamegraph.txt
+stats.txt<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n5::n2">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="26.0" width="149.0" x="914.7975425720215" y="594.2137064597166"/>
+ <y:Fill color="#FFFF99" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="28.515846252441406" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="149.0" x="0.0" xml:space="preserve" y="-1.2579231262207031">framac.sav<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ </graph>
+ </node>
+ <node id="n6">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="158.0" x="1189.5" y="449.40174831689444"/>
+ <y:Fill color="#FFCC99" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="58.479949951171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="148.71983337402344" x="4.640083312988281" xml:space="preserve" y="7.2600250244140625">Benchmarking/
+Profiling<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n7">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="158.0" x="1189.5" y="243.40174831689444"/>
+ <y:Fill color="#CCFFCC" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="58.479949951171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="135.59983825683594" x="11.200080871582031" xml:space="preserve" y="7.2600250244140625">Pretty-printed
+C source<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n8">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="158.0" x="1189.5" y="346.40174831689444"/>
+ <y:Fill color="#99CCFF" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="58.479949951171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="131.81983947753906" x="13.090080261230469" xml:space="preserve" y="7.2600250244140625">Analysis logs/
+Results<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n9">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="239.0" x="941.7975425720215" y="720.8797105555417"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="188.07977294921875" x="25.460113525390625" xml:space="preserve" y="20.88001251220703">Open results in GUI<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n10">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="73.0" width="177.0" x="1180.0" y="552.4017483168944"/>
+ <y:Fill color="#FFFF99" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="58.479949951171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="169.69981384277344" x="3.6500930786132812" xml:space="preserve" y="7.2600250244140625">Saved state
+(Frama-C session)<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <node id="n11">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="93.0" width="284.0" x="178.625" y="601.8519359999999"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="85.71992492675781" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="264.419677734375" x="9.7901611328125" xml:space="preserve" y="3.6400375366210938">(Optional)
+JSON Compilation Database
+(compile_commands.json)<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
+ <edge id="e0" source="n0" target="n1">
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="0.0" sy="0.0" tx="13.179599999999596" ty="1.600377541666603">
+ <y:Point x="364.0" y="314.8519359999999"/>
+ <y:Point x="364.0" y="407.9523135416665"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" hasText="false" height="4.0" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="4.0" x="166.88603870451527" y="91.10038483072901">
+ <y:LabelModel>
+ <y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/>
+ </y:LabelModel>
+ <y:ModelParameter>
+ <y:SmartEdgeLabelModelParameter angle="6.283185307179586" distance="11.207369976486891" distanceToCenter="false" position="center" ratio="0.8492785518650576" segment="-1"/>
+ </y:ModelParameter>
+ <y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/>
+ </y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e1" source="n1" target="n4">
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="60.5703125" sy="1.6877775416667191" tx="3.5438179240499488" ty="15.159046513427825">
+ <y:Point x="677.1953125" y="295.06079483032227"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="199.45977783203125" x="9.040044168467375" xml:space="preserve" y="-90.39680862426758">make <target>.parse<y:LabelModel><y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/></y:LabelModel><y:ModelParameter><y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="false" position="center" ratio="0.8554216369007797" segment="-1"/></y:ModelParameter><y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/></y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e2" source="n2" target="n1">
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="12.550799999999583" sy="1.1907775416665345" tx="10.257687999999916" ty="1.1907775416665345"/>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" hasText="false" height="4.0" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="4.0" x="4.971771083282761" y="-32.43774294236715">
+ <y:LabelModel>
+ <y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/>
+ </y:LabelModel>
+ <y:ModelParameter>
+ <y:SmartEdgeLabelModelParameter angle="0.0" distance="28.437731874658613" distanceToCenter="false" position="left" ratio="7.066285762837311E-5" segment="-1"/>
+ </y:ModelParameter>
+ <y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/>
+ </y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e3" source="n3" target="n1">
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="0.0" sy="0.0" tx="8.16053599999998" ty="1.600377541666603">
+ <y:Point x="364.0" y="522.3519359999999"/>
+ <y:Point x="364.0" y="407.9523135416665"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" hasText="false" height="4.0" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="4.0" x="5.0" y="-28.7947432453513">
+ <y:LabelModel>
+ <y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/>
+ </y:LabelModel>
+ <y:ModelParameter>
+ <y:SmartEdgeLabelModelParameter angle="0.0" distance="24.79475053441371" distanceToCenter="false" position="left" ratio="0.0" segment="0"/>
+ </y:ModelParameter>
+ <y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/>
+ </y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e4" source="n1" target="n5">
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="58.77031249999982" sy="-0.9788891249999097" tx="0.0" ty="0.0">
+ <y:Point x="675.3953124999998" y="554.1351179739988"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="179.47979736328125" x="18.452149164157504" xml:space="preserve" y="95.69732042761211">make <target>.eva<y:LabelModel><y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/></y:LabelModel><y:ModelParameter><y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="false" position="center" ratio="0.774668867229586" segment="-1"/></y:ModelParameter><y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/></y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e5" source="n5::n1" target="n6">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="74.5" sy="0.0" tx="-79.0" ty="0.0"/>
+ <y:LineStyle color="#FF0000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e6" source="n4::n2" target="n6">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="75.21875" sy="0.0" tx="-79.0" ty="0.0"/>
+ <y:LineStyle color="#FF0000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e7" source="n4::n0" target="n8">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="74.859375" sy="0.0" tx="-79.0" ty="0.0"/>
+ <y:LineStyle color="#0000FF" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e8" source="n5::n0" target="n8">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="74.5" sy="0.0" tx="-79.0" ty="0.0"/>
+ <y:LineStyle color="#0000FF" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e9" source="n4::n1" target="n7">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
+ <y:LineStyle color="#008000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e10" source="n4" target="n5">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e11" source="n5" target="n9">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="0.7024574279785156" sy="-15.095404432332202" tx="-71.29754257202148" ty="-7.339997013875063"/>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e12" source="n1" target="n9">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="58.97499999999991" sy="2.6637775416665477" tx="0.0" ty="0.0">
+ <y:Point x="675.3953124999998" y="554.1297501417196"/>
+ <y:Point x="675.3953124999998" y="757.3797105555417"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="214.65975952148438" x="18.08602631745009" xml:space="preserve" y="298.9100526575925">make <target>.eva.gui<y:LabelModel><y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/></y:LabelModel><y:ModelParameter><y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="false" position="center" ratio="0.8150251451233256" segment="-1"/></y:ModelParameter><y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/></y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e13" source="n4::n3" target="n10">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="75.21875" sy="0.0" tx="-88.5" ty="0.0"/>
+ <y:LineStyle color="#FF9900" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e14" source="n5::n2" target="n10">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="74.5" sy="0.0" tx="-88.5" ty="0.0"/>
+ <y:LineStyle color="#FF9900" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
+ <y:EdgeLabel alignment="center" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" hasText="false" height="4.0" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="4.0" x="54.93627077068413" y="19.397853167779658">
+ <y:LabelModel>
+ <y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/>
+ </y:LabelModel>
+ <y:ModelParameter>
+ <y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="true" position="right" ratio="0.5" segment="0"/>
+ </y:ModelParameter>
+ <y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/>
+ </y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e15" source="n11" target="n1">
+ <data key="d9"/>
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="43.375" sy="-37.35619205833348" tx="7.111959999999954" ty="1.600377541666603">
+ <y:Point x="364.0" y="407.9523135416665"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="standard"/>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="146.69981384277344" x="7.325258240567905" xml:space="preserve" y="-209.49274718831396">make-template<y:LabelModel><y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/></y:LabelModel><y:ModelParameter><y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="true" position="center" ratio="0.8467602870289302" segment="-1"/></y:ModelParameter><y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/></y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ </graph>
+ <data key="d7">
+ <y:Resources/>
+ </data>
+</graphml>
diff --git a/doc/userman/analysis-scripts.pdf b/doc/userman/analysis-scripts.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..853e0e687779bd694aa87a1786e28038948769d2
Binary files /dev/null and b/doc/userman/analysis-scripts.pdf differ
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
new file mode 100644
index 0000000000000000000000000000000000000000..901130870c3b664df60a2d85b7b089d4078f9d38
--- /dev/null
+++ b/doc/userman/user-analysis-scripts.tex
@@ -0,0 +1,389 @@
+%% --------------------------------------------------------------------------
+%% --- Analysis scripts
+%% --------------------------------------------------------------------------
+
+\chapter{Analysis Scripts}
+\label{user-analysis-scripts}
+
+This chapter describes some tools and scripts shipped with \FramaC to help
+users setup and run analyses on large code bases. These scripts can also help
+dealing with unfamiliar code and automating analyses.
+
+\section{Requirements}
+
+These analysis scripts are chiefly based on the following tools:
+
+\begin{description}
+\item[Python]: most scripts are written using Python 3. Some scripts require
+ features from specific Python versions, and perform version checks when
+ starting.
+\item[GNU Make]: the main workflow for analysis scripts consists in using
+ GNU Make (4.0 or newer) to compute dependencies and cache intermediate
+ results.
+\item[Bash]: some scripts are written in Bash.
+\end{description}
+
+Besides those, a few tools are occasionally required by the scripts, such as
+Perl and GNU Parallel.
+
+\section{Usage}
+
+Most scripts are accessible via the \texttt{frama-c-script} command, installed
+along with \FramaC. Running this command without any arguments prints the list
+of commands, with a brief description of each of them. Some extra scripts are
+available by directly running them; in both cases, the actual scripts
+themselves are installed in Frama-C's \texttt{share} directory, underneath
+\texttt{analysis-scripts}.
+
+\subsection{General Framework}
+
+{\em Note}: while the analysis scripts are intended for usage in a wide variety
+of scenarios with different plug-ins, they currently focus
+on analyses with the \Value plug-in only.
+
+The main usage mode of \texttt{analysis-scripts} consists in creating a
+Makefile dedicated to the analysis of a C code base.
+
+This Makefile has three main purposes:
+
+\begin{enumerate}
+\item To separate the main analysis steps, saving partial results and logging
+ output messages;
+\item To avoid recomputing unnecessary data when modifying
+ analysis-specific options;
+\item To document analysis options and improve replayability, e.g. when
+ iteratively fine-tuning the analysis in order to improve its results.
+\end{enumerate}
+
+The intended usage is as follows:
+
+\begin{enumerate}
+\item The user identifies a C code base on which they would like to run
+ Frama-C;
+\item The user runs a script to interactively fill a template for
+ the analysis, with the list of source files and required parameters
+ (architecture, preprocessing flags, main function);
+\item The user edits and runs the generated Makefile, adjusting the
+ analysis as needed and re-running \texttt{make}.
+\end{enumerate}
+
+Ideally, after modifying the source code or re-parametrizing the analysis,
+re-running \texttt{make} should be enough to obtain a new result.
+
+Section~\ref{sec:using-generated-makefile} details usage of the Makefile
+and presents an illustrative diagram.
+
+\subsection{Necessary Build Information}
+\label{sec:necessary-build-information}
+
+The command \texttt{frama-c-script make-template} can be used to generate the
+Makefile from a template. The user must fill in the following information,
+required for running an \Value analysis:
+
+\begin{description}
+\item[machdep]: architectural information about system where the code will run:
+ integer type sizes, compiler, OS, etc. See section~\ref{sec:normalize} for
+ more details.
+\item[preprocessing flags]: options given to the C preprocessor, mainly
+ macros (\texttt{-D}) and include directories (\texttt{-I}).
+\item[list of sources]: the actual list of source files that make a logical
+ unit (e.g. a test case or a whole program), without duplicate function
+ definitions.
+\item[main function]: the function where the analysis will start; it is often
+ \texttt{main}, but not always. ({\em Note: \FramaC itself thes not require
+ a \texttt{main} function, but plug-ins such as \texttt{Eva} do}.)
+\end{description}
+
+A project without this information is incomplete; an alternative
+workflow is then necessary. The next section presents some possibilities to
+retrieve such information.
+
+\subsection{Possible Workflows in the Absence of Build Information}
+\label{alternative-workflows}
+
+It is sometimes the case that the \FramaC user is not the developer of the
+code under analysis, and does not have full build information about it;
+or the code contains non-portable features or missing libraries which prevent
+\FramaC from parsing it.
+In such cases, these analysis scripts provide two alternative workflows,
+depending on how one prefers to choose their source files:
+{\em one at a time} or {\em all-in}, described below.
+
+\subsubsection{One at a time}
+
+In this workflow, the user starts from the entry point
+of the analysis: typically the \texttt{main} function of a program or a test
+case. Only the file defining that function is included at first. Then, using
+\texttt{make-wrapper} (described in section~\ref{sec:script-descriptions}),
+the user iteratively adds new sources as needed,
+so that all function definitions are included.
+
+\begin{itemize}
+\item Advantages: higher code coverage; faster preprocessing/parsing; and
+avoids including possibly unrelated files
+(e.g. for an alternative OS/architecture).
+\item Drawbacks: the iterative approach recomputes the analysis several times;
+ also, it may miss files containing global initializers, which are not flagged
+ as missing.
+\end{itemize}
+
+\subsubsection{All-in}
+
+In this workflow, the user adds {\em all} source files to the analysis, and
+if necessary removes some of them, e.g. when there are conflicting definitions,
+such as when multiple test files define a \texttt{main} function.
+
+\begin{itemize}
+\item Advantages: optimistic approach; may not require any extra iterations, if
+ everything is defined, and only once. Does not miss global initializers, and
+ may find issues in code which is not reachable (e.g. syntax-related warnings).
+\item Drawbacks: preprocesses and parses several files which may end up never
+ being used; smaller code coverage; if parsing fails, it may be harder to
+ find the cause (especially if due to unnecessary sources).
+\end{itemize}
+
+\subsection{Using a JSON Compilation Database (JCDB)}
+
+Independently of the chosen workflow, some partial information can be retrieved
+when CMake or Makefile scripts are available for compiling the sources.
+They allow the production of a JSON Compilation Database
+(\texttt{compile\_commands.json}, called JCDB for short; see related option
+in section~\ref{sec:preprocessing}). This leads to a different workflow:
+
+\begin{enumerate}
+\item Run CMake with the flag \texttt{-DCMAKE\_EXPORT\_COMPILE\_COMMANDS=1},
+ or install Build EAR (\url{https://github.com/rizsotto/Bear}) and run
+ \texttt{bear make <targets>} instead of \texttt{make <targets>}. This will
+ create a \texttt{compile\_commands.json} file.
+\item Run \texttt{frama-c-script list-files}. A list of the compiled files,
+ along with files defining a \texttt{main} function, will be presented.
+\item Run \texttt{frama-c-script make-template} to create a template for
+ \FramaC/\Value. Answer ``yes'' when asked about using the
+ \texttt{compile\_commands.json} file.
+\end{enumerate}
+
+Ideally, the above approach should result in a working template. In practice,
+however, the compilation database may include extraneous sources
+(used to compile other files than the target object) and duplicate flags
+(e.g. when compiling the same source for different binary targets or test
+cases). Manual intervention may be necessary.
+
+\section{Using the generated Makefile}
+\label{sec:using-generated-makefile}
+
+The generated Makefile can be used to run one or several analyses.
+The diagram in Fig.~\ref{fig:analysis-scripts} summarizes its usage.
+Makefile targets and outputs are detailed in this section.
+
+\begin{figure}[htbp]
+ \begin{center}
+ \includegraphics[width=\textwidth]{analysis-scripts.pdf}
+ \caption{Overview of the {\em analysis-scripts} workflow:
+ the inputs on the left produce a GNUmakefile which is then used
+ for parsing, analyzing and visualizing results.}
+ \label{fig:analysis-scripts}
+ \end{center}
+\end{figure}
+
+Each analysis is defined in a target, written by the user as follows:
+
+\texttt{<target>.parse: file1.c file2.c ...}
+
+That is, the target name (chosen by the user), suffixed with \texttt{.parse},
+is defined as depending on each of its source files. Changes to any of these
+sources will trigger a recomputation of the AST.
+
+{\em Note:} the target name itself {\em cannot} contain slashes or dots.
+See also the {\em Technical Notes} section about some current limitations.
+
+Then, for each \texttt{.parse} target, a corresponding \texttt{.eva} target
+needs to be added to the \texttt{TARGETS} variable in the Makefile.
+This will run \Value on the test case.
+
+Each \texttt{.eva} target depends on its corresponding \texttt{.parse} target;
+if the sources change, the analysis must take into account the new AST.
+
+\subsection{Important Variables}
+
+Several Makefile variables are available to customize \FramaC; the main
+ones are presented below.
+
+\begin{description}
+\item[TARGETS]: as mentioned before, must contain the list of targets,
+ suffixed with \texttt{.eva}.
+\item[CPPFLAGS]: preprocessing options, passed to \FramaC inside option
+ \texttt{-cpp-extra-args}, when parsing the sources.
+\item[FCFLAGS]: extra command-line options given to \FramaC when parsing the
+ sources and when running analyses. Typically, the options given to the
+ \FramaC kernel.
+\item[EVAFLAGS]: extra command-line options given to \Value when running
+ its analyses.
+\end{description}
+
+These variables are defined globally, but they can also be customized for
+each target; for instance, if a given target \texttt{t1} has a main
+function \texttt{test1} and requires a global macro \texttt{-DTEST1}, but
+target \texttt{t2}'s main function is \texttt{test2} and it requires
+\texttt{-DTEST2}, you can locally modify \texttt{FCFLAGS} and \texttt{CPPFLAGS}
+as follows:
+
+\begin{lstlisting}
+t1.parse: FCFLAGS += -main test1
+t1.parse: CPPFLAGS += -DTEST1
+t2.parse: FCFLAGS += -main test2
+t2.parse: CPPFLAGS += -DTEST2
+\end{lstlisting}
+
+\subsection{Predefined targets}
+
+The predefined targets below are the {\em raison d'être} of the generated
+Makefile; they speed up analyses, provide self-documentation, and enable
+quick iterations during parametrization of the analysis.
+
+\begin{description}
+\item[all (default target)]: the default target simply calls
+ \texttt{<target>.eva}, for each \texttt{<target>} added to variable
+ \texttt{TARGETS}. Does nothing once the analysis is finished and saved.
+\item[<target>.parse]: runs \FramaC on the specified target, preprocessing
+ and parsing its source files. Produces a directory \texttt{<target>.parse}
+ containing several logs, a pretty-printed version of the parsed code, and
+ a \FramaC session file (\texttt{framac.sav}) to be loaded in the GUI or by
+ other analyses. Does nothing if parsing already happened.
+\item[<target>.eva]: loads the parsed result (from the \texttt{.parse} target)
+ and runs the \Value plug-in, with the options given in \texttt{EVAFLAGS}.
+ If the analysis succeeds, produces a directory \texttt{<target>.eva} with the
+ analysis results and a saved session file.
+ Also creates a timestamped version of \texttt{<target>.eva}, to enable
+ future comparisons between different parametrizations. The non-timestamped
+ version corresponds to the latest (successful) analysis.
+ If the analysis fails, tries to save a partial result in
+ \texttt{<target>.eva.error} (when possible).
+\item[<target>.eva.gui]: loads the result of the corresponding
+ \texttt{<target>.eva} session and opens it in the GUI. This allows inspecting
+ the results of \Value. This target always opens the GUI, even when no
+ changes have happened.
+\item[clean]: removes all results produced by the \texttt{.parse} and
+ \texttt{.eva} targets.
+\end{description}
+
+\section{Script Descriptions}
+\label{sec:script-descriptions}
+
+The most useful commands are described below.
+Run \texttt{frama-c-script help} for more details and optional arguments.
+
+\begin{description}
+\item[make-template]: creates the initial Makefile, based on a template.
+ This command creates a file named \texttt{GNUmakefile} with some hardcoded
+ sections, some filled in interactively by the user, and comments indicating
+ which parts may need change. Once created, it enables the general workflow
+ mentioned earlier.
+\item[make-wrapper <target> <args>]: calls \texttt{make <target> <args>} with
+ a special wrapper: when running \Value, upon encountering one of a few known
+ error messages, suggests some actions on how to proceed.
+ For instance, if a missing function definition is encountered when analyzing
+ the code with \Value, the wrapper will look for its definition and, if found,
+ suggest that its source code be added to the analysis. This script is meant
+ to be used with the {\em one at a time} workflow describe in
+ section~\ref{alternative-workflows}.
+\item[find-fun <fun>]: looks for possible declarations and definitions
+ of function \texttt{<fun>}. Uses a heuristic that does not depend on \FramaC
+ being able to parse the sources. Useful to find entry points and missing
+ includes.
+\end{description}
+
+Other commands, only useful in a few cases, are described below.
+
+\begin{description}
+\item[configure <machdep>]: runs a \texttt{configure}
+ script (based on Autoconf) with some settings to emulate a more portable
+ system, removing optional code features that could prevent \FramaC from
+ parsing the sources. Currently still depends partially on the host system,
+ so many features are not disabled.
+\item[make-path] (for \FramaC developers): to be used when Frama-C is not
+ installed in the PATH; adds a \texttt{frama-c-path.mk} file that is used
+ by the Makefile generated by \texttt{make-template}.
+\item[flamegraph]: opens a {\em flamegraph}\footnote{%
+ See \url{https://github.com/brendangregg/FlameGraph} for details about
+ flamegraphs.} to visualize which functions take most of the time
+ during analysis with \Value.
+\item[summary]: for monitoring the progression of multiple analyses defined
+ in a single Makefile. Presents a summary of the analyses when done. Mostly
+ useful for benchmarking or when dealing with several test cases.
+\end{description}
+
+The following commands require a JSON Compilation Database.
+
+\begin{description}
+\item[list-files]: lists all files in the given JCDB. Useful for filling
+ out the Makefile template when running \texttt{make-template}.
+\item[normalize-jcdb]: converts absolute paths inside a
+ \texttt{compile\_commands.json} file into relative paths (w.r.t. PWD)
+ when possible. Used to allow moving/versioning the directory containing
+ the JCDB file.
+\end{description}
+
+Finally, there is the following script, which is {\em not} available as a
+command in \texttt{frama-c-script}, since its usage scenario is very
+different. It is available at\\
+\texttt{\$FRAMAC\_SHARE/analysis-scripts/creduce.sh}.
+
+\begin{description}
+\item[creduce.sh]: A script to help running the C-Reduce\footnote{%
+ See \url{https://embed.cs.utah.edu/creduce} for more details.} tool to minify
+ C programs causing crashes in \FramaC; useful e.g. when submitting a bug
+ report to \FramaC, without needing to submit potentially confidential data.
+ The script contains extensive comments about its usage. It is also
+ described in a post\footnote{%
+ {\em Debugging Frama-C analyses: better privacy with C-Reduce},
+ at \url{https://pub.frama-c.com/scripts/usability/2020/04/02/creduce.html}.}
+ from the \FramaC blog.
+\end{description}
+
+To use the \texttt{creduce.sh} script, you need to have the C-Reduce tool
+installed in your path or in environment variable \texttt{CREDUCE}.
+
+\section{Practical Examples: Open Source Case Studies}
+
+The {\em open-source-case-studies} Git repository (OSCS for short),
+available at \url{https://git.frama-c.com/pub/open-source-case-studies},
+contains several open-source C code bases parametrized with the help of
+analysis scripts. Each case study has its own directory, with a
+\texttt{GNUmakefile} defining one or more analysis targets.
+
+Due to the variety of test cases, OSCS provide practical usage
+examples of the \texttt{GNUmakefile} described in this chapter.
+They are periodically synchronized w.r.t. the public \FramaC repository
+(daily snapshots), so they may contain features not yet available in the
+major \FramaC releases. A few case studies may also contain legacy features
+which are no longer used; but overall, they provide useful examples and allow
+the user to tweak analysis parameters to test their effects.
+
+\section{Technical Notes}
+
+This section lists known issues and technical details which may help users
+understand some unintuitive behaviors.
+
+\paragraph{\em Changes to header files do not trigger a new parsing/analysis.}
+Currently, changes to included files (e.g. headers) are {\em not}
+tracked by the generated Makefile and may require running \texttt{make}
+with \texttt{-B} (to force recomputation of dependencies), or running
+\texttt{make clean} before re-running \texttt{make}.
+
+\paragraph{\em Why is the generated Makefile called \texttt{GNUmakefile}?}
+GNU Make, by default, searches for a file named \texttt{GNUmakefile} before
+searching for a \texttt{Makefile}. Thus, running \texttt{make} without
+arguments results in running the Makefile generated by \texttt{make-template}.
+You can rename it to \texttt{framac.mk} or something else, and then run it
+via \texttt{make -f framac.mk <targets>}.
+
+\paragraph{\em Most scripts are heuristics-based and offer no
+ correctness/completeness guarantees.} In order to handle files {\em before}
+the source preparation step is complete (that is, before \FramaC is able to
+parse the sources into a complete AST), most commands use scripts based on
+syntactic heuristics, which were found to work well in practice but are
+easily disturbed by syntactic changes (e.g. whitespaces).
+
+\paragraph{\em Most commands are experimental.} These analysis scripts are a
+recent addition and subject to changes. They are provided on a best-effort
+basis.
diff --git a/doc/userman/user-intro.tex b/doc/userman/user-intro.tex
index c0245ee59776c667f985a621b36bb22e388150fe..eaaf0c0a778922a5bc1aebfb860b67e9c2ac0d1d 100644
--- a/doc/userman/user-intro.tex
+++ b/doc/userman/user-intro.tex
@@ -53,6 +53,13 @@ The remainder of this manual is organized in several chapters.
the platform.
\item[Chapter~\ref{user-gui}] gives a detailed description of the graphical
user interface of \FramaC.
+\item[Chapter~\ref{user-report}] describes the \texttt{Report} plug-in, used
+ for textual consolidation and export of warnings, errors and properties.
+\item[Chapter~\ref{user-variadic}] presents the \texttt{Variadic} plug-in,
+ used to help other plug-ins handle code containing variadic functions, such
+ as \texttt{printf} and \texttt{scanf}.
+\item[Chapter~\ref{user-analysis-scripts}] details several scripts used to
+ help setup and run analyses on large code bases.
\item[Chapter~\ref{user-errors}] explains how to report errors \via \FramaC's
public Gitlab repository.
\end{description}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index ee189cbe97c2d80eb4e448417b23946573c27fa7..e4c5b2f429525043198c6cf2ac42c33cec34f60b 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -1,4 +1,4 @@
-ojson\chapter{Preparing the Sources}
+\chapter{Preparing the Sources}
\label{user-sources}
This chapter explains how to specify the source files that form the
diff --git a/doc/userman/user-variadic.tex b/doc/userman/user-variadic.tex
index f730beef81b75abcc3f87a86e40ce0e4fe38f3f2..45d55547225e43ab87604c5304f000bc24a9b663 100644
--- a/doc/userman/user-variadic.tex
+++ b/doc/userman/user-variadic.tex
@@ -17,7 +17,7 @@ their prototype by an ellipsis (\ldots) after a set of fixed arguments.
Some functions in the C standard library are variadic, in particular
formatted input/output functions, such as \texttt{printf}/\texttt{scanf}.
Due to the dynamic nature of their arguments, such functions present additional
-challenges to code analysis. The \textttdef{Variadic} helps dealing with some
+challenges to code analysis. The \textttuse{Variadic} helps dealing with some
of these challenges, reducing or eliminating the need for plug-ins to have
to deal with these special cases.
diff --git a/doc/userman/userman.tex b/doc/userman/userman.tex
index 46e8a404dbee0955045b6755d8f202bfdafd4728..14e4cb255bb86c581c303c71df2b53a06afb9918 100644
--- a/doc/userman/userman.tex
+++ b/doc/userman/userman.tex
@@ -64,6 +64,7 @@ Baudin, Mickaël Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente
\include{user-gui}
\include{user-report}
\include{user-variadic}
+\include{user-analysis-scripts}
\include{user-errors}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%