diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index b04af99c8e..bd6ea7716e 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1366,10 +1366,10 @@ module INT-SYMBOLIC [symbolic] rule X %Int N => X requires 0 <=Int X andBool X X [simplification] - rule 0 < 0 [simplification] - rule X >>Int 0 => X [simplification] - rule 0 >>Int _ => 0 [simplification] + rule X < X [simplification, preserves-definedness] + rule 0 < 0 requires 0 <=Int Y [simplification, preserves-definedness] + rule X >>Int 0 => X [simplification, preserves-definedness] + rule 0 >>Int Y => 0 requires 0 <=Int Y [simplification, preserves-definedness] endmodule module INT-SYMBOLIC-KORE [symbolic, haskell] diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index 420f6c1676..e154e7b653 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java @@ -146,6 +146,9 @@ private void llvmKompile(String type, String executable) { if (options.llvmMutableBytes) { args.add("--mutable-bytes"); } + if (options.llvmHiddenVisibility) { + args.add("--hidden-visibility"); + } if (options.debug) { args.add("-g"); diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java index 282b58c2f0..b330a5268a 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java @@ -119,4 +119,10 @@ public List convert(String str) { description = "Use a faster, unsound representation for byte arrays on the LLVM backend", hidden = true) public boolean llvmMutableBytes; + + @Parameter( + names = "--llvm-hidden-visibility", + description = "Build the llvm backend with -fvisibility=hidden", + hidden = true) + public boolean llvmHiddenVisibility; }