TrustInsoft
  • Product
  • Industries
  • Client testimonials
  • About Us
  • Blog
  • Press Kit
  • Contact Us
  • Try Online

About the Blog

Lorem ipsum dolor sit amet, consectetur elit porta. Vestibulum ante justo, volutpat quis porta non, vulputate id diam. Lorem et ipsum dolor sit amet, consectetur adipiscing elit. Morbi vitae sem in massa sagittis.
Follow Us!Get the latest news
Fresh newsfollow us

Categories

  • Archives
  • Events
  • Press
  • Product
  • Technical Article
  • Video

Tags

demo TrustInSoft Analyzer video

Meet TrustInSoft at Frama-C & SPARK Day 2019

Posted On May 27, 2019 By Pauline Schellenberger In Events /  

TrustInSoft is honored to take part in the Frama-C and SPARK day, co-organized with Adacore, CEA List and Inria. The event takes place in Paris on June 3rd as part of  Open Source Innovation Spring initiated by the thematic group `Logiciel libre’ of the cluster Systematic-Paris-Region and IRILL (`Initiative de Recherche et Innovation sur le Logiciel Libre’).

This one-day workshop is dedicated to researchers and engineers of the environment of Frama-C and SPARK tools, implemented in academic and industrial fields. One ambition, sharing and discussing research, project results, knowledge and experiences.

During the day our CTO, Benjamin Monate, will give a talk with EasyMile, the pioneer in driverless technology and smart mobility solutions.
The fast-growing start-up develops software revolutionizing passenger and goods transportation. They will together share feedbacks on the application of formal methods on EasyMile’s source code.

​In addition, keynote and talks will be given around the application of formal verification in the autonomous driving industry, to embedded software, and for safety.
Find out more about the day’s line up here: https://www.open-source-innovation-spring.org/2019/frama-c-and-spark-day-2019/.

Want to debrief or interact? Stop by the TrustInSoft booth to share a discussion with us!

To join, freely register here: https://bit.ly/2DA7TXu.​

Looking forward to seeing you there!

Frama-C & SPARK Day
Monday, June 3rd 2019
La Fabrique Événementielle
52 ter Rue des Vinaigriers, 75010 Paris 

Printing a null pointer with %s is undefined behavior
Upgrade your existing test suites with TrustInSoft

Pauline Schellenberger

All articles by: Pauline Schellenberger

All rights reserved. © TrustInSoft 2019.Twitter IconLinkedIn Icon

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

By continuing to use the site, you consent to the use of cookies. They allow us to gather anonymous browsing data that are indispensable to understand how our website is used and continuously improve your experience.I agreePrivacy policy