coap_spark.gpr

-- SPARKLib will be installed by Alire when installing the
-- gnatprove dependency.
with "sparklib.gpr";

with "config/coap_spark_config.gpr";

project Coap_Spark is

   for Library_Name use "Coap_Spark";
   for Library_Version use Project'Library_Name & ".so." & Coap_Spark_Config.Crate_Version;

   for Source_Dirs use ("src/", "config/", "generated/");
   for Object_Dir use "obj/" & Coap_Spark_Config.Build_Profile;
   for Create_Missing_Dirs use "True";
   for Library_Dir use "lib";

   type Library_Type_Type is ("relocatable", "static", "static-pic");
   Library_Type : Library_Type_Type :=
     external ("COAP_SPARK_LIBRARY_TYPE", external ("LIBRARY_TYPE", "static"));
   for Library_Kind use Library_Type;

   package Compiler is
      for Default_Switches ("Ada") use Coap_Spark_Config.Ada_Compiler_Switches;
   end Compiler;

   package Binder is
      for Switches ("Ada") use ("-Es"); --  Symbolic traceback
   end Binder;

   package Install is
      for Artifacts (".") use ("share");
   end Install;

   package Prove is

      for Proof_Dir use "proof";

      for Proof_Switches ("Ada") use (
         "-j0",
         "--mode=silver",
         "--prover=z3,cvc5,altergo,colibri",
         "--steps=0",
         "--timeout=360",
         "--memlimit=4000",
         "--checks-as-errors=on",
         "--warnings=error",
         "--counterexamples=on"
      );

   end Prove;

end Coap_Spark;