Merge branch 'develop' into c11-generic

Author: sim642

.github/workflows/tests.yml

@@ -15,7 +15,7 @@ jobs:
           - ubuntu-latest
           # - windows-latest
         ocaml-version:
-          - 4.04.2
+          # - 4.04.2
           - 4.05.0
           - 4.06.1
           - 4.07.1
@@ -32,20 +32,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
-      - name: Cache # https://github.com/marketplace/actions/cache
-        uses: actions/[email protected]
-        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
+        uses: ocaml/setup-ocaml@v2
         with:
-          ocaml-version: ${{ matrix.ocaml-version }}
+          ocaml-compiler: ${{ matrix.ocaml-version }}
 
       - run: opam pin add goblint-cil.dev . --no-action
       - run: opam depext goblint-cil --yes

.merlin

@@ -9,4 +9,4 @@ B _build/src/ext/
 B _build/src/ext/pta/
 B _build/src/frontc/
 B _build/src/ocamlutil/
-PKG findlib
+PKG findlib, zarith

CHANGES

@@ -1,12 +1,24 @@
+## Unreleased
+* Add ends to locations, allowing for ranges.
+* Add additional expression locations to statements, etc.
+* Drop all support for MSVC
+
+## Older versions
+
+18 November 2021: goblint-cil-1.8.2
+
+    * Add columns to locations.
+    * Add support for __int128, __int128_t and __uint128_t.
+
 18 May 2021: goblint-cil-1.8.0
 
