Menu
Guarantee the absence of undefined behaviours in C programs
Despite valid alternatives, the C programming language is still largely used in industry and taught to students.
The C language is unsafe, meaning that the execution of erroneous operations causes the program’s behavior to be unpredictable. The ISO C standard tells that erroneous operations have undefined behavior.
Undefined behavior is a serious matter. Most C programmers know that accessing an out-of-bounds array element is an erroneous operation. Few of them understand that the related undefined behavior is a security flaw that could lead, for example, to a stack smashing attack.
Understanding undefined behaviors is so tricky that it is pretty much impossible to avoid them when writing nontrivial C programs. Programmers should then use verification tools ensuring that their code is correct.
Today TrustInSoft unveils TSnippet, the easiest way to guarantee the absence of undefined behaviors in C programs.
TSnippet is a free, cloud-powered, advanced static source code analyzer, built on top of TrustInSoft Kernel, that guarantees the absence of subtle bugs, notably those related with undefined behaviors, in single-file snippets of C source code.
Users are not required to be experienced in software verification. A minimalist user interface allows TSnippet to provide a lightweight and intuitive C code analysis workflow: Users just need to type in their program and click on a button to know whether their code is correct.
This is what TSnippet looks like:
TSnippet is an advanced, static source code analysis tool that guarantees the absence of undefined behaviors in single-file snippets of C source code.
The user can type in, or paste, a self-contained C code snippet, and then check for undefined behavior by clicking on the Analyze button.
TSnippet warns the user whenever the code has an undefined behavior. The Overview tab (bottom left) reports a synopsis about the analysis’ status, while the Analyzer View (right panel) shows precisely which assertion was expected to hold and has been violated. All the code that follows the violation is highlighted in red, as the analysis will not reach it as it stops upon encountering the problem.
TSnippet provides several advanced debugging features useful to understand the detected undefined behavior. The user may look at the TrustInSoft documentation concerning the failed assertion by clicking on the Help button, inspect the values of program variables (bottom right) by clicking on Inspect buttons, see which statements have influenced the variable values in the Show Defs Statements tab (bottom left), and much more.
The user can then modify the code snippet, and run the analysis once again.
The user may iterate the edit-analyze-check result process as many times as needed till all the problems in the program are fixed, and TSnippet finally declares it correct.Try this example online
On the left, the Source Code Editor panel allows users to directly type in a C code snippet. Then, an analysis is triggered either by a click on the toolbar button Analyze or automatically after choosing a target architecture. Finally, the outcome of the analysis is shown in the bottom-left Overview area.
The Overview displays a verdict on the users’ program. The verdict is positive if TSnippet has determined the program correct. This means that the provided code is mathematically guaranteed to be free of runtime errors, i.e. it has no undefined behavior. Otherwise, the verdict is negative, and TSnippet warns the user that it has found a flaw in the code snippet.
The precise violation is reported as a failed assertion in the right panel Analyzer View. The latter shows an interactive version of the original code, and provides the majority of TrustInSoft Analyzer’s advanced debugging features which help the user to understand the root causes of the detected flaw. In particular, users can investigate variables in multiple ways:
• Inspect the possible runtime values of variables, at any point in the program,
• Track variables to check how their values evolve all along the program,
• View the values of variables per callstack, to check what values are taken by variables for specific chains of function calls,
• Inspect which statements might have influenced the values of particular variables.
The user may then iterate the edit-analyze-check result process as many times as needed till all the problems in the program are fixed, and TSnippet finally declares it correct.
Simply put, TSnippet provides a step-by-step interactive workflow towards correct C code snippets, backed by a source code analyzer that will not miss anything. This is especially valuable for engineers needing to check for undefined behaviors since the early stages of software prototyping, or for teachers showing their students what it really means to program correctly in C.
Mostly nobody knows about all the C language quirks, especially for what concerns undefined behaviors.
TSnippet is useful in this regard too, as a tool for teaching and spreading knowledge about correct C programming. Indeed, the tool supports a sharing service which allows sharing C code snippets, together with their respective analysis outcomes.
At any moment, users can choose to share their C code analysis with a click on the toolbar button Share. TSnippet will provide a URL that, when visited, will reproduce the original analysis session.
TSnippet is a free, cloud-powered, advanced static source code analyzer for single-file C code snippets. Users can directly type in some C code, and immediately get warned if it exhibits an undefined behavior. Users may also share their code snippets and respective analysis sessions.
(TSnippet is powered by TrustInSoft Kernel, available at https://github.com/TrustInSoft/tis-kernel as Open Source Software. At the moment, TSnippet allows single-file code snippets only. For more comprehensive analyses, on actual C code bases, please take a look at the TrustInSoft tools designed for such tasks at https://taas.trust-in-soft.com)
