「‍」 Lingenic

lingenic_text_c

(⤓.gpr ◇.gpr); γ ≜ [2026-07-12T135544.190, 2026-07-12T135544.190] ∧ |γ| = 1

--  Copyright © 2026 Lingenic LLC. All rights reserved.
--  Licensed under the Lingenic Source-Available License v2.3.
--  Production use requires a separate license from Licensor.
--  See LICENSE.md and COPYRIGHT in the project root.
--

-------------------------------------------------------------------------------
--  Lingenic-Text
--  Formally Verified Unicode Text Processing Library
--
--  C library project: builds the proved SPARK core plus the C binding
--  (src-c/lingenic_text_c.ads/.adb) as a standalone static library.
--
--  Usage from C:
--    1. call lingenic_text_cinit()  (elaboration, generated by gprbuild)
--    2. call lt_init("<ucd dir>")
--    3. use the lt_* API (see include/lingenic_text.h)
--
--  Build:
--    gprbuild -P lingenic_text_c.gpr -j0
--
--  Output:
--    lib-c/liblingenic_text_c.a
-------------------------------------------------------------------------------

library project Lingenic_Text_C is

   for Source_Dirs use ("src", "src-c");
   for Object_Dir use "obj-c";
   for Library_Name use "lingenic_text_c";
   for Library_Dir use "lib-c";
   for Library_Kind use "static";

   --  Standalone: gprbuild generates lingenic_text_cinit(), which runs
   --  Ada elaboration for the whole closure.  C callers must invoke it
   --  once before any lt_* function.
   for Library_Standalone use "standard";
   for Library_Interface use ("Lingenic_Text_C");

   Core_Switches :=
      ("-gnat2022",       --  Ada 2022 standard
       "-gnatwa",         --  All warnings
       "-gnatwe",         --  Warnings as errors
       "-gnatVa",         --  All validity checks
       "-gnato13",        --  Overflow checks (eliminate, strict)
       "-O2");            --  Optimization

   package Compiler is
      --  Proved core: checks suppressed (absence of runtime errors is
      --  proved by gnatprove).
      for Default_Switches ("Ada") use Core_Switches & ("-gnatp");

      --  C binding shim: NOT proved (SPARK_Mode Off), compiled with full
      --  runtime checks as defense in depth.  Exceptions are caught at the
      --  API boundary and reported as LT_ERR.
      for Switches ("lingenic_text_c.adb") use Core_Switches;
   end Compiler;

   package Builder is
      for Global_Configuration_Pragmas use "build.adc";
      for Default_Switches ("Ada") use ("-j0");
   end Builder;

end Lingenic_Text_C;