cil-project · jerhard · Jul 8, 2015 · Jul 21, 2015 · Dec 22, 2015 · Jul 18, 2016
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -0,0 +1,56 @@
+name: build and run tests
+# https://github.com/avsm/setup-ocaml
+
+on:
+  - push
+  - pull_request
+
+jobs:
+  tests:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+          # - windows-latest
+        ocaml-version:
+          - 4.04.2
+          - 4.05.0
+          - 4.06.1
+          - 4.07.1
+          - 4.08.1
+          - 4.09.1
+          - 4.10.1
+          - 4.11.2
+          - 4.12.0
+
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+
+      - name: Cache # https://github.com/marketplace/actions/cache
+        uses: actions/cache@v2.0.0
+        with:
+          # A list of files, directories, and wildcard patterns to cache and restore
+          path: |
+            ~/.opam
+            _opam
+          # An explicit key for restoring and saving the cache
+          key: ${{ runner.os }}-new-${{ matrix.ocaml-version }}
+
+      - name: Setup OCaml ${{ matrix.ocaml-version }}
+        uses: avsm/setup-ocaml@v1
+        with:
+          ocaml-version: ${{ matrix.ocaml-version }}
+
+      - run: opam pin add goblint-cil.dev . --no-action
+      - run: opam depext goblint-cil --yes
+      - run: opam depext goblint-cil --yes --with-doc
+      - run: opam depext goblint-cil --yes --with-test
+      - run: opam install . --deps-only --with-doc --with-test
+      - run: opam exec -- dune build
+      - run: opam exec -- dune runtest
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,5 @@
+_opam/
+src/.merlin
 # /
 /camlprim0.obj
 /*.a
@@ -92,6 +94,7 @@
 
 # /lib/cil
 /lib/cil
+/lib/goblint-cil
 
 # /share
 /share/cil/ocamlpath
@@ -390,4 +393,26 @@
 /test/small2/funcptr3
 /test/small2/merge-ar
 /test/small2/libmerge.a
-
+/test/small2/*.o
+.vscode/settings.json
+src/ext/blockinggraph/.merlin
+src/ext/callgraph/.merlin
+src/ext/zrapp/.merlin
+src/ext/simplify/.merlin
+src/ext/simplemem/.merlin
+src/ext/sfi/.merlin
+src/ext/pta/.merlin
+src/ext/partial/.merlin
+src/ext/oneret/.merlin
+src/ext/logwrites/.merlin
+src/ext/logcalls/.merlin
+src/ext/llvm/.merlin
+src/ext/liveness/.merlin
+src/ext/inliner/.merlin
+src/ext/heapify/.merlin
+src/ext/epicenter/.merlin
+src/ext/dataslicing/.merlin
+src/ext/ccl/.merlin
+src/ext/canonicalize/.merlin
+src/ext/cqualann/.merlin
+src/ext/syntacticsearch/.merlin
diff --git a/.merlin b/.merlin
@@ -2,11 +2,11 @@ S src/
 S src/ext/
 S src/ext/pta/
 S src/frontc/
-S ocamlutil/
+S src/ocamlutil/
 B _build/
 B _build/src/
 B _build/src/ext/
 B _build/src/ext/pta/
 B _build/src/frontc/
-B _build/ocamlutil/
+B _build/src/ocamlutil/
 PKG findlib
diff --git a/.travis.yml b/.travis.yml
diff --git a/LICENSE b/LICENSE
@@ -1,10 +1,12 @@
-Copyright (c) 2001-2013,
+Copyright (c) 2001-2020,
  George C. Necula    <necula@cs.berkeley.edu>
  Scott McPeak        <smcpeak@cs.berkeley.edu>
  Wes Weimer          <weimer@cs.berkeley.edu>
  Ben Liblit          <liblit@cs.wisc.edu>
  Matt Harren         <matth@cs.berkeley.edu>
  Gabriel Kerneis     <kerneis@pps.univ-paris-diderot.fr>
+ Ralf Vogler         <ralf.vogler@tum.de>
+ Michael Schwarz     <m.schwarz@tum.de>
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without

diff --git a/META.goblint-cil.template b/META.goblint-cil.template
@@ -0,0 +1,11 @@
+# DUNE_GEN
+
+package "default-features" (
+requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.syntacticsearch"
+version = "1.7.8"
+)
+
+package "all-features" (
+requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.zrapp goblint-cil.syntacticsearch"
+version = "1.7.8"
+)
diff --git a/Makefile.in b/Makefile.in
@@ -57,10 +57,10 @@ CILLIB_TARGETS=
 CILLY_EXE_FILES=
 
 CIL_PLUGINS_DIR = src/ext
-CIL_EXCLUDE_PLUGINS =
+CIL_EXCLUDE_PLUGINS = dune
 CIL_PLUGINS = $(addprefix $(OBJDIR)/,$(filter-out $(addprefix $(CIL_PLUGINS_DIR)/, $(CIL_EXCLUDE_PLUGINS)),$(wildcard $(CIL_PLUGINS_DIR)/*)))
 
-CIL_DEFAULT_PLUGINS = $(patsubst $(CIL_PLUGINS_DIR)/%/default,cil.%,$(wildcard $(CIL_PLUGINS_DIR)/*/default))
+CIL_DEFAULT_PLUGINS = $(patsubst $(CIL_PLUGINS_DIR)/%/default,goblint-cil.%,$(wildcard $(CIL_PLUGINS_DIR)/*/default))
 
 ifneq ($(OCAMLC),no)
   CILLIB_TARGETS  += $(OBJDIR)/src/cil.cma
@@ -106,7 +106,7 @@ ocamlbuild:
 META:
 	@rm -f $@
 	@printf "description = \"C Intermediate Language\"\n" >>$@
-	@printf "requires = \"unix str num dynlink\"\n" >>$@
+	@printf "requires = \"unix str zarith dynlink\"\n" >>$@
 	@printf "version = \"$(CIL_VERSION)\"\n\n" >>$@
 	@printf "archive(byte) = \"cil.cma\"\n" >>$@
 	@printf "archive(native) = \"cil.cmxa\"\n\n" >>$@
@@ -115,7 +115,7 @@ META:
 	@printf "version = \"$(CIL_VERSION)\"\n" >>$@
 	@printf ")\n\n" >>$@
 	@printf "package \"all-features\" (\n" >>$@
-	@printf "requires=\"$(patsubst $(OBJDIR)/$(CIL_PLUGINS_DIR)/%,cil.%,$(CIL_PLUGINS))\"\n" >>$@
+	@printf "requires=\"$(patsubst $(OBJDIR)/$(CIL_PLUGINS_DIR)/%,goblint-cil.%,$(CIL_PLUGINS))\"\n" >>$@
 	@printf "version = \"$(CIL_VERSION)\"\n" >>$@
 	@printf ")\n\n" >>$@
 	@$(foreach plugin,$(patsubst $(OBJDIR)/$(CIL_PLUGINS_DIR)/%,%,$(CIL_PLUGINS)),\
@@ -167,6 +167,9 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
 	@echo "  sizeof_float: int;      (* Size of \"float\" *)"       >> $@
 	@echo "  sizeof_double: int;     (* Size of \"double\" *)"      >> $@
 	@echo "  sizeof_longdouble: int; (* Size of \"long double\" *)" >> $@
+	@echo "  sizeof_floatcomplex: int;      (* Size of \"float _Complex\" *)"       >> $@
+	@echo "  sizeof_doublecomplex: int;     (* Size of \"double _Complex\" *)"      >> $@
+	@echo "  sizeof_longdoublecomplex: int; (* Size of \"long double _Complex\" *)" >> $@
 	@echo "  sizeof_void: int;       (* Size of \"void\" *)"        >> $@
 	@echo "  sizeof_fun: int;        (* Size of function *)"        >> $@
 	@echo "  size_t: string;         (* Type of \"sizeof(T)\" *)"   >> $@
@@ -181,6 +184,9 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
 	@echo "  alignof_float: int;     (* Alignment of \"float\" *)"  >> $@
 	@echo "  alignof_double: int;    (* Alignment of \"double\" *)" >> $@
 	@echo "  alignof_longdouble: int;  (* Alignment of \"long double\" *)" >> $@
+	@echo "  alignof_floatcomplex: int;     (* Alignment of \"float _Complex\" *)"  >> $@
+	@echo "  alignof_doublecomplex: int;    (* Alignment of \"double _Complex\" *)" >> $@
+	@echo "  alignof_longdoublecomplex: int;  (* Alignment of \"long double _Complex\" *)" >> $@
 	@echo "  alignof_str: int;       (* Alignment of strings *)" >> $@
 	@echo "  alignof_fun: int;       (* Alignment of function *)" >> $@
 	@echo "  alignof_aligned: int;   (* Alignment of anything with the \"aligned\" attribute *)" >> $@
@@ -277,7 +283,7 @@ distclean: clean
 clean: $(CILLYDIR)/Makefile
 	rm -rf $(OBJDIR)
 	rm -f $(BINDIR)/$(CILLY).*
-	rm -rf lib/cil share/
+	rm -rf lib/goblint-cil share/
 	rm -f META
 	rm -rf doc/html/
 	rm -rf doc/cilcode.tmp/
@@ -346,10 +352,10 @@ endif
 install-findlib: META $(CILLIB_FILES) $(CILLIB_TARGETS) uninstall-findlib
 	mkdir -p $(OCAMLFIND_INSTALLDIR)
 	OCAMLFIND_DESTDIR=$(OCAMLFIND_INSTALLDIR) \
-	  $(OCAMLFIND) install cil META $(CILLIB_TARGETS) `cat $(CILLIB_FILES)`
+	  $(OCAMLFIND) install goblint-cil META $(CILLIB_TARGETS) `cat $(CILLIB_FILES)`
 
 uninstall-findlib:
-	OCAMLFIND_DESTDIR=$(OCAMLFIND_INSTALLDIR) $(OCAMLFIND) remove cil
+	OCAMLFIND_DESTDIR=$(OCAMLFIND_INSTALLDIR) $(OCAMLFIND) remove goblint-cil
 
 .PHONY: install-data uninstall-data
 install-data:

diff --git a/README.md b/README.md
@@ -1,45 +1,64 @@
 C Intermediate Language (CIL)
 ============================
 
-Linux [![Linux build Status](https://travis-ci.org/cil-project/cil.svg?branch=develop)](https://travis-ci.org/cil-project/cil)
-Windows [![Windows build status](https://ci.appveyor.com/api/projects/status/jtgf72r03jnge7jw/branch/develop?svg=true)](https://ci.appveyor.com/project/kerneis/cil/branch/develop)
-
-
 CIL is a front-end for the C programming language that facilitates
 program analysis and transformation. CIL will parse and typecheck a
 program, and compile it into a simplified subset of C.
 
-CIL supports ANSI C as well as most of the extensions of the GNU C and
-Microsoft C compilers. A Perl script acts as a drop in replacement for
-either gcc or Microsoft's cl, and allows merging of the source files in
-your project. Other features include support for control-flow and
-points-to analyses.
+`goblint-cil` is a fork of CIL that supports C99 as well as most of the
+extensions of the GNU C. It makes many changes to the original CIL in an effort
+to modernize it and keep up with the latest versions of the C language. Here is
+an incomplete list of some of the ways `goblint-cil` improves upon CIL:
+- Proper support for C99, ([#9][i9]) and VLAs in particular ([#5][i5], [#7][pr7])
+- It uses [Zarith][zarith] instead of the deprecated [Num][num]
+- Support for more recent OCaml versions (≥ 4.06)
+- Large integer constants that do not fit in an OCaml `int` are represented as a
+  `string` instead of getting truncated
+- Syntactic search extension ([#21][pr21])
+- Some warnings were made optional
+- Unmaintained extensions ([#30][pr30]) were removed
+- Many bug fixes
+
+[zarith]: https://github.com/ocaml/Zarith
+[num]: https://github.com/ocaml/num
+[i5]: https://github.com/goblint/cil/issues/5
+[pr7]: https://github.com/goblint/cil/pull/7
+[i9]: https://github.com/goblint/cil/issues/9
+[pr21]: https://github.com/goblint/cil/pull/21
+[pr30]: https://github.com/goblint/cil/pull/30
+
+Quickstart
+----------
+
+Install the latest release of `goblint-cil` with [opam][]:
 
-Quick start
------------
+    opam install goblint-cil
 
-Install the latest release of CIL with [opam][]:
+Read the excellent [CIL tutorial][tuto] by Zachary Anderson, much of which
+still applies to `goblint-cil`.
 
-    opam install cil
+**ATTENTION:** Don't install the `cil` package. This is the unmaintained
+original version of CIL.
 
-Read the excellent [CIL tutorial][tuto] by Zachary Anderson, and
-check out the accompanying [project template][template].
+[tuto]: https://web.eecs.umich.edu/~weimerw/2011-6610/reading/ciltut.pdf
 
-[tuto]: https://bitbucket.org/zanderso/cil-template/downloads/ciltut.pdf
-[template]: https://bitbucket.org/zanderso/cil-template
+Installation from Source
+------------------------
 
-Installation
------------
+Prerequisites:
+- opam
+- Some C compiler (preferably `gcc`)
+- Perl
 
-To build and install CIL, you need the OCaml compiler, perl, and
-[ocamlfind][findlib].  (Of course, you also need some C compiler,
-preferably gcc.)
+First create a local opam switch and install all dependencies:
 
-Run the following commands to build and install CIL:
+    opam switch create .
+
+Then, run the following commands to build and install `goblint-cil`:
 
     ./configure
     make
-    make test       # regression test suite, optionnal
+    make test       # runs the regression test suite, optional
     make install    # as root or using sudo
 
 If you want to install to some other directory, you can tweak the prefix
@@ -48,17 +67,26 @@ directory:
 
     ./configure --prefix=`opam config var prefix`
 
-[findlib]: http://projects.camlcity.org/projects/findlib.html
-[opam]: http://opam.ocamlpro.com/
+[opam]: https://opam.ocaml.org/
+
+Build with Dune
+---------------
+Alternatively, you can use [dune] to build `goblint-cil`. Run the following
+commands to build and test `goblint-cil`:
+
+    dune build
+    dune runtest    # runs the regression test suite
+
+[dune]: https://github.com/ocaml/dune
 
 Usage
 -----
 
-You can use cilly (installed in /usr/local/bin by default) as a drop-in
-replacement for gcc to compile and link your programs.
+You can use cilly (installed in `/usr/local/bin` by default) as a drop-in
+replacement for `gcc` to compile and link your programs.
 
-You can also use CIL as a library to write your own programs.  For
-instance in the OCaml toplevel using [findlib][]:
+You can also use `goblint-cil` as a library to write your own programs. For
+instance in the OCaml toplevel using [Findlib][findlib]:
 
     $ ocaml
             Objective Caml version 4.00.1
@@ -67,29 +95,20 @@ instance in the OCaml toplevel using [findlib][]:
     [...]
     # #require "cil";;
     [...]
-    # Cil.cilVersion;;           
+    # Cil.cilVersion;;
     - : string = "1.7.3"
 
+[findlib]: http://projects.camlcity.org/projects/findlib.html
 
-More documentation
-------------------
-
-The documentation is located in the doc/html/cil directory.  The API
-documentation (generated by ocamldoc) is in the api subdirectory.
-
-To (re)build the doc, you need [Hevea][] and run:
-
-    make doc
-
-You can also [browse the documentation online][doc].
+TODO
+----
 
-[hevea]: http://hevea.inria.fr/ "Hevea - LaTex to HTML translator"
-[doc]:   http://cil-project.github.io/cil/doc/html/cil/ "Cil online doc"
+- C11 support ([#13][i13])
 
-Ressources
-----------
+[i13]: https://github.com/goblint/cil/issues/13
 
-* [Mailing list](https://lists.sourceforge.net/lists/listinfo/cil-users)
-* [Bug tracker](http://sourceforge.net/p/cil/bugs/)
+License
+-------
+`goblint-cil` is licensed under the BSD license. See [LICENSE][license].
 
-CIL is maintained by Gabriel Kerneis <gabriel@kerneis.info>
+[license]: https://github.com/goblint/cil/blob/develop/LICENSE
diff --git a/_tags b/_tags
@@ -1,5 +1,5 @@
 # Traverse only subdirectories containing source code
-true: -traverse
+true: -traverse, package(zarith), package(stdlib-shims), package(batteries), package(yojson), package(ppx_deriving_yojson)
 <src>: include
 # build every cmo in debug mode (for cil.cma)
 <**/*.cmo>: debug