• 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
  • Gem #60: Generating Ada bindings for C++ headers

    Ada Gem #60 — In Gem #59 we saw how simple it is to automatically generate Ada bindings for C header files. In this Gem, we will see that, similarly, it's now also possible to generate Ada bindings for C++ header files. Continue Reading »

    Arnaud Charlet
    AdaCore
  • Gem #59: Generating Ada bindings for C headers

    Ada Gem #59 — One of the delicate areas of Ada that is often unfamiliar to developers is how to intermix Ada code with other programming languages. While Ada provides very powerful and complete capabilities to interface with other compiled languages such as C, C++, and Fortran, writing the Ada glue code that enables a programmer to use complex and large APIs can be tedious and error-prone.
    In this Gem, we will explore a new tool provided by AdaCore to automate the interface generation of C header files through the compiler. Continue Reading »

    Arnaud Charlet
    AdaCore
  • Gem #58: Ada / Java exception handling

    Ada Gem #58 — Ada and Java are two languages that rely heavily on exceptions. A large part of the Ada data model is based on the fact that data is checked at run time, and will raise various kinds of exceptions such as Constraint_Error when constraints are violated. Similarly, there are many cases where Java performs checks that can raise exceptions, among the most common being checks on casts and null dereferences. It is therefore extremely important to support exceptions that are properly propagated from one language to the other and even potentially caught/handled, without having to worry about the language of origin. Continue Reading »

    Quentin Ochem
    AdaCore
« Previous    3  4  5  6  7     Next »