=> Bootstrap dependency digest>=20010302: found digest-20111104 ===> Skipping vulnerability checks. WARNING: No /var/db/pkg/pkg-vulnerabilities file found. WARNING: To fix run: `/usr/sbin/pkg_admin -K /var/db/pkg fetch-pkg-vulnerabilities'. ===> Building for frama-c-20111001nb10 Makefile:2267: .depend: No such file or directory Copying to src/lib/my_bigint.ml Building ocamlgraph gmake[1]: Entering directory `/scratch/devel/frama-c/work/frama-c-Nitrogen-20111001/ocamlgraph' sed -e s/VERSION/1.8/ -e s/CMA/graph.cma/ -e s/CMXA/graph.cmxa/ \ META.in > META Generating src/lib/printexc_common_interface.ml rm -f src/version.ml echo "let version = \""1.8"\"" > src/version.ml Generating src/lib/map_common_interface.mli echo "let date = \""`date`"\"" >> src/version.ml Generating src/lib/map_common_interface.ml Generating src/lib/dynlink_common_interface.ml Generating src/kernel/config.ml Generating share/frama-c.rc Generating ptests/ptests_config.ml Generating share/Makefile.dynamic_config Generating share/Makefile.kernel Generating lib/plugins/Occurrence.mli rm -f .depend Generating lib/plugins/Metrics.mli ocamldep -slash -I src -I lib -I editor -I view_graph -I dgraph\ lib/*.ml lib/*.mli \ src/*.ml src/*.mli \ editor/*.mli editor/*.ml \ view_graph/*.mli view_graph/*.ml \ dgraph/*.mli dgraph/*.ml > .depend Generating lib/plugins/Syntactic_callgraph.mli Generating lib/plugins/Value.mli Generating lib/plugins/RteGen.mli Generating lib/plugins/From.mli Generating lib/plugins/Users.mli Generating lib/plugins/Constant_Propagation.mli Generating lib/plugins/Postdominators.mli Generating lib/plugins/Inout.mli Generating lib/plugins/Semantic_callgraph.mli Generating lib/plugins/Impact.mli Generating lib/plugins/Pdg.mli Generating lib/plugins/Scope.mli Generating lib/plugins/Sparecode.mli Generating lib/plugins/Aorai.mli Generating lib/plugins/Report.mli Generating lib/plugins/Security_slicing.mli Generating lib/plugins/Wp.mli gmake[1]: Leaving directory `/scratch/devel/frama-c/work/frama-c-Nitrogen-20111001/ocamlgraph' gmake[1]: Entering directory `/scratch/devel/frama-c/work/frama-c-Nitrogen-20111001/ocamlgraph' ocamlc.opt -c -I src -I lib -g -dtypes src/sig.mli Ocamldep src/occurrence/.depend ocamlc.opt -c -I src -I lib -g -dtypes src/sig_pack.mli ocamlc.opt -c -I src -I lib -g -dtypes src/dot_ast.mli ocamlc.opt -c -I src -I lib -g -dtypes lib/unionfind.mli Ocamldep src/metrics/.depend ocamlc.opt -c -I src -I lib -g -dtypes lib/unionfind.ml ocamlc.opt -c -I src -I lib -g -dtypes lib/heap.mli ocamlc.opt -c -I src -I lib -g -dtypes lib/heap.ml Ocamldep src/syntactic_callgraph/.depend Ocamldep src/value/.depend ocamlc.opt -c -I src -I lib -g -dtypes lib/bitv.mli ocamlc.opt -c -I src -I lib -g -dtypes lib/bitv.ml Ocamldep src/rte/.depend Ocamldep src/from/.depend Ocamldep src/users/.depend Ocamldep src/constant_propagation/.depend Ocamldep src/postdominators/.depend Ocamldep src/inout/.depend ocamlc.opt -c -I src -I lib -g -dtypes src/version.ml ocamlc.opt -c -I src -I lib -g -dtypes src/util.mli ocamlc.opt -c -I src -I lib -g -dtypes src/util.ml Ocamldep src/semantic_callgraph/.depend Ocamldep src/impact/.depend Ocamldep src/pdg/.depend ocamlc.opt -c -I src -I lib -g -dtypes src/blocks.ml Ocamldep src/scope/.depend Ocamldep src/sparecode/.depend Ocamldep src/slicing/.depend Ocamldep src/aorai/.depend Ocamldep src/report/.depend Ocamldep src/security_slicing/.depend Ocamldep src/wp/.depend ocamlc.opt -c -I src -I lib -g -dtypes src/persistent.mli ocamlc.opt -c -I src -I lib -g -dtypes src/persistent.ml ocamlc.opt -c -I src -I lib -g -dtypes src/imperative.mli ocamlc.opt -c -I src -I lib -g -dtypes src/imperative.ml ocamlc.opt -c -I src -I lib -g -dtypes src/delaunay.mli ocamlc.opt -c -I src -I lib -g -dtypes src/delaunay.ml ocamlc.opt -c -I src -I lib -g -dtypes src/builder.mli ocamlc.opt -c -I src -I lib -g -dtypes src/builder.ml ocamlc.opt -c -I src -I lib -g -dtypes src/classic.mli ocamlc.opt -c -I src -I lib -g -dtypes src/classic.ml ocamlc.opt -c -I src -I lib -g -dtypes src/rand.mli ocamlc.opt -c -I src -I lib -g -dtypes src/rand.ml ocamlc.opt -c -I src -I lib -g -dtypes src/oper.mli ocamlc.opt -c -I src -I lib -g -dtypes src/oper.ml ocamlc.opt -c -I src -I lib -g -dtypes src/path.mli ocamlc.opt -c -I src -I lib -g -dtypes src/path.ml ocamlc.opt -c -I src -I lib -g -dtypes src/traverse.mli ocamlc.opt -c -I src -I lib -g -dtypes src/traverse.ml ocamlc.opt -c -I src -I lib -g -dtypes src/coloring.mli ocamlc.opt -c -I src -I lib -g -dtypes src/coloring.ml ocamlc.opt -c -I src -I lib -g -dtypes src/topological.mli ocamlc.opt -c -I src -I lib -g -dtypes src/topological.ml ocamlc.opt -c -I src -I lib -g -dtypes src/components.mli ocamlc.opt -c -I src -I lib -g -dtypes src/components.ml ocamlc.opt -c -I src -I lib -g -dtypes src/kruskal.mli ocamlc.opt -c -I src -I lib -g -dtypes src/kruskal.ml ocamlc.opt -c -I src -I lib -g -dtypes src/flow.mli ocamlc.opt -c -I src -I lib -g -dtypes src/flow.ml ocamlc.opt -c -I src -I lib -g -dtypes src/graphviz.mli ocamlc.opt -c -I src -I lib -g -dtypes src/graphviz.ml ocamlc.opt -c -I src -I lib -g -dtypes src/gml.mli ocamlc.opt -c -I src -I lib -g -dtypes src/gml.ml ocamlc.opt -c -I src -I lib -g -dtypes src/dot_parser.mli ocamlc.opt -c -I src -I lib -g -dtypes src/dot_parser.ml ocamlc.opt -c -I src -I lib -g -dtypes src/dot_lexer.ml ocamlc.opt -c -I src -I lib -g -dtypes src/dot.mli ocamlc.opt -c -I src -I lib -g -dtypes src/dot.ml ocamlc.opt -c -I src -I lib -g -dtypes src/pack.mli ocamlc.opt -c -I src -I lib -g -dtypes src/pack.ml ocamlc.opt -c -I src -I lib -g -dtypes src/gmap.mli ocamlc.opt -c -I src -I lib -g -dtypes src/gmap.ml ocamlc.opt -c -I src -I lib -g -dtypes src/minsep.mli ocamlc.opt -c -I src -I lib -g -dtypes src/minsep.ml ocamlc.opt -c -I src -I lib -g -dtypes src/cliquetree.mli ocamlc.opt -c -I src -I lib -g -dtypes src/cliquetree.ml ocamlc.opt -c -I src -I lib -g -dtypes src/mcs_m.mli ocamlc.opt -c -I src -I lib -g -dtypes src/mcs_m.ml ocamlc.opt -c -I src -I lib -g -dtypes src/md.mli ocamlc.opt -c -I src -I lib -g -dtypes src/md.ml ocamlc.opt -c -I src -I lib -g -dtypes src/strat.mli ocamlc.opt -c -I src -I lib -g -dtypes src/strat.ml ocamlc.opt -I src -I lib -pack -o graph.cmo src/sig.cmi src/sig_pack.cmi src/dot_ast.cmi lib/unionfind.cmo lib/heap.cmo lib/bitv.cmo src/version.cmo src/util.cmo src/blocks.cmo src/persistent.cmo src/imperative.cmo src/delaunay.cmo src/builder.cmo src/classic.cmo src/rand.cmo src/oper.cmo src/path.cmo src/traverse.cmo src/coloring.cmo src/topological.cmo src/components.cmo src/kruskal.cmo src/flow.cmo src/graphviz.cmo src/gml.cmo src/dot_parser.cmo src/dot_lexer.cmo src/dot.cmo src/pack.cmo src/gmap.cmo src/minsep.cmo src/cliquetree.cmo src/mcs_m.cmo src/md.cmo src/strat.cmo ocamlc.opt -I src -I lib -a -o graph.cma graph.cmo ocamlopt.opt -c -I src -I lib -for-pack Graph lib/unionfind.ml ocamlopt.opt -c -I src -I lib -for-pack Graph lib/heap.ml ocamlopt.opt -c -I src -I lib -for-pack Graph lib/bitv.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/version.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/util.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/blocks.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/persistent.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/imperative.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/delaunay.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/builder.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/classic.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/rand.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/oper.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/path.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/traverse.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/coloring.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/topological.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/components.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/kruskal.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/flow.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/graphviz.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/gml.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/dot_parser.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/dot_lexer.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/dot.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/pack.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/gmap.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/minsep.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/cliquetree.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/mcs_m.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/md.ml ocamlopt.opt -c -I src -I lib -for-pack Graph src/strat.ml ocamlopt.opt -I src -I lib -pack -o graph.cmx src/sig.cmi src/sig_pack.cmi src/dot_ast.cmi lib/unionfind.cmx lib/heap.cmx lib/bitv.cmx src/version.cmx src/util.cmx src/blocks.cmx src/persistent.cmx src/imperative.cmx src/delaunay.cmx src/builder.cmx src/classic.cmx src/rand.cmx src/oper.cmx src/path.cmx src/traverse.cmx src/coloring.cmx src/topological.cmx src/components.cmx src/kruskal.cmx src/flow.cmx src/graphviz.cmx src/gml.cmx src/dot_parser.cmx src/dot_lexer.cmx src/dot.cmx src/pack.cmx src/gmap.cmx src/minsep.cmx src/cliquetree.cmx src/mcs_m.cmx src/md.cmx src/strat.cmx ocamlopt.opt -I src -I lib -a -o graph.cmxa graph.cmx gmake[1]: Leaving directory `/scratch/devel/frama-c/work/frama-c-Nitrogen-20111001/ocamlgraph' Copying to lib/graph.cmi Copying to lib/graph.cmo Copying to lib/graph.cmx Copying to lib/graph.o Generating .depend Ocamlc src/lib/printexc_common_interface.cmi Ocamlc external/unmarshal.cmi Ocamlc src/lib/map_common_interface.cmi Ocamlc src/lib/dynlink_common_interface.cmi Ocamlc src/type/structural_descr.cmi Ocamlc src/lib/extlib.cmi Ocamlc src/lib/pretty_utils.cmi Ocamlc src/lib/hook.cmi Ocamlc src/lib/bag.cmi Ocamlc src/lib/bitvector.cmi Ocamlc src/lib/qstack.cmi Ocamlc src/lib/my_bigint.cmi Ocamlc src/kernel/config.cmi Ocamlc src/kernel/log.cmi Ocamlc src/kernel/cmdline.cmi Ocamlc cil/src/cilmsg.cmi Ocamlc cil/ocamlutil/alpha.cmi Ocamlc cil/ocamlutil/clist.cmi Ocamlc cil/ocamlutil/growArray.cmi Ocamlc cil/ocamlutil/inthash.cmi Ocamlc cil/src/cil_types.cmi Ocamlc cil/src/logic/utf8_logic.cmi Ocamlc cil/src/cilglobopt.cmo Ocamlc cil/src/escape.cmi Ocamlc cil/src/frontc/errorloc.cmi Ocamlc cil/src/logic/logic_builtin.cmi Ocamlc cil/src/mergecil.cmi Ocamlc cil/src/rmtmps.cmi Ocamlc cil/src/logic/logic_preprocess.cmi Ocamlc cil/src/ext/obfuscate.cmi Ocamlc cil/src/ext/dataflow.cmi Ocamlc cil/src/ext/dominators.cmi Ocamlc cil/src/ext/oneret.cmi Ocamlc src/kernel/ast_info.cmi Ocamlc src/kernel/ast_printer.cmi Ocamlc src/kernel/unicode.cmi Ocamlc src/misc/subst.cmi Ocamlc src/kernel/unroll_loops.cmi Ocamlc src/kernel/command.cmi Ocamlc src/kernel/task.cmi Ocamlc src/logic/translate_lightweight.cmi Ocamlc src/kernel/special_hooks.cmi Ocamlc lib/plugins/Value.cmi Ocamlc lib/plugins/From.cmi Ocamlc src/memory_state/bit_model_access.cmi Ocamlc src/logic/logic_interp.cmi Ocamlc src/logic/infer_annotations.cmi Ocamlc lib/plugins/Occurrence.cmi Ocamlc src/metrics/css_html.cmo Ocamlc lib/plugins/Metrics.cmi Ocamlc src/metrics/metrics_cabs.cmi Ocamlc lib/plugins/Syntactic_callgraph.cmi Ocamlc src/value/kf_state.cmi Ocamlc src/value/separate.cmi Ocamlc src/value/eval_funs.cmi Ocamlc lib/plugins/RteGen.cmi Ocamlc lib/plugins/Postdominators.cmi Ocamlc lib/plugins/Users.cmi Ocamlc src/constant_propagation/register.cmi Ocamlc lib/plugins/Constant_Propagation.cmi Ocamlc src/inout/inputs.cmi Ocamlc src/inout/outputs.cmi Ocamlc src/inout/derefs.cmi Ocamlc src/inout/access_path.cmi Ocamlc lib/plugins/Semantic_callgraph.cmi Ocamlc lib/plugins/Inout.cmi Ocamlc lib/plugins/Impact.cmi Ocamlc src/scope/zones.cmi Ocamlc src/scope/defs.cmi Ocamlc lib/plugins/Scope.cmi Ocamlc lib/plugins/Sparecode.cmi Ocamlc src/buckx/mybigarray.o Ocamlc src/buckx/buckx_c.o Ocamlc src/aorai/bool3.cmi Ocamlc src/aorai/spec_tools.cmo Ocamlc src/aorai/ltlast.cmi Ocamlc lib/plugins/Aorai.cmi Ocamlc lib/plugins/Report.cmi Ocamlc lib/plugins/Security_slicing.cmi Ocamlc src/wp/clabels.cmi Ocamlc src/wp/wp_error.cmi Ocamlc src/wp/ctypes.cmi Ocamlc src/wp/normAtLabels.cmi Ocamlc src/wp/script.cmi src/buckx/buckx_c.c:37:0: warning: "FE_DOWNWARD" redefined /usr/include/machine/fenv.h:62:0: note: this is the location of the previous definition src/buckx/buckx_c.c:38:0: warning: "FE_UPWARD" redefined /usr/include/machine/fenv.h:63:0: note: this is the location of the previous definition src/buckx/buckx_c.c:39:0: warning: "FE_TONEAREST" redefined /usr/include/machine/fenv.h:61:0: note: this is the location of the previous definition Ocamlc src/wp/proof.cmi src/buckx/buckx_c.c: In function 'terminate_process': src/buckx/buckx_c.c:124:4: warning: #warning Does your system have kill()? src/buckx/buckx_c.c:117:8: warning: unused variable 'pid' Ocamlc src/wp/variables_analysis.cmi Ocamlc src/wp/formula.cmi Ocamlc src/wp/kreal.cmi Ocamlc src/wp/LogicId.cmi Ocamlc lib/plugins/Wp.cmi Ocamlopt external/unmarshal.cmx Ocamlopt src/lib/printexc_common_interface.cmx Ocamlopt src/lib/map_common_interface.cmx Ocamlopt src/lib/dynlink_common_interface.cmx Ocamlopt src/lib/pretty_utils.cmx Ocamlopt src/lib/hook.cmx Ocamlopt src/lib/bag.cmx Ocamlopt src/lib/bitvector.cmx Ocamlopt src/lib/qstack.cmx Ocamlopt src/lib/my_bigint.cmx Ocamlopt src/kernel/config.cmx Ocamlopt src/kernel/log.cmx Ocamlopt cil/ocamlutil/clist.cmx Ocamlopt cil/ocamlutil/inthash.cmx Ocamlopt cil/src/logic/utf8_logic.cmx Ocamlopt cil/src/cilglobopt.cmx Ocamlopt cil/src/machdep_ppc_32.cmx Ocamlopt cil/src/escape.cmx Ocamlopt src/metrics/css_html.cmx Ocamlopt src/aorai/bool3.cmx Ocamlopt src/aorai/spec_tools.cmx Ocamlopt src/wp/script.cmx Ocamlopt src/wp/kreal.cmx Linking bin/ptests.byte Ocamlc external/unmarshal.cmo Ocamlc external/unmarshal_nums.cmi Ocamlc src/lib/printexc_common_interface.cmo Ocamlc src/lib/map_common_interface.cmo Ocamlc src/lib/dynlink_common_interface.cmo Ocamlc src/type/structural_descr.cmo Ocamlc src/type/type.cmi Ocamlc src/lib/extlib.cmo Ocamlc src/lib/pretty_utils.cmo Ocamlc src/lib/hook.cmo Ocamlc src/lib/bag.cmo Ocamlc src/lib/bitvector.cmo Ocamlc src/lib/qstack.cmo Ocamlc src/lib/my_bigint.cmo Ocamlc src/kernel/config.cmo Ocamlc src/kernel/log.cmo Ocamlc src/kernel/cmdline.cmo Ocamlc src/project/project_skeleton.cmi Ocamlc src/kernel/journal.cmi Ocamlc cil/ocamlutil/clist.cmo Ocamlc cil/ocamlutil/inthash.cmo Ocamlc cil/src/logic/logic_ptree.cmi Ocamlc cil/src/logic/utf8_logic.cmo Ocamlc cil/src/machdep_x86_16.cmi Ocamlc cil/src/machdep_x86_32.cmi Ocamlc cil/src/machdep_x86_64.cmi Ocamlc cil/src/machdep_ppc_32.cmo Ocamlc cil/src/machdep.cmi Ocamlc cil/src/escape.cmo Ocamlc cil/src/logic/logic_utils.cmi Ocamlc cil/src/logic/logic_print.cmi Ocamlc cil/src/logic/logic_typing.cmi Ocamlc src/aorai/bool3.cmo Ocamlc src/aorai/promelaast.cmi Ocamlc src/aorai/ltl_output.cmi Ocamlc src/wp/script.cmo Ocamlc src/wp/mint.cmi Ocamlc src/wp/mfloat.cmi Ocamlc src/wp/fol.cmi Ocamlc src/wp/mint_natural.cmo Ocamlc src/wp/mfloat_natural.cmo Ocamlc src/wp/fol_cc.cmo Ocamlc src/wp/fol_eval.cmo Ocamlc src/wp/fol_norm.cmi Ocamlc src/wp/kreal.cmo Ocamlc src/wp/fol_formula.cmi Ocamlc src/wp/LogicTau.cmi Ocamlopt src/type/structural_descr.cmx Ocamlopt external/unmarshal_nums.cmx Ocamlopt src/lib/extlib.cmx Ocamlopt cil/src/frontc/cabs.cmx Ocamlopt cil/src/machdep_x86_16.cmx Ocamlopt cil/src/machdep_x86_32.cmx Ocamlopt cil/src/machdep_x86_64.cmx Ocamlopt src/aorai/ltl_output.cmx Ocamlopt src/wp/mfloat_natural.cmx Ocamlc external/unmarshal_nums.cmo Ocamlc src/type/type.cmo Ocamlc src/type/descr.cmi Ocamlc src/project/project_skeleton.cmo Ocamlc src/type/datatype.cmi Ocamlc cil/src/frontc/cabs.cmo Ocamlc cil/ocamlutil/setWithNearest.cmi Ocamlc cil/src/machdep_x86_16.cmo Ocamlc cil/src/machdep_x86_32.cmo Ocamlc cil/src/machdep_x86_64.cmo Ocamlc cil/src/machdep.cmo Ocamlc cil/src/frontc/whitetrack.cmi Ocamlc cil/src/logic/logic_parser.cmi Ocamlc cil/src/frontc/cprint.cmi Ocamlc cil/src/frontc/cabscond.cmi Ocamlc cil/src/frontc/cparser.cmi Ocamlc cil/src/frontc/frontc.cmi Ocamlc src/logic/property.cmi Ocamlc src/misc/service_graph.cmi Ocamlc src/aorai/promelaoutput.cmi Ocamlc src/aorai/logic_simplification.cmi Ocamlc src/aorai/ltl_output.cmo Ocamlc src/aorai/ltlparser.cmi Ocamlc src/aorai/yaparser.cmi Ocamlc src/aorai/promelaparser.cmi Ocamlc src/aorai/promelaparser_withexps.cmi Ocamlc src/wp/mvalues.cmi Ocamlc src/wp/fol_let.cmi Ocamlc src/wp/LogicTau.cmo Ocamlc src/wp/LogicLang.cmi Ocamlc src/wp/translate_expr.cmi Ocamlopt src/type/type.cmx Ocamlopt cil/src/machdep.cmx Ocamlc src/type/descr.cmo Ocamlc src/type/datatype.cmo Ocamlc src/kernel/journal.cmo Ocamlc src/kernel/parameter.cmi Ocamlc src/lib/rangemap.cmi Ocamlc src/project/state.cmi Ocamlc cil/ocamlutil/setWithNearest.cmo Ocamlc cil/src/frontc/cabshelper.cmi Ocamlc cil/src/frontc/clexer.cmi Ocamlc src/kernel/ast.cmi Ocamlc src/kernel/annotations.cmi Ocamlc src/kernel/globals.cmi Ocamlc src/logic/description.cmi Ocamlc src/kernel/messages.cmi Ocamlc src/misc/service_graph.cmo Ocamlc src/aorai/ltllexer.cmo Ocamlc src/aorai/yalexer.cmo Ocamlc src/wp/data_mem.cmi Ocamlc src/wp/mlogic.cmi Ocamlc src/wp/LogicLib.cmi Ocamlc src/wp/LogicHavoc.cmi Ocamlc src/wp/LogicDef.cmi Ocamlc src/wp/ACSL.cmi Ocamlopt src/type/descr.cmx Ocamlopt src/kernel/cmdline.cmx Ocamlc src/kernel/parameter.cmo Ocamlc src/kernel/dynamic.cmi Ocamlc src/lib/rangemap.cmo Ocamlc src/project/state.cmo Ocamlc src/project/state_dependency_graph.cmi Ocamlc src/project/state_topological.cmi Ocamlc src/project/state_selection.cmi Ocamlc src/kernel/emitter.cmi Ocamlc external/hptmap.cmi Ocamlc src/lib/hptset.cmi Ocamlc src/logic/property_status.cmi Ocamlc src/kernel/cilE.cmi Ocamlc src/ai/abstract_interp.cmi Ocamlc src/wp/LogicLib.cmo Ocamlc src/wp/LogicHavoc.cmo Ocamlopt src/project/project_skeleton.cmx Ocamlc src/kernel/dynamic.cmo Ocamlc src/project/state_dependency_graph.cmo Ocamlc src/project/state_topological.cmo Ocamlc src/project/state_selection.cmo Ocamlc src/project/project.cmi Ocamlc src/lib/hptset.cmo Ocamlc cil/src/cil_datatype.cmi Ocamlc src/kernel/alarms.cmi Ocamlc src/ai/lattice_Interval_Set.cmi Ocamlc src/ai/int_Base.cmi Ocamlc src/ai/origin.cmi Ocamlc src/memory_state/int_Interv.cmi Ocamlc src/kernel/stmts_graph.cmi Ocamlc src/kernel/loop.cmi Ocamlc src/misc/filter.cmi Ocamlc src/aorai/data_for_aorai.cmi Ocamlopt src/type/datatype.cmx Ocamlc src/project/project.cmo Ocamlc src/project/dashtbl.cmi Ocamlc cil/ocamlutil/cilutil.cmi Ocamlc cil/src/logic/logic_const.cmi Ocamlc cil/src/frontc/cabs2cil.cmi Ocamlc src/ai/lattice_Interval_Set.cmo Ocamlc src/ai/int_Base.cmo Ocamlc src/misc/bit_utils.cmi Ocamlc src/ai/ival.cmi Ocamlc src/ai/origin.cmo Ocamlc src/aorai/aorai_utils.cmi Ocamlc src/project/dashtbl.cmo Ocamlc src/project/state_builder.cmi Ocamlc src/ai/base.cmi Ocamlc src/wp/wprop.cmi Ocamlc src/project/state_builder.cmo Ocamlc src/kernel/plugin.cmi Ocamlc src/lib/binary_cache.cmi Ocamlc cil/src/cil_state_builder.cmi Ocamlc cil/src/cil_const.cmi Ocamlc cil/src/logic/logic_env.cmi Ocamlc cil/src/cil.cmi Ocamlc src/buckx/buckx.cmi Ocamlc src/kernel/kernel_function.cmi Ocamlc src/ai/base_Set_Lattice.cmi Ocamlc src/memory_state/tr_offset.cmi Ocamlc src/kernel/visitor.cmi Ocamlc src/kernel/printer.cmi Ocamlc src/occurrence/options.cmi Ocamlc src/metrics/metrics_parameters.cmi Ocamlc src/metrics/metrics_coverage.cmi Ocamlc src/syntactic_callgraph/options.cmi Ocamlc src/value/value_parameters.cmi Ocamlc src/rte/rte_parameters.cmi Ocamlc src/from/from_parameters.cmi Ocamlc src/constant_propagation/propagationParameters.cmi Ocamlc src/postdominators/postdominators_parameters.cmi Ocamlc src/inout/inout_parameters.cmi Ocamlc src/semantic_callgraph/options.cmi Ocamlc src/impact/options.cmi Ocamlc src/pdg/pdg_parameters.cmi Ocamlc src/pdg/ctrlDpds.cmi Ocamlc src/sparecode/sparecode_params.cmi Ocamlc src/slicing/slicingParameters.cmi Ocamlc src/aorai/ltlparser.cmo Ocamlc src/aorai/aorai_option.cmi Ocamlc src/report/scan.cmi Ocamlc src/report/register.cmi Ocamlc src/security_slicing/security_slicing_parameters.cmi Ocamlc src/security_slicing/components.cmi Ocamlc src/wp/wprop.cmo Ocamlc src/wp/wpPropId.cmi Ocamlc src/wp/wp_error.cmo Ocamlc src/wp/cil2cfg.cmi Ocamlc src/wp/wpo.cmi Ocamlc src/wp/translate_prop.cmi Ocamlopt src/kernel/journal.cmx Ocamlopt src/kernel/parameter.cmx Ocamlopt src/lib/rangemap.cmx Ocamlopt src/project/state.cmx Ocamlopt cil/ocamlutil/setWithNearest.cmx Ocamlc src/kernel/plugin.cmo Ocamlc src/kernel/kernel.cmi Ocamlc src/lib/binary_cache.cmo Ocamlc external/hptmap.cmo Ocamlc cil/src/cilmsg.cmo Ocamlc cil/ocamlutil/alpha.cmo Ocamlc cil/ocamlutil/growArray.cmo Ocamlc cil/src/cil_datatype.cmo Ocamlc cil/ocamlutil/cilutil.cmo Ocamlc cil/src/cil_state_builder.cmo Ocamlc cil/src/cil_const.cmo Ocamlc cil/src/logic/logic_env.cmo Ocamlc cil/src/logic/logic_const.cmo Ocamlc cil/src/cil.cmo Ocamlc cil/src/frontc/errorloc.cmo Ocamlc cil/src/ext/expcompare.cmo Ocamlc cil/src/frontc/cabshelper.cmo Ocamlc cil/src/frontc/whitetrack.cmo Ocamlc cil/src/logic/logic_utils.cmo Ocamlc cil/src/logic/logic_builtin.cmo Ocamlc cil/src/logic/logic_print.cmo Ocamlc cil/src/logic/logic_parser.cmo Ocamlc cil/src/logic/logic_lexer.cmo Ocamlc cil/src/frontc/lexerhack.cmo Ocamlc cil/src/mergecil.cmo Ocamlc cil/src/rmtmps.cmo Ocamlc cil/src/logic/logic_typing.cmo Ocamlc cil/src/frontc/cprint.cmo Ocamlc cil/src/frontc/cabscond.cmo Ocamlc cil/src/frontc/cabsvisit.cmi Ocamlc cil/src/frontc/clexer.cmo Ocamlc cil/src/frontc/cparser.cmo Ocamlc cil/src/logic/logic_preprocess.cmo Ocamlc cil/src/frontc/frontc.cmo Ocamlc cil/src/ext/obfuscate.cmo Ocamlc cil/src/ext/ciltools.cmo Ocamlc cil/src/ext/callgraph.cmi Ocamlc cil/src/ext/dataflow.cmo Ocamlc cil/src/ext/dominators.cmo Ocamlc cil/src/ext/oneret.cmo Ocamlc cil/src/ext/cfg.cmi Ocamlc cil/src/ext/usedef.cmo Ocamlc src/buckx/buckx.cmo Ocamlc src/kernel/ast_info.cmo Ocamlc src/kernel/ast_printer.cmo Ocamlc src/kernel/ast.cmo Ocamlc src/logic/property.cmo Ocamlc src/logic/property_status.cmo Ocamlc src/kernel/annotations.cmo Ocamlc src/kernel/globals.cmo Ocamlc src/kernel/kernel_function.cmo Ocamlc src/logic/description.cmo Ocamlc src/kernel/alarms.cmo Ocamlc src/kernel/cilE.cmo Ocamlc src/kernel/messages.cmo Ocamlc src/ai/abstract_interp.cmo Ocamlc src/kernel/unicode.cmo Ocamlc src/misc/bit_utils.cmo Ocamlc src/misc/subst.cmo Ocamlc src/ai/ival.cmo Ocamlc src/memory_state/abstract_value.cmo Ocamlc src/ai/base_Set_Lattice.cmo Ocamlc src/ai/map_Lattice.cmo Ocamlc src/memory_state/locations.cmi Ocamlc src/memory_state/int_Interv.cmo Ocamlc src/memory_state/int_Interv_Map.cmo Ocamlc src/memory_state/tr_offset.cmo Ocamlc src/ai/lattice_With_Isotropy.cmi Ocamlc src/memory_state/offsetmap_bitwise.cmi Ocamlc src/memory_state/lmap_bitwise.cmi Ocamlc src/memory_state/widen_type.cmi Ocamlc src/kernel/stmts_graph.cmo Ocamlc src/kernel/visitor.cmo Ocamlc src/kernel/printer.cmo Ocamlc src/kernel/unroll_loops.cmo Ocamlc src/kernel/loop.cmo Ocamlc src/memory_state/inout_type.cmi Ocamlc src/pdg_types/pdgIndex.cmi Ocamlc src/logic/translate_lightweight.cmo Ocamlc src/kernel/file.cmi Ocamlc src/kernel/special_hooks.cmo Ocamlc src/memory_state/widen.cmo Ocamlc src/occurrence/options.cmo Ocamlc src/metrics/metrics_parameters.cmo Ocamlc src/syntactic_callgraph/options.cmo Ocamlc src/value/separate.cmo Ocamlc src/value/non_linear.cmi Ocamlc src/rte/rte_parameters.cmo Ocamlc src/from/from_parameters.cmo Ocamlc src/constant_propagation/propagationParameters.cmo Ocamlc src/postdominators/postdominators_parameters.cmo Ocamlc src/inout/kf_state.cmi Ocamlc src/inout/inout_parameters.cmo Ocamlc src/semantic_callgraph/options.cmo Ocamlc src/impact/options.cmo Ocamlc src/pdg/pdg_parameters.cmo Ocamlc src/sparecode/sparecode_params.cmo Ocamlc src/sparecode/marks.cmi Ocamlc src/slicing/slicingParameters.cmo Ocamlc src/aorai/aorai_option.cmo Ocamlc src/aorai/cil_manipulation.cmo Ocamlc src/aorai/path_analysis.cmo Ocamlc src/aorai/promelaoutput.cmo Ocamlc src/aorai/logic_simplification.cmo Ocamlc src/aorai/data_for_aorai.cmo Ocamlc src/aorai/aorai_utils.cmo Ocamlc src/aorai/utils_parser.cmo Ocamlc src/aorai/yaparser.cmo Ocamlc src/aorai/promelaparser.cmo Ocamlc src/aorai/promelalexer.cmo Ocamlc src/aorai/promelaparser_withexps.cmo Ocamlc src/aorai/promelalexer_withexps.cmo Ocamlc src/aorai/abstract_ai.cmo Ocamlc src/aorai/bycase_ai.cmo Ocamlc src/aorai/aorai_visitors.cmo Ocamlc src/report/scan.cmo Ocamlc src/report/dump.cmi Ocamlc src/security_slicing/security_slicing_parameters.cmo Ocamlc src/wp/mcfg.cmi Ocamlc src/wp/wpStrategy.cmi Ocamlc src/wp/prover.cmi Ocamlc src/wp/datalib.cmi Ocamlc src/wp/mwp.cmi Ocamlc src/wp/fol_split.cmi Ocamlc src/wp/calculus.cmi Ocamlc src/wp/cfgpropid.cmi Ocamlc src/wp/cfgWeakestPrecondition.cmi Ocamlopt src/kernel/dynamic.cmx Ocamlopt src/project/state_dependency_graph.cmx Ocamlopt src/project/state_topological.cmx Ocamlc src/kernel/kernel.cmo Ocamlc src/kernel/emitter.cmo Ocamlc cil/src/frontc/cabsvisit.cmo Ocamlc cil/src/frontc/cabs2cil.cmo Ocamlc cil/src/ext/callgraph.cmo Ocamlc cil/src/ext/cfg.cmo Ocamlc cil/src/ext/liveness.cmo Ocamlc cil/src/ext/availexpslv.cmo Ocamlc src/ai/base.cmo Ocamlc src/memory_state/locations.cmo Ocamlc src/memory_state/shifted_Location.cmi Ocamlc src/memory_state/new_offsetmap.cmi Ocamlc src/memory_state/offsetmap.cmi Ocamlc src/memory_state/offsetmap_bitwise.cmo Ocamlc src/memory_state/lmap.cmi Ocamlc src/memory_state/lmap_bitwise.cmo Ocamlc src/memory_state/function_Froms.cmo Ocamlc src/memory_state/cvalue.cmi Ocamlc src/memory_state/inout_type.cmo Ocamlc src/pdg_types/pdgIndex.cmo Ocamlc src/pdg_types/pdgTypes.cmi Ocamlc src/kernel/file.cmo Ocamlc src/value/library_functions.cmi Ocamlc src/value/eval_exprs.cmi Ocamlc src/value/non_linear.cmo Ocamlc src/value/initial_state.cmi Ocamlc src/inout/kf_state.cmo Ocamlc src/pdg/pdg_state.cmi Ocamlc src/pdg/build.cmi Ocamlc src/pdg/annot.cmi Ocamlc src/report/dump.cmo Ocamlc src/wp/wp_parameters.cmi Ocamlc src/wp/wpFroms.cmi Ocamlc src/wp/wpAnnot.cmi Ocamlc src/wp/proof.cmo Ocamlc src/wp/prover.cmo Ocamlc src/wp/variables_analysis.cmo Ocamlc src/wp/datalib.cmo Ocamlc src/wp/fol.cmo Ocamlc src/wp/fol_let.cmo Ocamlc src/wp/fol_decl.cmo Ocamlc src/wp/funvar_mem.cmi Ocamlc src/wp/runtime_mem.cmi Ocamlc src/wp/store_mem.cmi Ocamlc src/wp/hoare_mem.cmi Ocamlc src/wp/fol_eqs.cmo Ocamlc src/wp/fol_split.cmo Ocamlc src/wp/fol_ergo.cmo Ocamlc src/wp/fol_coq.cmo Ocamlc src/wp/LogicId.cmo Ocamlc src/wp/LogicRaw.cmo Ocamlc src/wp/LogicDef.cmo Ocamlc src/wp/ACSL.cmo Ocamlc src/wp/translate_expr.cmo Ocamlc src/wp/translate_prop.cmo Ocamlc src/wp/cfgpropid.cmo Ocamlc src/wp/cfgWeakestPrecondition.cmo Ocamlopt src/project/state_selection.cmx Ocamlc cil/src/ext/reachingdefs.cmo Ocamlc src/memory_state/shifted_Location.cmo Ocamlc src/memory_state/path_lattice.cmi Ocamlc src/memory_state/new_offsetmap.cmo Ocamlc src/memory_state/offsetmap.cmo Ocamlc src/memory_state/lmap.cmo Ocamlc src/memory_state/cvalue.cmo Ocamlc src/memory_state/widen_type.cmo Ocamlc src/memory_state/state_set.cmi Ocamlc src/pdg_types/pdgTypes.cmo Ocamlc src/pdg_types/pdgMarks.cmi Ocamlc src/pdg/pdg_state.cmo Ocamlc src/pdg/marks.cmi Ocamlc src/wp/wp_parameters.cmo Ocamlc src/wp/ctypes.cmo Ocamlc src/wp/clabels.cmo Ocamlc src/wp/normAtLabels.cmo Ocamlc src/wp/wpPropId.cmo Ocamlc src/wp/wpStrategy.cmo Ocamlc src/wp/wpFroms.cmo Ocamlc src/wp/wpo.cmo Ocamlc src/wp/fol_pretty.cmo Ocamlc src/wp/data_mem.cmo Ocamlc src/wp/funvar_mem.cmo Ocamlc src/wp/runtime_mem.cmo Ocamlc src/wp/store_mem.cmo Ocamlc src/wp/hoare_mem.cmo Ocamlc src/wp/fol_norm.cmo Ocamlc src/wp/fol_why.cmo Ocamlc src/wp/fol_formula.cmo Ocamlc src/wp/LogicPretty.cmi Ocamlopt src/project/project.cmx Ocamlc cil/src/ext/rmciltmps.cmo Ocamlc cil/src/ext/deadcodeelim.cmo Ocamlc src/memory_state/path_lattice.cmo Ocamlc src/memory_state/state_set.cmo Ocamlc src/memory_state/state_imp.cmi Ocamlc src/slicing_types/slicingInternals.cmo Ocamlc src/wp/LogicPretty.cmo Ocamlc src/wp/LogicLang.cmo Ocamlopt src/project/dashtbl.cmx Ocamlc src/memory_state/state_imp.cmo Ocamlc src/slicing_types/slicingTypes.cmo Ocamlc src/slicing/fct_slice.cmi Ocamlc src/slicing/register.cmi Ocamlc src/kernel/db.cmi Ocamlc src/slicing/slicingMarks.cmi Ocamlopt src/project/state_builder.cmx Ocamlc lib/plugins/Pdg.cmi Ocamlc src/kernel/db.cmo Ocamlc src/kernel/command.cmo Ocamlc src/kernel/task.cmo Ocamlc src/misc/filter.cmo Ocamlc src/memory_state/bit_model_access.cmo Ocamlc src/logic/logic_interp.cmo Ocamlc src/logic/infer_annotations.cmo Ocamlc src/occurrence/register.cmo Ocamlc src/metrics/metrics_base.cmi Ocamlc src/syntactic_callgraph/register.cmo Ocamlc src/value/kf_state.cmo Ocamlc src/value/value_parameters.cmo Ocamlc src/value/library_functions.cmo Ocamlc src/value/mark_noresults.cmo Ocamlc src/value/value_util.cmo Ocamlc src/rte/rte.cmo Ocamlc src/rte/register.cmo Ocamlc src/from/from_register.cmo Ocamlc src/users/users_register.cmo Ocamlc src/constant_propagation/register.cmo Ocamlc src/postdominators/print.cmo Ocamlc src/inout/cumulative_analysis.cmi Ocamlc src/inout/operational_inputs.cmo Ocamlc src/semantic_callgraph/register.cmo Ocamlc src/inout/access_path.cmo Ocamlc src/impact/register.cmo Ocamlc src/pdg/ctrlDpds.cmo Ocamlc src/pdg/build.cmo Ocamlc src/pdg/sets.cmi Ocamlc src/scope/datascope.cmo Ocamlc src/sparecode/globs.cmo Ocamlc src/sparecode/marks.cmo Ocamlc src/sparecode/transform.cmo Ocamlc src/slicing/slicingMacros.cmo Ocamlc src/slicing/slicingMarks.cmo Ocamlc src/slicing/slicingActions.cmi Ocamlc src/slicing/slicingTransform.cmi Ocamlc src/slicing/slicingCmds.cmo Ocamlc src/kernel/boot.cmo Ocamlc src/aorai/aorai_register.cmo Ocamlc src/report/register.cmo Ocamlc src/security_slicing/components.cmo Ocamlc src/wp/cil2cfg.cmo Ocamlc src/wp/wpAnnot.cmo Ocamlc src/wp/calculus.cmo Ocamlc src/wp/cfgProof.cmo Ocamlopt src/kernel/plugin.cmx Ocamlopt src/lib/binary_cache.cmx Ocamlopt src/buckx/buckx.cmx Ocamlc src/pdg_types/pdgMarks.cmo Packing lib/plugins/Occurrence.cmo Ocamlc src/metrics/metrics_base.cmo Ocamlc src/metrics/metrics_cabs.cmo Ocamlc src/metrics/metrics_cilast.cmi Ocamlc src/metrics/metrics_coverage.cmo Ocamlc src/metrics/register.cmo Packing lib/plugins/Syntactic_callgraph.cmo Ocamlc src/value/builtins.cmo Ocamlc src/value/current_table.cmo Ocamlc src/value/eval_exprs.cmo Ocamlc src/value/initial_state.cmo Ocamlc src/value/eval_logic.cmo Ocamlc src/value/register.cmo Packing lib/plugins/RteGen.cmo Packing lib/plugins/From.cmo Packing lib/plugins/Users.cmo Packing lib/plugins/Constant_Propagation.cmo Ocamlc src/postdominators/compute.cmo Ocamlc src/inout/cumulative_analysis.cmo Ocamlc src/inout/inputs.cmo Ocamlc src/inout/outputs.cmo Ocamlc src/inout/derefs.cmo Ocamlc src/inout/register.cmo Packing lib/plugins/Semantic_callgraph.cmo Packing lib/plugins/Impact.cmo Ocamlc src/pdg/sets.cmo Ocamlc src/pdg/annot.cmo Ocamlc src/pdg/marks.cmo Ocamlc src/pdg/register.cmo Ocamlc src/scope/zones.cmo Ocamlc src/scope/defs.cmo Ocamlc src/sparecode/register.cmo Ocamlc src/slicing/slicingActions.cmo Ocamlc src/slicing/fct_slice.cmo Ocamlc src/slicing/printSlice.cmo Ocamlc src/slicing/slicingTransform.cmo Packing lib/plugins/Aorai.cmo Packing lib/plugins/Report.cmo Packing lib/plugins/Security_slicing.cmo Ocamlc src/wp/register.cmo Ocamlopt src/kernel/kernel.cmx Ocamlopt external/hptmap.cmx Ocamlopt cil/src/cilmsg.cmx Ocamlopt cil/ocamlutil/alpha.cmx Ocamlopt cil/ocamlutil/growArray.cmx Ocamlopt cil/src/frontc/errorloc.cmx Ocamlopt cil/src/frontc/lexerhack.cmx Ocamlopt src/kernel/unicode.cmx Ocamlopt src/occurrence/options.cmx Ocamlopt src/metrics/metrics_parameters.cmx Ocamlopt src/syntactic_callgraph/options.cmx Ocamlopt src/rte/rte_parameters.cmx Ocamlopt src/from/from_parameters.cmx Ocamlopt src/constant_propagation/propagationParameters.cmx Ocamlopt src/postdominators/postdominators_parameters.cmx Ocamlopt src/inout/inout_parameters.cmx Ocamlopt src/semantic_callgraph/options.cmx Ocamlopt src/impact/options.cmx Ocamlopt src/pdg/pdg_parameters.cmx Ocamlopt src/aorai/aorai_option.cmx Ocamlopt src/security_slicing/security_slicing_parameters.cmx Ocamlopt src/wp/wp_parameters.cmx Ocamlc src/metrics/metrics_cilast.cmo Ocamlc src/value/locals_scoping.cmo Packing lib/plugins/Postdominators.cmo Packing lib/plugins/Inout.cmo Packing lib/plugins/Pdg.cmo Packing lib/plugins/Scope.cmo Packing lib/plugins/Sparecode.cmo Ocamlc src/slicing/slicingProject.cmo Packing lib/plugins/Wp.cmo Ocamlopt src/kernel/emitter.cmx Ocamlopt src/lib/hptset.cmx Ocamlopt src/aorai/cil_manipulation.cmx Ocamlopt src/aorai/path_analysis.cmx Ocamlopt src/wp/LogicId.cmx Packing lib/plugins/Metrics.cmo Ocamlc src/value/eval_stmts.cmo Ocamlc src/slicing/register.cmo Ocamlopt cil/src/cil_datatype.cmx Ocamlopt src/wp/LogicTau.cmx Ocamlc src/value/eval_funs.cmo Packing lib/plugins/Slicing.cmo Ocamlopt src/wp/LogicRaw.cmx Packing lib/plugins/Value.cmo Ocamlopt src/wp/LogicPretty.cmx Linking bin/toplevel.byte Ocamlopt src/wp/LogicLang.cmx Ocamlopt cil/ocamlutil/cilutil.cmx Ocamlopt cil/src/cil_state_builder.cmx Ocamlopt cil/src/cil_const.cmx Ocamlopt src/wp/fol.cmx Ocamlopt src/wp/LogicLib.cmx Ocamlopt cil/src/logic/logic_env.cmx Copying to bytecode kernel API Ocamlopt src/wp/fol_let.cmx Ocamlopt src/wp/fol_cc.cmx Ocamlopt src/wp/fol_eqs.cmx Ocamlopt src/wp/fol_eval.cmx Ocamlopt src/wp/fol_split.cmx Ocamlopt src/wp/LogicHavoc.cmx Ocamlopt cil/src/logic/logic_const.cmx Ocamlopt src/wp/fol_norm.cmx Ocamlopt cil/src/cil.cmx Ocamlopt cil/src/ext/expcompare.cmx Ocamlopt cil/src/frontc/cabshelper.cmx Ocamlopt cil/src/logic/logic_utils.cmx Ocamlopt cil/src/logic/logic_print.cmx Ocamlopt cil/src/rmtmps.cmx Ocamlopt cil/src/frontc/cprint.cmx Ocamlopt cil/src/frontc/cabscond.cmx Ocamlopt cil/src/frontc/cabsvisit.cmx Ocamlopt cil/src/ext/obfuscate.cmx Ocamlopt cil/src/ext/ciltools.cmx Ocamlopt cil/src/ext/callgraph.cmx Ocamlopt cil/src/ext/dataflow.cmx Ocamlopt cil/src/ext/oneret.cmx Ocamlopt cil/src/ext/cfg.cmx Ocamlopt cil/src/ext/usedef.cmx Ocamlopt src/kernel/ast_info.cmx Ocamlopt src/kernel/ast_printer.cmx Ocamlopt src/kernel/ast.cmx Ocamlopt src/logic/property.cmx Ocamlopt src/ai/abstract_interp.cmx Ocamlopt src/misc/subst.cmx Ocamlopt src/misc/service_graph.cmx Ocamlopt src/kernel/special_hooks.cmx Ocamlopt src/aorai/utils_parser.cmx Ocamlopt src/aorai/ltlparser.cmx Ocamlopt src/wp/wp_error.cmx Ocamlopt src/wp/ctypes.cmx Ocamlopt src/wp/LogicDef.cmx Ocamlopt cil/src/frontc/whitetrack.cmx Ocamlopt cil/src/logic/logic_builtin.cmx Ocamlopt cil/src/logic/logic_parser.cmx Ocamlopt cil/src/mergecil.cmx Ocamlopt cil/src/ext/dominators.cmx Ocamlopt cil/src/ext/liveness.cmx Ocamlopt cil/src/ext/availexpslv.cmx Ocamlopt src/logic/property_status.cmx Ocamlopt src/kernel/messages.cmx Ocamlopt src/ai/lattice_Interval_Set.cmx Ocamlopt src/ai/int_Base.cmx Ocamlopt src/ai/origin.cmx Ocamlopt src/aorai/ltllexer.cmx Ocamlopt src/wp/wprop.cmx Ocamlopt src/wp/clabels.cmx Ocamlopt src/wp/fol_decl.cmx Ocamlopt src/wp/mint_natural.cmx Ocamlopt src/wp/ACSL.cmx Ocamlopt src/wp/translate_expr.cmx Ocamlopt cil/src/logic/logic_lexer.cmx Ocamlopt cil/src/ext/reachingdefs.cmx Ocamlopt src/kernel/annotations.cmx Ocamlopt src/kernel/globals.cmx Ocamlopt src/misc/bit_utils.cmx Ocamlopt src/ai/ival.cmx Ocamlopt src/ai/map_Lattice.cmx Ocamlopt src/kernel/visitor.cmx Ocamlopt src/kernel/printer.cmx Ocamlopt src/wp/normAtLabels.cmx Ocamlopt src/wp/fol_pretty.cmx Ocamlopt src/wp/data_mem.cmx Ocamlopt src/wp/fol_ergo.cmx Ocamlopt src/wp/fol_coq.cmx Ocamlopt src/wp/fol_formula.cmx Ocamlopt cil/src/logic/logic_typing.cmx Ocamlopt cil/src/frontc/cparser.cmx Ocamlopt cil/src/ext/rmciltmps.cmx Ocamlopt cil/src/ext/deadcodeelim.cmx Ocamlopt src/kernel/kernel_function.cmx Ocamlopt src/memory_state/abstract_value.cmx Ocamlopt src/wp/fol_why.cmx Ocamlopt cil/src/frontc/cabs2cil.cmx Ocamlopt cil/src/frontc/clexer.cmx Ocamlopt src/logic/description.cmx Ocamlopt src/kernel/alarms.cmx Ocamlopt src/ai/base.cmx Ocamlopt src/memory_state/int_Interv.cmx Ocamlopt src/kernel/stmts_graph.cmx Ocamlopt src/kernel/unroll_loops.cmx Ocamlopt src/kernel/loop.cmx Ocamlopt src/logic/translate_lightweight.cmx Ocamlopt src/aorai/promelaoutput.cmx Ocamlopt src/report/scan.cmx Ocamlopt src/wp/variables_analysis.cmx Ocamlopt cil/src/logic/logic_preprocess.cmx Ocamlopt src/kernel/cilE.cmx Ocamlopt src/ai/base_Set_Lattice.cmx Ocamlopt src/memory_state/locations.cmx Ocamlopt src/memory_state/int_Interv_Map.cmx Ocamlopt src/memory_state/tr_offset.cmx Ocamlopt src/memory_state/offsetmap_bitwise.cmx Ocamlopt src/aorai/logic_simplification.cmx Ocamlopt src/report/dump.cmx Ocamlopt cil/src/frontc/frontc.cmx Ocamlopt src/memory_state/shifted_Location.cmx Ocamlopt src/memory_state/new_offsetmap.cmx Ocamlopt src/memory_state/lmap_bitwise.cmx Ocamlopt src/memory_state/inout_type.cmx Ocamlopt src/pdg_types/pdgIndex.cmx Ocamlopt src/kernel/file.cmx Ocamlopt src/value/non_linear.cmx Ocamlopt src/inout/kf_state.cmx Ocamlopt src/aorai/data_for_aorai.cmx Ocamlopt src/memory_state/path_lattice.cmx Ocamlopt src/memory_state/offsetmap.cmx Ocamlopt src/memory_state/function_Froms.cmx Ocamlopt src/pdg_types/pdgTypes.cmx Ocamlopt src/aorai/aorai_utils.cmx Ocamlopt src/aorai/yaparser.cmx Ocamlopt src/aorai/promelaparser.cmx Ocamlopt src/aorai/promelaparser_withexps.cmx Ocamlopt src/aorai/abstract_ai.cmx Ocamlopt src/aorai/bycase_ai.cmx Ocamlopt src/aorai/aorai_visitors.cmx Ocamlopt src/memory_state/lmap.cmx Ocamlopt src/pdg_types/pdgMarks.cmx Ocamlopt src/pdg/pdg_state.cmx Ocamlopt src/aorai/yalexer.cmx Ocamlopt src/aorai/promelalexer.cmx Ocamlopt src/aorai/promelalexer_withexps.cmx Ocamlopt src/memory_state/cvalue.cmx Ocamlopt src/slicing_types/slicingInternals.cmx Ocamlopt src/slicing_types/slicingTypes.cmx Ocamlopt src/memory_state/widen_type.cmx Ocamlopt src/memory_state/state_set.cmx Ocamlopt src/memory_state/state_imp.cmx Ocamlopt src/kernel/db.cmx Ocamlopt src/memory_state/widen.cmx Ocamlopt src/kernel/command.cmx Ocamlopt src/misc/filter.cmx Ocamlopt src/memory_state/bit_model_access.cmx Ocamlopt src/logic/logic_interp.cmx Ocamlopt src/logic/infer_annotations.cmx Ocamlopt src/occurrence/register.cmx Ocamlopt src/metrics/metrics_base.cmx Ocamlopt src/syntactic_callgraph/register.cmx Ocamlopt src/value/kf_state.cmx Ocamlopt src/value/value_parameters.cmx Ocamlopt src/rte/rte.cmx Ocamlopt src/rte/register.cmx Ocamlopt src/from/from_register.cmx Ocamlopt src/users/users_register.cmx Ocamlopt src/constant_propagation/register.cmx Ocamlopt src/postdominators/print.cmx Ocamlopt src/inout/cumulative_analysis.cmx Ocamlopt src/inout/operational_inputs.cmx Ocamlopt src/inout/access_path.cmx Ocamlopt src/semantic_callgraph/register.cmx Ocamlopt src/impact/register.cmx Ocamlopt src/pdg/ctrlDpds.cmx Ocamlopt src/pdg/sets.cmx Ocamlopt src/scope/datascope.cmx Ocamlopt src/kernel/boot.cmx Ocamlopt src/aorai/aorai_register.cmx Ocamlopt src/report/register.cmx Ocamlopt src/security_slicing/components.cmx Ocamlopt src/wp/cil2cfg.cmx Ocamlopt src/wp/proof.cmx Ocamlopt src/kernel/task.cmx Packing lib/plugins/Occurrence.cmx Ocamlopt src/metrics/metrics_cabs.cmx Ocamlopt src/metrics/metrics_cilast.cmx Ocamlopt src/metrics/metrics_coverage.cmx Packing lib/plugins/Syntactic_callgraph.cmx Ocamlopt src/value/library_functions.cmx Ocamlopt src/value/mark_noresults.cmx Ocamlopt src/value/separate.cmx Ocamlopt src/value/value_util.cmx Packing lib/plugins/RteGen.cmx Packing lib/plugins/From.cmx Packing lib/plugins/Users.cmx Packing lib/plugins/Constant_Propagation.cmx Ocamlopt src/postdominators/compute.cmx Ocamlopt src/inout/inputs.cmx Ocamlopt src/inout/outputs.cmx Ocamlopt src/inout/derefs.cmx Packing lib/plugins/Semantic_callgraph.cmx Packing lib/plugins/Impact.cmx Ocamlopt src/pdg/build.cmx Ocamlopt src/pdg/annot.cmx Ocamlopt src/pdg/marks.cmx Ocamlopt src/scope/zones.cmx Ocamlopt src/scope/defs.cmx Packing lib/plugins/Aorai.cmx Packing lib/plugins/Report.cmx Packing lib/plugins/Security_slicing.cmx Ocamlopt src/wp/wpPropId.cmx Ocamlopt src/metrics/register.cmx Ocamlopt src/value/builtins.cmx Ocamlopt src/value/current_table.cmx Ocamlopt src/value/eval_exprs.cmx Packing lib/plugins/Postdominators.cmx Ocamlopt src/inout/register.cmx Ocamlopt src/pdg/register.cmx Packing lib/plugins/Scope.cmx Packing lib/plugins/Aorai.cmxs Packing lib/plugins/Report.cmxs Packing lib/plugins/Security_slicing.cmxs Ocamlopt src/wp/wpStrategy.cmx Packing lib/plugins/Metrics.cmx Ocamlopt src/value/initial_state.cmx Ocamlopt src/value/eval_logic.cmx Ocamlopt src/value/register.cmx Packing lib/plugins/Inout.cmx Packing lib/plugins/Pdg.cmx Ocamlopt src/wp/wpFroms.cmx Ocamlopt src/wp/calculus.cmx Ocamlopt src/value/locals_scoping.cmx Ocamlopt src/sparecode/sparecode_params.cmx Ocamlopt src/slicing/slicingParameters.cmx Ocamlopt src/slicing/slicingMarks.cmx Ocamlopt src/wp/wpAnnot.cmx Ocamlopt src/value/eval_stmts.cmx Ocamlopt src/sparecode/globs.cmx Ocamlopt src/sparecode/marks.cmx Ocamlopt src/slicing/slicingMacros.cmx Ocamlopt src/slicing/slicingCmds.cmx Ocamlopt src/wp/wpo.cmx Ocamlopt src/value/eval_funs.cmx Ocamlopt src/sparecode/transform.cmx Ocamlopt src/slicing/slicingActions.cmx Ocamlopt src/wp/prover.cmx Ocamlopt src/wp/datalib.cmx Packing lib/plugins/Value.cmx Ocamlopt src/sparecode/register.cmx Ocamlopt src/slicing/fct_slice.cmx Packing lib/plugins/Sparecode.cmx Ocamlopt src/wp/funvar_mem.cmx Ocamlopt src/wp/runtime_mem.cmx Ocamlopt src/wp/store_mem.cmx Ocamlopt src/wp/hoare_mem.cmx Ocamlopt src/wp/translate_prop.cmx Ocamlopt src/wp/cfgpropid.cmx Ocamlopt src/slicing/printSlice.cmx Ocamlopt src/slicing/slicingTransform.cmx Ocamlopt src/slicing/slicingProject.cmx Ocamlopt src/slicing/register.cmx Ocamlopt src/wp/cfgWeakestPrecondition.cmx Ocamlopt src/wp/cfgProof.cmx Packing lib/plugins/Slicing.cmx Ocamlopt src/wp/register.cmx Packing lib/plugins/Wp.cmx Packing lib/plugins/Wp.cmxs Linking bin/toplevel.opt Copying to native kernel API => Unwrapping files-to-be-installed.