Skip to content

Commit f8b4bdd

Browse files
committed
Only add bodies to system functions
by checking the name-prefix.
1 parent f62fe16 commit f8b4bdd

File tree

3 files changed

+16
-1
lines changed

3 files changed

+16
-1
lines changed

gnat2goto/driver/goto_utils.adb

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,18 @@ package body GOTO_Utils is
3030
return R;
3131
end Make_Address_Of;
3232

33+
function Is_Prefix (Prefix : String; Base_String : String) return Boolean
34+
is
35+
begin
36+
if Prefix'Length < Base_String'Length and then
37+
Prefix = Base_String (Base_String'First .. Prefix'Length)
38+
then
39+
return True;
40+
else
41+
return False;
42+
end if;
43+
end Is_Prefix;
44+
3345
-------------------
3446
-- Make_Int_Type --
3547
-------------------

gnat2goto/driver/goto_utils.ads

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ package GOTO_Utils is
2222

2323
type String_Access is access String;
2424

25+
function Is_Prefix (Prefix : String; Base_String : String) return Boolean;
26+
2527
package Addressed_Variables is new
2628
GNAT.Table (Table_Component_Type => String_Access,
2729
Table_Index_Type => Natural,

gnat2goto/driver/tree_walk.adb

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5460,7 +5460,8 @@ package body Tree_Walk is
54605460
Default_Body : Irep := Make_Nil (Sloc (N));
54615461
begin
54625462
if List_Length (Parameter_Specifications (N)) = 1 and
5463-
not (Kind (Get_Return_Type (Subprog_Type)) = I_Void_Type)
5463+
not (Kind (Get_Return_Type (Subprog_Type)) = I_Void_Type) and
5464+
Is_Prefix ("system", Unique_Name (Defining_Unit_Name (N)))
54645465
then
54655466
Default_Body := Build_Identity_Body (Get_Parameters (Subprog_Type));
54665467
end if;

0 commit comments

Comments
 (0)