Skip to content

Move from stephenrkell/cil to goblint/cil #180

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
probablytom wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Move from stephenrkell/cil to goblint/cil #180

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7830be3
Remove original CIL
probablytom Sep 29, 2025
43eec0d
goblint/cil liballocs with fixed makefiles, working `allocscc`
probablytom Oct 23, 2025
29d1049
More-or-less building liballocs with goblint/cil
probablytom Dec 16, 2025
bd10eb2
Install cil+configurator to `lib/ocaml`, remove manual deps
probablytom Dec 18, 2025
df74633
Merge branch 'master' into goblint-cil
probablytom Dec 18, 2025
3afcf2b
Clean up clang-18 reference from Makefile (CC is gcc unless CIL_CC set)
probablytom Dec 19, 2025
ebedd22
Update apt dependencies for circleCI
probablytom Dec 19, 2025
fc8d5e8
.gitignore changes to ensure lib/ocaml exists
probablytom Dec 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions .circleci/config.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,11 @@ jobs:
ocaml ocamlbuild ocaml-findlib libnum-ocaml-dev \
default-jdk-headless python3 \
make git gawk gdb wget libc6-dbg \
ocaml-dune libdune-ocaml-dev \
libyojson-ocaml libyojson-ocaml-dev libppx-deriving-yojson-ocaml-dev \
libzarith-ocaml libzarith-ocaml-dev \
libnum-ocaml libnum-ocaml-dev \
libcsexp-ocaml libcsexp-ocaml-dev \
libunwind-dev libunwind-dev:i386 linux-libc-dev-i386-cross libc6-dev-i386 \
libboost-iostreams-dev libboost-regex-dev \
libboost-serialization-dev libboost-filesystem-dev libffi-dev \
Expand Down
9 changes: 6 additions & 3 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,12 @@
[submodule "contrib/donald"]
path = contrib/donald
url = https://github.com/stephenrkell/donald.git
[submodule "contrib/cil"]
path = contrib/cil
url = https://github.com/stephenrkell/cil.git
[submodule "contrib/elftin"]
path = contrib/elftin
url = https://github.com/stephenrkell/elftin.git
[submodule "contrib/dune"]
path = contrib/dune
url = git@github.com:probablytom/dune
[submodule "contrib/cil"]
path = contrib/cil
url = https://github.com/probablytom/cil.git
9 changes: 7 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,11 +220,16 @@ look something like the following.

$ sudo apt-get install libelf-dev libdw-dev binutils-dev \
autoconf automake libtool pkg-config autoconf-archive \
g++ ocaml ocamlbuild ocaml-findlib \
g++ ocaml ocamlbuild ocaml-dune ocaml-findlib \
libppx-deriving-yojson-ocaml-dev \
default-jre-headless python3 python \
make git gawk gdb wget \
libunwind-dev libc6-dev-i386 zlib1g-dev libc6-dbg \
libboost-{iostreams,regex,serialization,filesystem}-dev && \
libboost-{iostreams,regex,serialization,filesystem}-dev \
cppo libcsexp-ocaml libcsexp-ocaml-dev libyojson-ocaml \
libyojson-ocaml-dev libnum-ocaml libnum-ocaml-dev \
libzarith-ocaml libzarith-ocaml-dev \
linux-libc-dev-i386-cross libdune-ocaml-dev && \
git clone https://github.com/stephenrkell/liballocs.git && \
cd liballocs && \
git submodule update --init --recursive && \
Expand Down
41 changes: 33 additions & 8 deletions contrib/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
CONTRIB := $(realpath $(dir $(THIS_MAKEFILE)))

export OCAML_LIBDEST := ${CONTRIB}/../lib/ocaml/
export PATH := ${PATH}:${OCAML_LIBDEST}bin/

export CIL_CC := gcc
export CC := ${CIL_CC}

# NOTE all this env.sh amounts to just a different way to do
# ./configure --with-blah=/path/to/blah ?
# ... but we prefer it because it's more compositional:
Expand Down Expand Up @@ -121,29 +127,48 @@ clean::
# ----------------------------cil

.PHONY: build-cil
build-cil: cil.stamp
build-cil: cil.stamp mainFeature.cmx