-    * Proper support for C99, ([#9][i9]) and VLAs in particular ([#5][i5], [#7][pr7])
+    * Proper support for C99, (#9) and VLAs in particular (#5, #7)
     * 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])
+    * Syntactic search extension (#21)
     * Some warnings were made optional
-    * Unmaintained extensions ([#30][pr30]) were removed
+    * Unmaintained extensions (#30) were removed
     * Many bug fixes
 
 24 July 2013: cil-1.7.3

META.goblint-cil.template

@@ -2,10 +2,10 @@
 
 package "default-features" (
 requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.syntacticsearch"
-version = "1.8.1"
+version = "1.8.2"
 )
 
 package "all-features" (
 requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.zrapp goblint-cil.syntacticsearch"
-version = "1.8.1"
+version = "1.8.2"
 )

Makefile.in

@@ -146,7 +146,6 @@ $(CILLY): $(CILLY_EXE_BIN) $(CILLYDIR)/Makefile
 	$(MAKE) -C $(CILLYDIR)
 
 # Create the machine dependency module
-# If the cl command cannot be run then the MSVC part will be identical to GCC
 .PHONY : machdep
 machdep: $(OBJDIR)/machdep.ml
 $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
@@ -203,15 +202,6 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
 	@echo "let gcc = {" >>$@
 	@$(OBJDIR)/machdep-ml.exe >>$@
 	@echo "}"          >>$@
-	@if cl -D_MSVC $< -Fe$(OBJDIR)/machdep-ml.exe -Fo$(OBJDIR)/machdep-ml.obj ;then \
-           echo "let hasMSVC = true" >>$@ ;\
-	         echo "let msvc = {" >>$@ ;\
-	           $(OBJDIR)/machdep-ml.exe >>$@ ;\
-	         echo "}"          >>$@ \
-        ;else \
-           echo "let hasMSVC = false" >>$@ ;\
-					 echo "let msvc = gcc" >> $@ \
-			  ;fi
 	@echo "let theMachine : mach ref = ref gcc" >>$@
 
 $(CILLYDIR)/App/$(CILLYMOD).pm: $(CILLYDIR)/App/$(CILLYMOD).pm.in src/machdep-ml.c configure.ac Makefile.in

README.md

@@ -15,6 +15,7 @@ an incomplete list of some of the ways `goblint-cil` improves upon CIL:
 - 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])
+- More precise locations (with columns)
 - Some warnings were made optional
 - Unmaintained extensions ([#30][pr30]) were removed
 - Many bug fixes
@@ -35,12 +36,14 @@ Install the latest release of `goblint-cil` with [opam][]:
     opam install goblint-cil
 
 Read the excellent [CIL tutorial][tuto] by Zachary Anderson, much of which
-still applies to `goblint-cil`.
+still applies to `goblint-cil`. The repository referenced in that document has now moved [here][repo].
 
 **ATTENTION:** Don't install the `cil` package. This is the unmaintained
 original version of CIL.
 
+
 [tuto]: https://web.eecs.umich.edu/~weimerw/2011-6610/reading/ciltut.pdf
+[repo]: https://github.com/zanderso/cil-template
 
 Installation from Source
 ------------------------
@@ -96,7 +99,7 @@ instance in the OCaml toplevel using [Findlib][findlib]:
     # #require "cil";;
     [...]
     # Cil.cilVersion;;
-    - : string = "1.8.1"
+    - : string = "1.8.2"
 
 [findlib]: http://projects.camlcity.org/projects/findlib.html
 

config.mk.in

@@ -1,3 +1,2 @@
 # A bunch of variables  -*- Mode: makefile -*-
-export HAS_MSVC=@HAS_MSVC@
 export @DEFAULT_COMPILER@=1

configure

@@ -655,7 +655,6 @@ CIL_VERSION_MINOR
 CIL_VERSION_MAJOR
 DEFAULT_CIL_MODE
 DEFAULT_COMPILER
-HAS_MSVC
 EMUL
 LIBOBJS
 CYGPATH
@@ -2531,7 +2530,7 @@ ac_config_files="$ac_config_files stamp-h"
 # Assign here the CIL version numbers
 CIL_VERSION_MAJOR=1
 CIL_VERSION_MINOR=8
-CIL_VERSION_REV=1
+CIL_VERSION_REV=2
 CIL_VERSION=$CIL_VERSION_MAJOR.$CIL_VERSION_MINOR.$CIL_VERSION_REV
 
 # make sure I haven't forgotten to run autoconf
@@ -3470,30 +3469,6 @@ test -n "$target_alias" &&
 DEFAULT_COMPILER=_GNUCC
 DEFAULT_CIL_MODE=GNUCC
 
-# is the microsoft compiler available?
-# hmm.. I think we should check the version or something, because
-# sometimes people have Common Lisp's interpreter called 'cl' ..
-{ printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for msvc cl.exe (optional)" >&5
-printf %s "checking for msvc cl.exe (optional)... " >&6; }
-# See if CC points to the MS compiler
-if "$CC" 2>&1 | grep "Microsoft" >/dev/null; then
-  { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: found, set as default" >&5
-printf "%s\n" "found, set as default" >&6; }
-  HAS_MSVC=yes
-  DEFAULT_COMPILER=_MSVC
-  DEFAULT_CIL_MODE=MSVC
-  CFLAGS="-WX"
-else
-  if cl 2>&1 | grep "Microsoft" >/dev/null ;then
-     { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: found" >&5
-printf "%s\n" "found" >&6; }
-     HAS_MSVC=yes
-  else
-     { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: not found" >&5
-printf "%s\n" "not found" >&6; }
-     HAS_MSVC=no
-  fi
-fi
 
 # ------------------- OCaml ----------------
 
@@ -5266,7 +5241,6 @@ rm -f core conftest.err conftest.$ac_objext conftest.beam conftest.$ac_ext
 printf "%s\n" "$THREAD_IS_KEYWORD" >&6; }
 
 # Does gcc add underscores to identifiers to make assembly labels?
-# (I think MSVC always does)
 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking if gcc adds underscores to assembly labels." >&5
 printf %s "checking if gcc adds underscores to assembly labels.... " >&6; }
 cat confdefs.h - <<_ACEOF >conftest.$ac_ext
@@ -6046,7 +6020,6 @@ printf "%s\n" "$real_type" >&6; }
 
 
 
-
 # finish the configure script and generate various files; ./configure
 # will apply variable substitutions to <filename>.in to generate <filename>;
 
@@ -7433,7 +7406,6 @@ fi
 cat <<EOF
 
 CIL configuration:
-  (optional) cl.exe found:    HAS_MSVC           $HAS_MSVC
   gcc to use                  CC                 $CC
   default compiler            DEFAULT_COMPILER   $DEFAULT_COMPILER
   CIL version                 CIL_VERSION        $CIL_VERSION

configure.ac

@@ -33,7 +33,7 @@ AC_PREREQ([2.71])
 # Assign here the CIL version numbers
 CIL_VERSION_MAJOR=1
 CIL_VERSION_MINOR=8
-CIL_VERSION_REV=1
+CIL_VERSION_REV=2
 CIL_VERSION=$CIL_VERSION_MAJOR.$CIL_VERSION_MINOR.$CIL_VERSION_REV
 
 # make sure I haven't forgotten to run autoconf
@@ -82,26 +82,6 @@ AC_EXEEXT
 DEFAULT_COMPILER=_GNUCC
 DEFAULT_CIL_MODE=GNUCC
 
-# is the microsoft compiler available?
-# hmm.. I think we should check the version or something, because
-# sometimes people have Common Lisp's interpreter called 'cl' ..
-AC_MSG_CHECKING(for msvc cl.exe (optional))
-# See if CC points to the MS compiler
-if "$CC" 2>&1 | grep "Microsoft" >/dev/null; then
-  AC_MSG_RESULT([found, set as default])
-  HAS_MSVC=yes
-  DEFAULT_COMPILER=_MSVC
-  DEFAULT_CIL_MODE=MSVC
-  CFLAGS="-WX"
-else
-  if cl 2>&1 | grep "Microsoft" >/dev/null ;then
-     AC_MSG_RESULT(found)
-     HAS_MSVC=yes
-  else
-     AC_MSG_RESULT(not found)
-     HAS_MSVC=no
-  fi
-fi
 
 # ------------------- OCaml ----------------
 
@@ -155,7 +135,6 @@ AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main(int __thread) { return 0; }])],
 AC_MSG_RESULT($THREAD_IS_KEYWORD)
 
 # Does gcc add underscores to identifiers to make assembly labels?
