• Gem #80: Speedy Shift and Rotate in SPARK

    Ada Gem #80 — This Gem covers a topic that I recently encountered while working on a crypto algorithm in SPARK: how to use Ada's predefined shift and rotate functions with modular types from a SPARK program. Continue Reading »

    Rod Chapman
    Altran
  • Gem #79: Where did my memory go? (Part 3)

    Ada Gem #79 — A number of tools and libraries exist to monitor memory usage, detect memory leaks and more generally solve issues with memory management. The Gems in this three-part series offer an overview of these issues and explain how you can benefit from these tools in your own development. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #78: Where did my memory go? (Part 2)

    Ada Gem #78 — A number of tools and libraries exist to monitor memory usage, detect memory leaks and more generally solve issues with memory management. The Gems in this three-part series offer an overview of these issues and explain how you can benefit from these tools in your own development. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #77: Where did my memory go? (Part 1)

    Ada Gem #77 — A number of tools and libraries exist to monitor memory usage, detect memory leaks, and more generally solve issues with memory management. This Gem, and others to follow, offer an overview of these issues and explain how you can benefit from these tools in your own development. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #76: Tokeneer Discovery - Lesson 6

    Ada Gem #76 — In the previous Gem in this series, we saw how to deal with overflow errors, based on source code from Tokeneer. In this Gem, we show how to ensure secure information flow.
    This Gem brings us to the end of this series on Tokeneer, and we would like to say a big thank you to the SPARK team at Altran for providing these resources.
    We will now take a break for the holiday period and will return with more Gems on January 11, 2010. Very happy holidays to all Gem readers, wherever you are!
    Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #75: Tokeneer Discovery - Lesson 5

    Ada Gem #75 — In the previous Gem in this series, we saw how the SPARK Toolset can verify application-specific safety and security properties, based on source code from Tokeneer. In this Gem, we show how to deal with overflow errors. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #74: Tokeneer Discovery - Lesson 4

    Ada Gem #74 — In the previous Gem in this series, we saw how to validate input in SPARK, based on source code from Tokeneer. In this Gem, we show how the SPARK Toolset can verify application-specific safety and security properties. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #73: Tokeneer Discovery - Lesson 3

    Ada Gem #73 — In the previous Gem in this series, we saw how to identify ineffective statements in SPARK, based on source code from Tokeneer. In this Gem, we show how to validate input. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #72: Tokeneer Discovery - Lesson 2

    Ada Gem #72 — In the previous Gem in this series we saw how to deal with improper initialization in SPARK, based on source code from Tokeneer. In this Gem, we show how to identify ineffective statements. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #71: Tokeneer Discovery - Lesson 1

    Ada Gem #71 — In previous Gems, we saw how to create a SPARK project in GPS, and how to run the Examiner and Simplifier tools to verify various properties of a simple linear search function. In this series of Gems on SPARK, we will explore SPARK capabilities in greater depth, using source code from Tokeneer, an NSA-funded, highly secure biometric software system.
    In this Gem, we show how to deal with improper initialization. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #70: The Scope Locks Idiom

    Ada Gem #70 — This Gem marks a brief break from SPARK, which will return in two weeks with the first in a series of six Gems on that topic.
    Encapsulating shared variables inside protected operations is not always possible. This Gem shows how to add mutual exclusion to existing sequential code using a combination of controlled and protected types, such that the resulting code is robust and minimally changed. Continue Reading »

    Pat Rogers
    AdaCore
  • Gem #69: Let's SPARK! - Part 2

    Ada Gem #69 — Welcome back! We hope you had a great summer. Now let's get back to where we left off.
    In this Gem and the previous one, we give you a simple walkthrough of SPARK's capabilities and its integration with GPS. In the previous Gem, we showed how to set up a SPARK project and prove that your SPARK programs are free from uninitialized variable accesses and that they execute without run-time errors. In this Gem, we show how to prove that your SPARK programs respect given contracts. Continue Reading »

    Yannick Moy
    AdaCore
  • Gem #68: Let's SPARK! - Part 1

    Ada Gem #68 — Please note that this is the final Gem before we break for summer. The series will resume on September 7, 2009.

    In this Gem and the next one, we present a simple walk-through of SPARK's capabilities and its integration with GPS. In this first Gem, we show how to set up a SPARK project and prove that your SPARK programs are free from uninitialized variable accesses and that they execute without run-time errors.

    Continue Reading »

    Yannick Moy
    AdaCore
  • Gem #67: Managing the GPS Workspace

    Ada Gem #67 — GPS has a multitude of views and editors, several of which may be displayed on the screen at the same time. It is based on a very flexible desktop that helps you organize these windows the way you prefer. This Gem describes some of the lesser-known aspects of the GPS desktop. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #66: GPS's Key Shortcuts Editor

    Ada Gem #66 — Most GPS features are accessible through menus and contextual menus. However, for maximum efficiency most users prefer to use keyboard shortcuts. Although GPS comes with a number of predefined shortcuts, you might want to adapt them to your own habits, especially if you are moving from a previous editor. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #65: gprbuild

    Ada Gem #65 — gprbuild is a new program builder, superseding gnatmake. It supports multiple languages, automatically manages source dependencies, and reduces the need for recompilation. This Gem describes a high-level view of how gprbuild works. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #64: Handling Multiple-Unit Source Files

    Ada Gem #64 — This Gem describes how to compile applications in GNAT when source files contain multiple units. The preferred approach is to split source files, and here we describes how this can be done, although GNAT also provides a workaround that allows you to keep your existing files. Continue Reading »

    Emmanuel Briot
    AdaCore
  • Gem #63: The Effect of Pragma Suppress

    Ada Gem #63 — The features of Ada have generally been designed to prevent violating the properties of data types, enforced either by compile-time rules or, in the case of dynamic properties, by using run-time checks. Ada allows run-time checks to be suppressed, but not with the intent of allowing programmers to subvert the type system. Continue Reading »

    Gary Dismukes
    AdaCore
  • Gem #62: C++ constructors and Ada 2005

    Ada Gem #62 — In the previous Gem, we explored how to interface and make simple use of C++ constructors on the Ada side.

    In this Gem, we detail more advanced constructs related to Ada 2005 and C++ constructors.

    Continue Reading »

    Javier Miranda, Arnaud Charlet
  • Gem #61: Interfacing with C++ constructors

    Ada Gem #61 — In the previous Gem about generating bindings from C++ headers, we mentioned, without going into details, how to interface with C++ constructors in Ada using the CPP_Constructor pragma.

    In this Gem we present some common uses of C++ constructors in mixed-language programs in GNAT, and in the next Gem, we will show the use of some powerful Ada 2005 features in conjunction with C++ constructors.

    Continue Reading »

    Javier Miranda, Arnaud Charlet
« Previous    3  4  5  6  7     Next »