+ -- In GNATprove mode we must write the spec of a unit which
+ -- requires a body if that body is not found. This will
+ -- allow partial analysis on incomplete sources. Also, in
+ -- the case of a unit that is a remote call interface, the
+ -- bodies of packages may not exist but still may form a
+ -- valid program - so we handle that here as well.
+
+ if GNATprove_Mode
+ or else Is_Remote_Call_Interface (Cunit_Entity (Unum))
+ then
+ Body_Fname :=
+ Get_File_Name
+ (Uname => Get_Body_Name (Uname),
+ Subunit => False,
+ May_Fail => True);
+
+ Body_Index := Get_Unit_Index (Get_Body_Name (Uname));
+
+ if Body_Fname = No_File then
+ Body_Fname := Get_File_Name (Uname, Subunit => False);
+ Body_Index := Get_Unit_Index (Uname);
+ end if;
+
+ -- In the normal path we don't allow failure in fetching the
+ -- name of the desired body unit so that it may be properly
+ -- referenced in the output ali - even if it is missing.
+
+ else
+ Body_Fname :=
+ Get_File_Name
+ (Uname => Get_Body_Name (Uname),
+ Subunit => False,
+ May_Fail => False);
+
+ Body_Index := Get_Unit_Index (Get_Body_Name (Uname));
+ end if;