.PHONY: dune-configurator
dune-configurator:
cd dune && dune build -p dune-configurator && dune install -p dune-configurator --prefix=${OCAML_LIBDEST} --libdir=${OCAML_LIBDEST}

# PROBLEM: cil's ocamlbuild takes a significant time to re-run even in the
# case where nothing's changed. So use a stamp to run around that.
cil.stamp: cil/Makefile $(shell find cil -name '*.c' -o -name '*.ml' -o -name '*.mli' -o -name '*.in' -o -name '*.mly' )
$(MAKE) -C cil all install-local && touch $@
cil/Makefile: cil/configure
cd cil && CC=$${ALLOCSCC_CC:-$${CC:-cc}} ./configure INSTALL="`which install` -p"
cil.stamp: goblint-cil
goblint-cil: dune-configurator
cd cil && dune build && dune build @install && dune install --prefix=${OCAML_LIBDEST} --libdir=${OCAML_LIBDEST}
touch cil.stamp

CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/cil/lib\n
CONFIG_MK += \nCIL_ROOT ?= $(CONTRIB)/cil/\n
varlist += CIL_ROOT
export CIL_ROOT

CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/../lib/ocaml/goblint-cil/\n
varlist += CIL_INSTALL
export CIL_INSTALL

.PHONY: mainFeature.cmx
mainFeature.cmx:
cd cil && cp ${CIL_ROOT}/src/mainFeature.ml ${CIL_ROOT}/src/mainFeature.mli ${CIL_INSTALL} && ocamlfind ocamlopt -c ${CIL_INSTALL}/mainFeature.mli && ocamlfind ocamlopt -linkpkg -package dynlink -package findlib -package str -package zarith -I ${CIL_INSTALL} ${CIL_INSTALL}goblintCil.cmxa ${CIL_INSTALL}mainFeature.ml

.PHONY: goblint-cil-deps
goblint-cil-deps: cppo csexp dune-configurator yojson

clean::
$(MAKE) -C cil clean
cd cil && dune clean
cd yojson && dune uninstall -p yojson --prefix=/usr/lib/ocaml/
cd csexp && dune uninstall -p csexp --prefix=/usr/lib/ocaml/
cd cppo && dune uninstall -p cppo --prefix=/usr/lib/ocaml/
cd dune && dune uninstall -p dune-configurator --prefix=/usr/lib/ocaml/
rm -f cil.stamp

# ----------------------------toolsub

.PHONY: build-toolsub
build-toolsub: build-cil
$(MAKE) -C toolsub wrapper-recursive cilpp-recursive # don't build clang-based cccppp
$(MAKE) -C toolsub/wrapper/example/constructor-priority-checker dumpconstr
#$(MAKE) -C toolsub/wrapper/example/constructor-priority-checker dumpconstr
CONFIG_MK += \nTOOLSUB ?= $(CONTRIB)/toolsub\n
varlist += TOOLSUB

Expand Down
2 changes: 1 addition & 1 deletion contrib/cil
Open in desktop
Submodule cil updated 856 files
1 change: 1 addition & 0 deletions contrib/dune
Open in desktop
Submodule dune added at ef3b45
2 changes: 1 addition & 1 deletion contrib/toolsub
Open in desktop
Submodule toolsub updated 7 files
+7 −6 cilpp/src/Makefile
+1 −1 cilpp/src/cilpp.ml
+10 −9 cilpp/src/cilpp_common.ml
+1 −1 cilpp/src/cilprint.ml
+2 −2 wrapper/example/constructor-priority-checker/Makefile
+4 −4 wrapper/example/constructor-priority-checker/dumpconstr.ml
+1 −0 wrapper/src/mkstemp_stubs.c
52 changes: 26 additions & 26 deletions include/liballocs_cil_inlines.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,15 +85,15 @@ CURRENT_ALLOC_VARS_QUALIFIERS void *__current_allocsite CURRENT_ALLOC_VARS_QUALI

void __liballocs_unindex_stack_objects_counted_by(unsigned long *, void *frame_addr);

extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_caller_frame_cleanup)(void *counter);
extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_caller_frame_cleanup)(void *counter)
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_caller_frame_cleanup)(void *counter);
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_caller_frame_cleanup)(void *counter)
{
__liballocs_unindex_stack_objects_counted_by((unsigned long *) counter, __builtin_frame_address(0));
}

