K框架中C的语义

kcc的作用很像gcc。您可以使用它并以相同的方式运行程序。如果您的系统已经提供了命令kcc（有多种可能），我们还将提供同义词kclang。

kcc生成的程序的行为类似于普通程序。输出tostdout（例如printf）以及程序的返回值都应该是您所期望的。就操作行为而言，用kcc编译的正确程序的行为应与用gcc编译的程序相同。

看一下kcc -h中的一些编译时选项。对于大多数程序，您只需要运行kcc program.c，一切都会正常。

编译程序并生成a.out输出文件后，结果程序是本机可执行文件，并且可以在任何平台上运行，只要它可以访问动态链接程序所需的运行时库即可。

如果您尝试运行未定义的程序（或缺少语义的程序），则该程序将被卡住。该消息应该告诉您它卡在哪里，并可能提示原因。如果您需要帮助解密输出或帮助理解为什么未定义程序，请将最终配置发送给我们。如果使用默认设置，则在程序执行时卡住该配置位于当前目录的文件config中，或者可以使用kcc -din编译时错误生成该配置。

一旦在C源文件上运行了kcc，它将生成一个可执行脚本（默认为a.out）。

测试目录包含许多我们用来建立对语义正确性的信心的测试。要运行基本测试集，请从顶层目录运行make check。出于性能原因，您可能首先希望在后台运行kserver，并传递-j标志以获取所需的并行度。

默认情况下，KCC对C库的支持相对有限。如果您正在编译和链接使用许多库函数的程序，则可能会遇到CV-CID1和UB-TDR2错误，分别表示您所调用的函数未在相应的头文件中声明或已声明，但是目前语义中尚无定义。

如果您希望执行此类程序，请与Runtime Verification，Inc联系，该公司基于此语义许可RV-Match许可，该RV-Match能够通过链接系统上为这些库提供的现有代码来执行此类程序。有关更多信息，请联系https://runtimeverification.com/support。

x86-gcc-limited-libc：库标头和一些未在语义本身中直接定义的函数的库源。

dist：在构建过程中创建的，这是最终产品的来源。为了方便起见，请考虑将此目录添加到$ PATH中。

在构建过程中，使用带有不同标志的kompile构建了三个语义版本：a＆＃34; deterministic＆＃34;。版本，用于支持非确定性表达式排序的版本，以及另一个具有非确定性线程交织的版本。所有这些都将与x86-gcc-limited-libc / include和scripts / kcc脚本的内容一起复制到dist /中。最后，在x86-gcc-limited-libc / src中的所有libc源文件上共享makeruns kcc -s-。

kcc脚本是我们语义的主要接口。调用kcc myprogram.c会导致连续地通过管道传递参数C源文件的内容：

此AST的根是单个TranslationUnit术语，然后由我们的＆＃34; translation＆＃34;解释。语义。