diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index bd2e2a175..25968b7d4 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -578,11 +578,11 @@ and xlate_global : x -> Llvm.llvalue -> Global.t = its own initializer *) Hashtbl.set memo_global ~key:llg ~data:(Global.mk g typ loc) ; let init = - match (Llvm.classify_value llg, Llvm.linkage llg) with - | _, (External | External_weak) -> None - | GlobalVariable, _ -> + match (Llvm.classify_value llg, Llvm.global_initializer llg) with + | GlobalVariable, Some llinit -> let siz = size_of x (Llvm.element_type llt) in - Some (xlate_value x (Llvm.global_initializer llg), siz) + let init = xlate_value x llinit in + Some (init, siz) | _ -> None in Global.mk ?init g typ loc diff --git a/sledge/test/Makefile b/sledge/test/Makefile index ec9f69d42..5c55cafcc 100644 --- a/sledge/test/Makefile +++ b/sledge/test/Makefile @@ -42,7 +42,7 @@ $(MODEL_DIR)/cxxabi.bc : $(MODEL_DIR)/cxxabi.cpp @(cd $(dir $@) && clang $(CLANG_ARGS) -I../llvm/projects/libcxxabi/include -I../llvm/projects/libcxxabi/src -c -emit-llvm cxxabi.cpp) # compile c to llvm bitcode -%.bc : %.c $(MODEL_DIR)/cxxabi.bc +%.bc : %.c @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).c -o - | opt $(OPT_ARGS) -o $(notdir $*).bc) # $(MODEL_DIR)/cxxabi.bc diff --git a/sledge/test/exec/globals.c b/sledge/test/exec/globals.c new file mode 100644 index 000000000..800fb1eec --- /dev/null +++ b/sledge/test/exec/globals.c @@ -0,0 +1,22 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +char* mutable_string = "a string"; +const char* immutable_string = "a string"; + +int mutable_int = 0; +const int immutable_int = 0; + +int main() { + int mi = mutable_int; + int imi = immutable_int; + char* c = mutable_string; + char a_char = *mutable_string; + char b_char = *immutable_string; + + return 0; +}