-# (I think MSVC always does)
 AC_MSG_CHECKING([if gcc adds underscores to assembly labels.])
 AC_LINK_IFELSE([AC_LANG_SOURCE([int main() { __asm__("jmp _main"); }])],
                   UNDERSCORE_NAME=true,
@@ -186,7 +165,6 @@ CIL_CHECK_INTEGER_TYPE(wchar_t, TYPE_WCHAR_T)
 # names of the variables that get substituted in files; for example,
 # write @CIL_VERSION@ somewhere in a written file to get it substituted
 AC_SUBST(EMUL)
-AC_SUBST(HAS_MSVC)
 AC_SUBST(DEFAULT_COMPILER)
 AC_SUBST(DEFAULT_CIL_MODE)
 AC_SUBST(CIL_VERSION_MAJOR)
@@ -216,7 +194,6 @@ AC_OUTPUT
 cat <<EOF
 
 CIL configuration:
-  (optional) cl.exe found:    HAS_MSVC           $HAS_MSVC
   gcc to use                  CC                 $CC
   default compiler            DEFAULT_COMPILER   $DEFAULT_COMPILER
   CIL version                 CIL_VERSION        $CIL_VERSION

dune-project

@@ -2,12 +2,11 @@
 (name goblint-cil)
 (implicit_transitive_deps false)
 (generate_opam_files true)
-(version 1.8.1)
+(version 1.8.2)
 (source (github goblint/cil))
-(homepage "https://cil-project.github.io/cil/")
 ; (documentation "https://goblint.github.io/cil")
 (authors "[email protected]")
-(maintainers "Michael Schwarz <[email protected]>" "Ralf Vogler <[email protected]>")
+(maintainers "Michael Schwarz <[email protected]>" "Simmo Saan <[email protected]>" "Ralf Vogler <[email protected]>")
 (license "BSD-3-Clause")
 
 (package
@@ -16,16 +15,17 @@
   (description "\
 This is a fork of the 'cil' package needed to build 'goblint'.
 Changes:
-- Proper support for C99, (#9) and VLAs in particular (#5, #7)
+- Proper support for C99 and VLAs in particular
 - It uses Zarith instead of the deprecated 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)
+- Syntactic search extension
+- More precise locations (with columns)
 - Some warnings were made optional
-- Unmaintained extensions (#30) were removed
+- Unmaintained extensions were removed
 - Many bug fixes")
   (depends
-    (ocaml (>= 4.04.2))
+    (ocaml (>= 4.05.0))
     ocamlfind
     zarith
     (hevea :with-doc)