Skip to content
This repository has been archived by the owner on Aug 12, 2024. It is now read-only.

Commit

Permalink
Fix coverage
Browse files Browse the repository at this point in the history
ref #24
  • Loading branch information
jklmnn committed Dec 7, 2021
1 parent 22f12ef commit d1e7287
Show file tree
Hide file tree
Showing 5 changed files with 25 additions and 34 deletions.
4 changes: 2 additions & 2 deletions tests/tests.gpr
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,12 @@ project Tests is
for Exec_Dir use "../obj/tests";

package Compiler is
for Default_Switches ("Ada") use Z3_Switches.Compiler_Switches;
for Default_Switches ("Ada") use Z3_Switches.Compiler_Switches & ("--coverage");
end Compiler;

package Builder is
for Default_Switches ("Ada") use ("-O0", "-g", "-gnata");
for Global_Compilation_Switches ("Ada") use ("-O0", "-g", "--coverage", "-fsanitize=address", "-fno-omit-frame-pointer");
for Global_Compilation_Switches ("Ada") use ("-O0", "-g", "-fsanitize=address", "-fno-omit-frame-pointer");
end Builder;

package Linker is
Expand Down
2 changes: 1 addition & 1 deletion tests/z3-tests.adb
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
with AUnit.Assertions;

package body Z3.Tests is
package body Z3.Tests is -- GCOV_EXCL_LINE

use AUnit.Assertions;

Expand Down
29 changes: 9 additions & 20 deletions z3.adb
Original file line number Diff line number Diff line change
Expand Up @@ -457,17 +457,6 @@ is

------------------------------------------------------------------------------------------------

overriding
procedure Initialize (Solv : in out Solver)
is
use type z3_api_h.Z3_solver;
begin
if Solv.Data /= null then
z3_api_h.Z3_solver_inc_ref (c => Solv.Context.Data,
s => Solv.Data);
end if;
end Initialize;

overriding
procedure Adjust (Solv : in out Solver)
is
Expand All @@ -476,6 +465,8 @@ is
s => Solv.Data);
end Adjust;

------------------------------------------------------------------------------------------------

overriding
procedure Finalize (Solv : in out Solver)
is
Expand All @@ -484,6 +475,8 @@ is
s => Solv.Data);
end Finalize;

------------------------------------------------------------------------------------------------

function Create (Context : Z3.Context'Class) return Solver
is
Solver : constant Z3.Solver :=
Expand Down Expand Up @@ -733,15 +726,7 @@ is
Backtracking_Count => 0);
end Create;

overriding
procedure Initialize (Opt : in out Optimize)
is
use type z3_api_h.Z3_optimize;
begin
if Opt.Data /= null then
z3_optimization_h.Z3_optimize_inc_ref (Opt.Context.Data, Opt.Data);
end if;
end Initialize;
------------------------------------------------------------------------------------------------

overriding
procedure Adjust (Opt : in out Optimize)
Expand All @@ -750,13 +735,17 @@ is
z3_optimization_h.Z3_optimize_inc_ref (Opt.Context.Data, Opt.Data);
end Adjust;

------------------------------------------------------------------------------------------------

overriding
procedure Finalize (Opt : in out Optimize)
is
begin
z3_optimization_h.Z3_optimize_inc_ref (Opt.Context.Data, Opt.Data);
end Finalize;

------------------------------------------------------------------------------------------------

function "+" (Optimize : Z3.Optimize) return String
is
begin
Expand Down
10 changes: 2 additions & 8 deletions z3.ads
Original file line number Diff line number Diff line change
Expand Up @@ -150,9 +150,9 @@ package Z3 is -- GCOV_EXCL_LINE
type Int_Array is array (Natural range <>) of Int_Type;

function Int (Name : String; Context : Z3.Context'Class) return Int_Type;
function Int (Value : Long_Long_Integer;
function Int (Value : Long_Long_Integer; -- GCOV_EXCL_LINE
Context : Z3.Context'Class) return Int_Type;
function Int (Value : Long_Long_Unsigned;
function Int (Value : Long_Long_Unsigned; -- GCOV_EXCL_LINE
Context : Z3.Context'Class) return Int_Type;
function Int (Expr : Expr_Type'Class) return Int_Type with
Pre => Sort (Expr) in Sort_Int | Sort_Real;
Expand Down Expand Up @@ -472,9 +472,6 @@ private
Data : z3_api_h.Z3_solver;
end record;

overriding
procedure Initialize (Solv : in out Solver);

overriding
procedure Finalize (Solv : in out Solver);

Expand Down Expand Up @@ -536,9 +533,6 @@ private
Backtracking_Count : Natural;
end record;

overriding
procedure Initialize (Opt : in out Optimize);

overriding
procedure Adjust (Opt : in out Optimize);

Expand Down
14 changes: 11 additions & 3 deletions z3.gpr
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,20 @@ with "z3/libz3";

project Z3 is

type Build_Type is ("production", "development");
Build : Build_Type := external ("AZ3_BUILD", "development");

for Create_Missing_Dirs use "True";
for Source_Dirs use (".");
for Object_Dir use "obj";

package Builder is
for Default_Switches ("Ada") use Z3_Switches.Compiler_Switches;
end Builder;
package Compiler is
case Build is
when "development" =>
for Default_Switches ("Ada") use Z3_Switches.Compiler_Switches & ("-g", "-O0", "--coverage");
when others =>
for Default_Switches ("Ada") use Z3_Switches.Compiler_Switches;
end case;
end Compiler;

end Z3;

0 comments on commit d1e7287

Please sign in to comment.