Semantics of C in K
If this readme isn't enough, consider checking out these papers to better understand this project:
kccis meant to act a lot like
gcc. You use it and run programs the same way. If your system provides a command
kccalready (of which there are several possible), we also provide the synonym
kccgenerates act like normal programs. Both the output to stdout (e.g.,
printf), as well as the return value of the program should be what you expect. In terms of operational behavior, a correct program compiled with kcc should act the same as one compiled with
kcc -hfor some compile-time options. For most programs, you only need to run
kcc program.cand everything will work.
a.out, the resulting program is a native executable and can be run on any platform provided it has access to the runtime libraries required by the dynamic linker.
configin the current directory if the program got stuck while executing, or can be generated using
kcc -din case of compile-time errors.
kcchas been run on C source files, it should produce an executable script (
The tests directory includes many of the tests we've used to build confidence in the correctness of our semantics. To run the basic set of tests, run
make checkfrom the top-level directory. For performance reasons, you may first wish to run
kserverin the background, and pass a
-jflag to make to get the desired level of parallelism.
KCC comes by default with relatively limited support for the C library. If you are compiling and linking a program that makes use of many library functions, you may likely run into CV-CID1 and UB-TDR2 errors, signifying respectively that the function you are calling was not declared in the appropriate header file, or that it was declared, but no definition exists currently in the semantics.
We recommend if you wish to execute such programs that you contact Runtime Verification, Inc, which licenses a tool RV-Match based on this semantics which is capable of executing such programs by linking against the native code provided on your system for these libraries. For more information, contact https://runtimeverification.com/support.
examples: some simple example programs for demonstrating the undefinedness that we can catch.
x86-gcc-limited-libc: library headers and some library sources for functions that aren't defined directly in the semantics itself.
parser: the lightly modified OCaml CIL C parser.
scripts: e.g., the
program-runner, the script that becomes
semantics: the K C semantics.
tests: undefinedness, gcc-torture, juliet, llvm, etc.
dist: created during the build process, this is where the final products go. For convenience, consider adding this directory to your
During the build process, three versions of the semantics are built using
kompilewith different flags: a "deterministic" version, a version for supporting non-deterministic expression sequencing, and another with non-deterministic thread-interleaving. These all get copied to
dist/along with the contents of x86-gcc-limited-libc/include and the scripts/kcc script. Finally, make runs
kcc -s -sharedon all the libc source files in x86-gcc-limited-libc/src.
kccscript is the primary interface to our semantics. Invoking
kcc myprogram.cresults in the contents of the parameter C source file being piped through, consecutively:
The root of this AST is a single
TranslationUnitterm, which is then interpreted by our "translation" semantics.
See semantics/c/README.md for more details.