import the frama-c source code analysis tool

Frama-C is a suite of tools dedicated to the analysis of the source code of
software written in C.

Frama-C gathers several static analysis techniques in a single collaborative
framework. The collaborative approach of Frama-C allows static analyzers to
build upon the results already computed by other analyzers in the framework.
Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer
and dependency analysis.

1 files changed, 381 insertions, 0 deletions

diff --git a/devel/frama-c/PLIST b/devel/frama-c/PLIST
new file mode 100644
index 00000000000..9fb523e741b
--- /dev/null
+++ b/devel/frama-c/PLIST
@@ -0,0 +1,381 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2009/09/11 15:09:35 tonio Exp $
+bin/caduceus
+bin/frama-c
+bin/frama-c-gui
+bin/frama-c-gui.byte
+bin/frama-c.byte
+bin/gwhy
+bin/gwhy-bin
+bin/jessie
+bin/krakatoa
+bin/rv_merge
+bin/simplify2why
+bin/tool-stat
+bin/why
+bin/why-config
+bin/why-cpulimit
+bin/why-dp
+bin/why-obfuscator
+bin/why-stat
+bin/why2html
+lib/frama-c/about_dialog.cmi
+lib/frama-c/abstract_interp.cmi
+lib/frama-c/abstract_value.cmi
+lib/frama-c/alarms.cmi
+lib/frama-c/alpha.cmi
+lib/frama-c/annotations.cmi
+lib/frama-c/ast.cmi
+lib/frama-c/ast_info.cmi
+lib/frama-c/ast_printer.cmi
+lib/frama-c/availexpslv.cmi
+lib/frama-c/base.cmi
+lib/frama-c/baseUtils.cmi
+lib/frama-c/base_Set_Lattice.cmi
+lib/frama-c/binary_cache.cmi
+lib/frama-c/bit_model_access.cmi
+lib/frama-c/bit_utils.cmi
+lib/frama-c/boot.cmi
+lib/frama-c/buckx.cmi
+lib/frama-c/cabs.cmi
+lib/frama-c/cabs2cil.cmi
+lib/frama-c/cabshelper.cmi
+lib/frama-c/cabsvisit.cmi
+lib/frama-c/callgraph.cmi
+lib/frama-c/cfg.cmi
+lib/frama-c/cil.cmi
+lib/frama-c/cilE.cmi
+lib/frama-c/cil_computation.cmi
+lib/frama-c/cil_const.cmi
+lib/frama-c/cil_datatype.cmi
+lib/frama-c/cil_types.cmi
+lib/frama-c/cilglobopt.cmi
+lib/frama-c/cilmsg.cmi
+lib/frama-c/ciltools.cmi
+lib/frama-c/cilutil.cmi
+lib/frama-c/clexer.cmi
+lib/frama-c/clist.cmi
+lib/frama-c/cmdline.cmi
+lib/frama-c/computation.cmi
+lib/frama-c/concreteModel.cmi
+lib/frama-c/config.cmi
+lib/frama-c/cparser.cmi
+lib/frama-c/cprint.cmi
+lib/frama-c/cvalue_type.cmi
+lib/frama-c/dGraphModel.cmi
+lib/frama-c/dGraphView.cmi
+lib/frama-c/dGraphViewItem.cmi
+lib/frama-c/dataflow.cmi
+lib/frama-c/datatype.cmi
+lib/frama-c/db.cmi
+lib/frama-c/db_types.cmi
+lib/frama-c/deadcodeelim.cmi
+lib/frama-c/debug.cmi
+lib/frama-c/descr.cmi
+lib/frama-c/design.cmi
+lib/frama-c/dominators.cmi
+lib/frama-c/dynamic.cmi
+lib/frama-c/dynlink_common_interface.cmi
+lib/frama-c/errorloc.cmi
+lib/frama-c/escape.cmi
+lib/frama-c/expcompare.cmi
+lib/frama-c/extlib.cmi
+lib/frama-c/file.cmi
+lib/frama-c/filetree.cmi
+lib/frama-c/filter.cmi
+lib/frama-c/frontc.cmi
+lib/frama-c/function_Froms.cmi
+lib/frama-c/globals.cmi
+lib/frama-c/graph.cmi
+lib/frama-c/growArray.cmi
+lib/frama-c/gtk_helper.cmi
+lib/frama-c/gui_init.cmi
+lib/frama-c/hook.cmi
+lib/frama-c/infer_annotations.cmi
+lib/frama-c/inout_type.cmi
+lib/frama-c/int_Base.cmi
+lib/frama-c/int_Interv.cmi
+lib/frama-c/int_Interv_Map.cmi
+lib/frama-c/inthash.cmi
+lib/frama-c/ival.cmi
+lib/frama-c/journal.cmi
+lib/frama-c/kernel.cmi
+lib/frama-c/kernel_function.cmi
+lib/frama-c/kernel_type.cmi
+lib/frama-c/kind.cmi
+lib/frama-c/lattice_With_Isotropy.cmi
+lib/frama-c/launcher.cmi
+lib/frama-c/lexerhack.cmi
+lib/frama-c/liveness.cmi
+lib/frama-c/lmap.cmi
+lib/frama-c/lmap_bitwise.cmi
+lib/frama-c/lmap_whole.cmi
+lib/frama-c/locations.cmi
+lib/frama-c/log.cmi
+lib/frama-c/logic_builtin.cmi
+lib/frama-c/logic_const.cmi
+lib/frama-c/logic_env.cmi
+lib/frama-c/logic_interp.cmi
+lib/frama-c/logic_lexer.cmi
+lib/frama-c/logic_parser.cmi
+lib/frama-c/logic_preprocess.cmi
+lib/frama-c/logic_ptree.cmi
+lib/frama-c/logic_typing.cmi
+lib/frama-c/logic_utils.cmi
+lib/frama-c/loop.cmi
+lib/frama-c/machdep.cmi
+lib/frama-c/machdep_ppc_32.cmi
+lib/frama-c/machdep_ppc_32_diab.cmi
+lib/frama-c/machdep_x86_16.cmi
+lib/frama-c/machdep_x86_32.cmi
+lib/frama-c/machdep_x86_64.cmi
+lib/frama-c/map_Lattice.cmi
+lib/frama-c/mergecil.cmi
+lib/frama-c/mergemap.cmi
+lib/frama-c/messages.cmi
+lib/frama-c/mweak.cmi
+lib/frama-c/my_bigint.cmi
+lib/frama-c/namespace.cmi
+lib/frama-c/new_offsetmap.cmi
+lib/frama-c/obfuscate.cmi
+lib/frama-c/offsetmap.cmi
+lib/frama-c/offsetmap_bitwise.cmi
+lib/frama-c/oneret.cmi
+lib/frama-c/origin.cmi
+lib/frama-c/parameters.cmi
+lib/frama-c/patch.cmi
+lib/frama-c/path_lattice.cmi
+lib/frama-c/pdgIndex.cmi
+lib/frama-c/pdgMarks.cmi
+lib/frama-c/pdgTypes.cmi
+lib/frama-c/plugin.cmi
+lib/frama-c/plugins/Jessie.cma
+lib/frama-c/plugins/Jessie.cmxs
+lib/frama-c/plugins/Ltl_to_acsl.cmo
+lib/frama-c/plugins/Ltl_to_acsl.cmxs
+lib/frama-c/pretty_source.cmi
+lib/frama-c/pretty_utils.cmi
+lib/frama-c/printer.cmi
+lib/frama-c/project.cmi
+lib/frama-c/project_manager.cmi
+lib/frama-c/ptmap.cmi
+lib/frama-c/ptset.cmi
+lib/frama-c/qstack.cmi
+lib/frama-c/rangemap.cmi
+lib/frama-c/reachingdefs.cmi
+lib/frama-c/relations_type.cmi
+lib/frama-c/rmciltmps.cmi
+lib/frama-c/rmtmps.cmi
+lib/frama-c/service_graph.cmi
+lib/frama-c/setWithNearest.cmi
+lib/frama-c/shifted_Location.cmi
+lib/frama-c/signature.cmi
+lib/frama-c/slicingInternals.cmi
+lib/frama-c/slicingTypes.cmi
+lib/frama-c/source_manager.cmi
+lib/frama-c/source_viewer.cmi
+lib/frama-c/special_hooks.cmi
+lib/frama-c/state_set.cmi
+lib/frama-c/stmts_graph.cmi
+lib/frama-c/subst.cmi
+lib/frama-c/translate_lightweight.cmi
+lib/frama-c/type.cmi
+lib/frama-c/unicode.cmi
+lib/frama-c/unmarshal.cmi
+lib/frama-c/unmarshal_nums.cmi
+lib/frama-c/unroll_loops.cmi
+lib/frama-c/usedef.cmi
+lib/frama-c/utf8_logic.cmi
+lib/frama-c/viewGraph.cmi
+lib/frama-c/viewGraph_select.cmi
+lib/frama-c/viewGraph_utils.cmi
+lib/frama-c/visitor.cmi
+lib/frama-c/warning_manager.cmi
+lib/frama-c/whitetrack.cmi
+lib/frama-c/widen.cmi
+lib/frama-c/widen_type.cmi
+lib/frama-c/xDot.cmi
+lib/frama-c/xDotDraw.cmi
+lib/frama-c/zrapp.cmi
+man/man1/frama-c-gui.1
+man/man1/frama-c.1
+man/man1/why.1
+share/frama-c/Makefile.common
+share/frama-c/Makefile.config
+share/frama-c/Makefile.dynamic
+share/frama-c/Makefile.dynamic_config
+share/frama-c/Makefile.plugin
+share/frama-c/builtin.c
+share/frama-c/builtin.h
+share/frama-c/caduceus/coq/caduceus_tactics.v
+share/frama-c/caduceus/coq/caduceus_why.v
+share/frama-c/caduceus/harvey/caduceus_why.rv
+share/frama-c/caduceus/isabelle/caduceus_why.thy
+share/frama-c/caduceus/why/caduceus.why
+share/frama-c/caduceus/why/caduceus_arith.why
+share/frama-c/coq/jessie_why.v
+share/frama-c/fluctuat.h
+share/frama-c/frama-c.rc
+share/frama-c/jessie/assert.h
+share/frama-c/jessie/ctype.h
+share/frama-c/jessie/jc.cmi
+share/frama-c/jessie/jc.cmo
+share/frama-c/jessie/jc.cmx
+share/frama-c/jessie/jc.o
+share/frama-c/jessie/jc_ast.cmi
+share/frama-c/jessie/jc_common_options.cmi
+share/frama-c/jessie/jc_constructors.cmi
+share/frama-c/jessie/jc_env.cmi
+share/frama-c/jessie/jc_envset.cmi
+share/frama-c/jessie/jc_fenv.cmi
+share/frama-c/jessie/jc_iterators.cmi
+share/frama-c/jessie/jc_noutput.cmi
+share/frama-c/jessie/jc_output.cmi
+share/frama-c/jessie/jc_output_misc.cmi
+share/frama-c/jessie/jc_pervasives.cmi
+share/frama-c/jessie/jc_poutput.cmi
+share/frama-c/jessie/jc_region.cmi
+share/frama-c/jessie/jc_stdlib.cmi
+share/frama-c/jessie/jc_type_var.cmi
+share/frama-c/jessie/jessie_exact_prolog.h
+share/frama-c/jessie/jessie_machine_prolog.h
+share/frama-c/jessie/jessie_prolog.h
+share/frama-c/jessie/lib.cmi
+share/frama-c/jessie/loc.cmi
+share/frama-c/jessie/option_misc.cmi
+share/frama-c/jessie/output.cmi
+share/frama-c/jessie/pp.cmi
+share/frama-c/jessie/prolog.c
+share/frama-c/jessie/rc.cmi
+share/frama-c/jessie/stddef.h
+share/frama-c/jessie/stdio.h
+share/frama-c/jessie/stdlib.h
+share/frama-c/jessie/string.h
+share/frama-c/jessie/strings.h
+share/frama-c/jessie/unistd.h
+share/frama-c/jessie/wchar.h
+share/frama-c/libc.c
+share/frama-c/libc.h
+share/frama-c/machine.h
+share/frama-c/malloc.c
+share/frama-c/math.c
+share/frama-c/math.h
+share/frama-c/why/Makefile
+share/frama-c/why/acsl.why
+share/frama-c/why/java_api/java/io/BufferedWriter.java
+share/frama-c/why/java_api/java/io/File.java
+share/frama-c/why/java_api/java/io/FileDescriptor.java
+share/frama-c/why/java_api/java/io/FileNotFoundException.java
+share/frama-c/why/java_api/java/io/FileReader.java
+share/frama-c/why/java_api/java/io/FilterOutputStream.java
+share/frama-c/why/java_api/java/io/IOException.java
+share/frama-c/why/java_api/java/io/InputStream.java
+share/frama-c/why/java_api/java/io/InputStreamReader.java
+share/frama-c/why/java_api/java/io/ObjectStreamClass.java
+share/frama-c/why/java_api/java/io/OutputStream.java
+share/frama-c/why/java_api/java/io/OutputStreamWriter.java
+share/frama-c/why/java_api/java/io/PrintStream.java
+share/frama-c/why/java_api/java/io/Reader.java
+share/frama-c/why/java_api/java/io/Serializable.java
+share/frama-c/why/java_api/java/io/StreamTokenizer.java
+share/frama-c/why/java_api/java/lang/ArrayStoreException.java
+share/frama-c/why/java_api/java/lang/CharSequence.java
+share/frama-c/why/java_api/java/lang/Character.java
+share/frama-c/why/java_api/java/lang/Class.java
+share/frama-c/why/java_api/java/lang/Cloneable.java
+share/frama-c/why/java_api/java/lang/Comparable.java
+share/frama-c/why/java_api/java/lang/Double.java
+share/frama-c/why/java_api/java/lang/Exception.java
+share/frama-c/why/java_api/java/lang/IllegalArgumentException.java
+share/frama-c/why/java_api/java/lang/Integer.java
+share/frama-c/why/java_api/java/lang/Long.java
+share/frama-c/why/java_api/java/lang/Math.java
+share/frama-c/why/java_api/java/lang/Number.java
+share/frama-c/why/java_api/java/lang/NumberFormatException.java
+share/frama-c/why/java_api/java/lang/Object.java
+share/frama-c/why/java_api/java/lang/RuntimeException.java
+share/frama-c/why/java_api/java/lang/String.java
+share/frama-c/why/java_api/java/lang/StringBuffer.java
+share/frama-c/why/java_api/java/lang/System.java
+share/frama-c/why/java_api/java/lang/Throwable.java
+share/frama-c/why/java_api/java/util/AbstractMap.java
+share/frama-c/why/java_api/java/util/Collection.java
+share/frama-c/why/java_api/java/util/HashMap.java
+share/frama-c/why/java_api/java/util/HashMapIntegerInteger.java
+share/frama-c/why/java_api/java/util/HashMapIntegerLong.java
+share/frama-c/why/java_api/java/util/Iterator.java
+share/frama-c/why/java_api/java/util/Locale.java
+share/frama-c/why/java_api/java/util/Map.java
+share/frama-c/why/java_api/java/util/Set.java
+share/frama-c/why/javacard_api/com/sun/javacard/impl/Constants.java
+share/frama-c/why/javacard_api/com/sun/javacard/impl/NativeMethods.java
+share/frama-c/why/javacard_api/com/sun/javacard/impl/PackedBoolean.java
+share/frama-c/why/javacard_api/com/sun/javacard/impl/PrivAccess.java
+share/frama-c/why/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java
+share/frama-c/why/javacard_api/java/lang/Exception.java
+share/frama-c/why/javacard_api/java/lang/IndexOutOfBoundsException.java
+share/frama-c/why/javacard_api/java/lang/Object.java
+share/frama-c/why/javacard_api/java/lang/RuntimeException.java
+share/frama-c/why/javacard_api/java/lang/Throwable.java
+share/frama-c/why/javacard_api/javacard/framework/AID.java
+share/frama-c/why/javacard_api/javacard/framework/APDU.java
+share/frama-c/why/javacard_api/javacard/framework/APDUException.java
+share/frama-c/why/javacard_api/javacard/framework/Applet.java
+share/frama-c/why/javacard_api/javacard/framework/CardException.java
+share/frama-c/why/javacard_api/javacard/framework/CardRuntimeException.java
+share/frama-c/why/javacard_api/javacard/framework/Dispatcher.java
+share/frama-c/why/javacard_api/javacard/framework/ISO7816.java
+share/frama-c/why/javacard_api/javacard/framework/ISOException.java
+share/frama-c/why/javacard_api/javacard/framework/JCSystem.java
+share/frama-c/why/javacard_api/javacard/framework/OwnerPIN.java
+share/frama-c/why/javacard_api/javacard/framework/PIN.java
+share/frama-c/why/javacard_api/javacard/framework/PINException.java
+share/frama-c/why/javacard_api/javacard/framework/Shareable.java
+share/frama-c/why/javacard_api/javacard/framework/SystemException.java
+share/frama-c/why/javacard_api/javacard/framework/TransactionException.java
+share/frama-c/why/javacard_api/javacard/framework/UserException.java
+share/frama-c/why/javacard_api/javacard/framework/Util.java
+share/frama-c/why/javacard_api/javacard/security/CryptoException.java
+share/frama-c/why/javacard_api/javacard/security/DESKey.java
+share/frama-c/why/javacard_api/javacard/security/DSAKey.java
+share/frama-c/why/javacard_api/javacard/security/DSAPrivateKey.java
+share/frama-c/why/javacard_api/javacard/security/DSAPublicKey.java
+share/frama-c/why/javacard_api/javacard/security/Key.java
+share/frama-c/why/javacard_api/javacard/security/KeyBuilder.java
+share/frama-c/why/javacard_api/javacard/security/KeyPair.java
+share/frama-c/why/javacard_api/javacard/security/MessageDigest.java
+share/frama-c/why/javacard_api/javacard/security/PrivateKey.java
+share/frama-c/why/javacard_api/javacard/security/PublicKey.java
+share/frama-c/why/javacard_api/javacard/security/RSAPrivateCrtKey.java
+share/frama-c/why/javacard_api/javacard/security/RSAPrivateKey.java
+share/frama-c/why/javacard_api/javacard/security/RSAPublicKey.java
+share/frama-c/why/javacard_api/javacard/security/RandomData.java
+share/frama-c/why/javacard_api/javacard/security/SecretKey.java
+share/frama-c/why/javacard_api/javacard/security/Signature.java
+share/frama-c/why/javacard_api/javacardx/crypto/Cipher.java
+share/frama-c/why/low-level.why
+share/frama-c/why/model0.why.src
+share/frama-c/why/model1.why.src
+share/frama-c/why/model2.why.src
+share/frama-c/why/test.why
+share/frama-c/why/test_low-level.why.src
+share/frama-c/why/test_model0.why.src
+share/frama-c/why/test_model1.why.src
+share/frama-c/why/test_model2.why.src
+share/frama-c/why/why-logo-1.png
+share/frama-c/why/why/arrays.why
+share/frama-c/why/why/bool.why
+share/frama-c/why/why/floats.why
+share/frama-c/why/why/floats_common.why
+share/frama-c/why/why/floats_full.why
+share/frama-c/why/why/floats_multi_rounding.why
+share/frama-c/why/why/floats_strict.why
+share/frama-c/why/why/integer.why
+share/frama-c/why/why/jessie.why
+share/frama-c/why/why/mix.why
+share/frama-c/why/why/prelude.why
+share/frama-c/why/why/real.why
+share/manuals/acsl-implementation.pdf
+share/manuals/aorai-manual.pdf
+share/manuals/plugin-developer.pdf
+share/manuals/value-analysis.pdf
+@pkgdir lib/frama-c/plugins/gui