C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources; dynamic properties of objects and the way they evolve during program execution. The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO~C code. The annotated C program parts can be validated by static analysis: if the static analyzer flags no error, then the annotations are provably coherent among themselves and with respect to annotated C code, in which case said annotated parts are provably exempt from a large class of logic, security, and run-time errors.
翻译:Crused是一个创新技术,C程序可以(部分)附加说明,以表达:语言、系统和用户界定的资源的所有权、排他性和可分享性;物体的动态特性及其在程序执行期间的演变方式。(部分)附加说明的C程序可以用任何能够处理ISO~C代码的编译工具链的未经修改的版本翻译。附加说明的C程序部分可以通过静态分析加以验证:如果静态分析师没有错误,则说明在它们之间和在附加说明的C代码方面可以明显保持一致,在这种情况下,附加说明的部分可以免于大量的逻辑、安全和运行时错误。