Add multi-language documentation #334
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Update the README to reflect that SMACK now supports many languages Add a short tutorial on how to compile a new language into SMACK.
zvonimir
requested changes
Aug 4, 2018
README.md
Outdated
| (and experimentally, C++ and Objective-C) via the [Clang](http://clang.llvm.org) compiler. | ||
| We are in the process of adding support for FORTRAN | ||
| (via [Flang](https://github.com/flang-compiler/flang)), Rust, and Swift. | ||
| In general, any AoT comipler that targets LLVM can be used with SMACK |
There was a problem hiding this comment.
Expand AoT into what it actually means.
docs/language.md
Outdated
|
|
||
| ### Prerequisites | ||
|
|
||
| - An AoT compiler that targets the same version of LLVM as SMACK. |
docs/language.md
Outdated
| @@ -0,0 +1,50 @@ | |||
|
|
|||
| # How to use SMACK with your own programming language. | |||
There was a problem hiding this comment.
Maybe change to: Using SMACK with your Favorite Programming Language
docs/language.md
Outdated
|
|
||
| # How to use SMACK with your own programming language. | ||
|
|
||
| SMACK can be used to verify any langauge that comiples to LLVM IR. Because there are so many languages, we are unable to provide out-of-the-box for the majority of LLVM languages. However, you can still verify code by manually compiling to LLVM and running SMACK on the LLVM IR. |
There was a problem hiding this comment.
In theory, SMACK can be used... In practice, how well SMACK would work on your favorite language is not always clear. Our experience though has been positive, and currently we have rudimentary SMACK extensions for ...
You also have a typo here - comiples
docs/language.md
Outdated
|
|
||
| For compatibility, SMACK version == LLVM version - 2. So, for LLVM 3.9, you want SMACK 1.9, etc. | ||
|
|
||
| - A working C interop |
There was a problem hiding this comment.
It is unclear what interop means.
docs/language.md
Outdated
|
|
||
| Step 2: Compile to LLVM IR | ||
|
|
||
| Compile your code to either a .ll or a .bc file (the two formats are equivalent). Most compilers provide a command-line option like `-emit-llvm` or `-output-ll`. You should also add debug symbols, which is `-g` on most compilers. Disabling optimizations may also be useful, with `-O0` or similar. |
There was a problem hiding this comment.
Please keep all lines of text under 80 columns wide.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Update the README to reflect that SMACK now supports
many languages
Add a short tutorial on how to compile a new language
into SMACK.