00_run.txt

[14:42:43] tyler:fosdem-ada $ ./precondition 
burp
PING!
done

fosdem.adb

with Ada.Text_IO;

package body Fosdem is
   function Is_Valid return Boolean is
   begin
      return False;
   end Is_Valid;

   procedure Ping is
   begin
      Ada.Text_IO.Put_Line ("PING!");
   end Ping;

end Fosdem;

fosdem.ads

package Fosdem is
   function Is_Valid return Boolean;

   procedure Ping
      with Pre => (Is_Valid  = True);

end Fosdem;

fosdem.gpr

project Fosdem is
    for Source_Dirs use (".");
    for Object_Dir use "obj";
    for Main use ("precondition.adb");

    package Compiler is
      for Switches ("Ada") use ("-g", "-gnata", "-gnat2012");
    end Compiler;
end Fosdem;

precondition.adb

with Ada.Text_IO;
with Fosdem;

procedure Precondition is
   use Ada.Text_IO;
begin
   Put_Line ("burp");
   Fosdem.Ping;
   Put_Line("done");
end Precondition;

You should include the "-fstack-check" and "-gnato" flags for the compiler to get proper Ada behaviour out of GNAT.

With GNATMAKE GPL 2013 (20130314) your example works as expected.