/* alloca helpers */
extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_sp)(void);
extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_sp)(void)
extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_sp)(void);
extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_sp)(void)
{
unsigned long our_sp;
#ifdef UNW_TARGET_X86
Expand All @@ -104,8 +104,8 @@ extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liba
return (const void*) our_sp;
}

extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_bp)(void);
extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_bp)(void)
extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_bp)(void);
extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_bp)(void)
{
return (const void *) __builtin_frame_address(0);
}
Expand All @@ -118,8 +118,8 @@ extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liba
* for the allocation site / type metadata. We call a helper to get
* the *overall* size, and then the __liballocs_notify_and_adjust_alloca()
* function will fill in both the header and the trailer. */
extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_size)(unsigned long orig_size);
extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_size)(unsigned long orig_size)
extern inline unsigned long (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_size)(unsigned long orig_size);
extern inline unsigned long (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_size)(unsigned long orig_size)
{
/* Insert heap trailer etc..
* Basically we have to do everything that our malloc hooks, allocator wrappers
Expand All @@ -138,8 +138,8 @@ extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __li
* we don't track them. */
}

extern inline void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller);
extern inline void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller)
extern inline void *(__attribute__((always_inline,gnu_inline)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller);
extern inline void *(__attribute__((always_inline,gnu_inline)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller)
{
#ifndef LIBALLOCS_NO_ZERO
__builtin_memset(allocated, 0, tweaked_size);
Expand Down Expand Up @@ -213,8 +213,8 @@ struct __liballocs_memrange_cache
};
extern struct __liballocs_memrange_cache /* __thread */ __liballocs_ool_cache;

extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)));
extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)))
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)));
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)))
{
#ifdef DEBUG
unsigned visited_linear = 0u;
Expand Down Expand Up @@ -247,8 +247,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
#endif
}

extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i)
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i)
{
__liballocs_check_cache_sanity(cache);
/* unset validity and make this the next victim */
Expand All @@ -266,8 +266,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
__liballocs_check_cache_sanity(cache);
}

extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
{
__liballocs_check_cache_sanity(cache);
/* Put us at the head of the LRU chain. */
Expand All @@ -284,8 +284,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
__liballocs_check_cache_sanity(cache);
}

extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i)
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i)
{
__liballocs_check_cache_sanity(cache);
/* make sure we're not the next victim */
Expand All @@ -299,8 +299,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
__liballocs_check_cache_sanity(cache);
}

extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
{
__liballocs_check_cache_sanity(cache);
if (cache->head_mru != i)
Expand All @@ -312,10 +312,10 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
}

extern inline
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
__liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, const void *obj, struct uniqtype *t, unsigned long require_period);
extern inline
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
__liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, const void *obj, struct uniqtype *t, unsigned long require_period)
{
#ifndef LIBALLOCS_NOOP_INLINES
Expand Down Expand Up @@ -352,10 +352,10 @@ __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, co
}

extern inline
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
__liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *cache, const void *obj, unsigned long require_period);
extern inline
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
__liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *cache, const void *obj, unsigned long require_period)
{
#ifndef LIBALLOCS_NOOP_INLINES
Expand Down Expand Up @@ -389,8 +389,8 @@ __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *ca
return (struct __liballocs_memrange_cache_entry_s *)(void*)0;
}

extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_cached_object_type)(const void *addr);
extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_cached_object_type)(const void *addr)
extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline)) __liballocs_get_cached_object_type)(const void *addr);
extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline)) __liballocs_get_cached_object_type)(const void *addr)
{
struct __liballocs_memrange_cache_entry_s *found = __liballocs_memrange_cache_lookup_notype(
&__liballocs_ool_cache,
Expand Down
8 changes: 8 additions & 0 deletions lib/ocaml/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# We want to ensure lib/ocaml _always_ exists, but we can't commit an empty dir
# to a git repo. There has to be some content at this path. However, everything
# that gets placed here is a build artifact that shouldn't be committed.

# So: ignore everything in this directory _except_ this file, so that this file
# ensures the path exists.
*
!.gitignore
19 changes: 12 additions & 7 deletions tools/lang/c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,14 @@ OCAMLFIND ?= ocamlfind
ifeq ($(CIL_INSTALL),)
$(error "Expected CIL_INSTALL to be set")
endif
ifeq ($(CIL_ROOT),)
$(error "Expected CIL_ROOT to be set")
endif
CILLY ?= $(CIL_INSTALL)/../bin/cilly
CIL_TOOLS ?= cilallocs dumpallocs monalloca dumpmemacc trapptrwrites
OCAMLFLAGS += -package findlib
OCAMLFLAGS += -I $(CIL_INSTALL)/cil -I $(dir $(THIS_MAKEFILE))/cilallocs
OCAMLFLAGS += -package findlib -package goblint-cil
OCAMLFLAGS += -I $(dir $(THIS_MAKEFILE))/cilallocs
OCAMLFLAGS += -open GoblintCil -open GoblintCil.Cilint

CIL_TOOLS_SRC := $(shell find $(CIL_TOOLS) $(realpath $(dir $(THIS_MAKEFILE)))/lib -name '*.ml')

Expand All @@ -24,13 +28,14 @@ DEPS += $(OCAML_DEPS)
-include $(DEPS)

%.cmxs: %.cmx
$(OCAMLFIND) ocamlopt -shared -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) $+
eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlopt -shared -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) $+
%.cmx %.cmi: %.ml
$(OCAMLFIND) ocamlopt -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) -c "$<"
eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlopt -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) -c "$<"
goblintCil.cmo: goblintCil.ml ;
%.cmo %.cmi: %.ml
$(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -c "$<"
eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -c "$<"
%.cma: %.cmo
$(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -a $+
eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -a $+

# build cilallocs first
dumpallocs/dumpallocs.cmx: cilallocs/cilallocs.cmx
Expand All @@ -46,4 +51,4 @@ monalloca/monalloca.cmo: cilallocs/cilallocs.cmo

.PHONY: clean
clean:
for dir in $(CIL_TOOLS); do (cd $$dir && rm -f *.o *.cmo *.cma *.cmi *.cmx *.cmxa *.cmxs *.cil.c *.i ); done
for dir in $(CIL_TOOLS); do (cd $$dir && rm -f *.o *.cmo *.cma *.cmi *.cmx *.cmxa *.cmxs *.cil.c *.i *.d ); done
11 changes: 4 additions & 7 deletions tools/lang/c/bin/allocscc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,11 @@ import os, sys, re, subprocess, tempfile
REAL_FILE = os.path.realpath(__file__)
REAL_DIR = os.path.realpath(os.path.dirname(REAL_FILE))
liballocs_base = os.path.realpath(REAL_DIR + "/../../../..")
cil_base = os.environ.get("CIL_ROOT", liballocs_base + "/contrib/cil/")
cilly_cmd = cil_base + "/_build/install/default/bin/cilly"
sys.path.append(liballocs_base + "/tools")
from allocscompilerwrapper import *
existing_cil_install = os.environ.get("CIL_INSTALL")
if existing_cil_install == None:
cilly_cmd = liballocs_base + "/contrib/cil/bin/cilly"
existing_cil_install = liballocs_base + "/contrib/cil/lib"
else:
cilly_cmd = existing_cil_install + "/../bin/cilly"
existing_cil_install = os.environ.get("CIL_INSTALL", cil_base + "_build/install/default/lib/goblint-cil")
existing_elftin = os.environ.get("ELFTIN")
if existing_elftin == None:
os.putenv("ELFTIN", liballocs_base + "/contrib/elftin")
Expand Down Expand Up @@ -95,7 +92,7 @@ class AllocsCC(AllocsCompilerWrapper):
return []
return [
"--decil",
"--native",
#"--native",
"--load=%s" % (self.getLibAllocsBaseDir() + "/tools/lang/c/cilallocs/cilallocs.cmxs"),
"--load=%s" % (self.getLibAllocsBaseDir() + "/tools/lang/c/dumpallocs/dumpallocs.cmxs"),
"--dodumpallocs",
Expand Down
Loading