diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 66ef00665..85e343027 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -4901,8 +4901,40 @@ package body Tree_Walk is -- be called from Ada, or a foreign-language variable to be -- accessed from Ada. This would (probably) require gnat2goto to -- understand the foreign code, which we do not at the moment. - Put_Line (Standard_Error, - "Warning: Multi-language analysis unsupported."); + -- However, if the calling convention is specified as "Intrinsic" + -- then the subprogram is built into the compiler and gnat2goto + -- can safely ignore the pragma. + declare + -- If the pragma is specified with positional parameter + -- association, then the calling convention is the first + -- parameter. Check to see if it is Intrinsic. + Next_Ass : Node_Id := First (Pragma_Argument_Associations (N)); + Is_Intrinsic : Boolean := Present (Next_Ass) and then + Nkind (Expression (Next_Ass)) = N_Identifier and then + Get_Name_String (Chars (Expression (Next_Ass))) = "intrinsic"; + begin + -- If the first parameter is not Intrinsic, check named + -- parameters for calling convention + while not Is_Intrinsic and Present (Next_Ass) loop + if Chars (Next_Ass) /= No_Name and then + Get_Name_String (Chars (Next_Ass)) = "convention" + then + -- The named parameter is Convention, check to see if it + -- is Intrinsic + Is_Intrinsic := + Get_Name_String (Chars (Expression (Next_Ass))) = + "intrinsic"; + end if; + -- Get the next parameter association + Next_Ass := Next (Next_Ass); + end loop; + + if not Is_Intrinsic then + Put_Line (Standard_Error, + "Warning: Multi-language analysis unsupported."); + end if; + end; + when Name_Elaborate => -- Specifies that the body of the named library unit is elaborated -- before the current library_item. We will support packages. diff --git a/testsuite/gnat2goto/tests/intrinsic/test.out b/testsuite/gnat2goto/tests/intrinsic/test.out new file mode 100644 index 000000000..19c69e408 --- /dev/null +++ b/testsuite/gnat2goto/tests/intrinsic/test.out @@ -0,0 +1,6 @@ +Standard_Error from gnat2goto use_import: +Warning: Multi-language analysis unsupported. +Warning: Multi-language analysis unsupported. + +[overflow.1] file use_import.adb line 16 arithmetic overflow on signed unary minus in -use_import__i: SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/intrinsic/test.py b/testsuite/gnat2goto/tests/intrinsic/test.py new file mode 100644 index 000000000..9f3fe4da7 --- /dev/null +++ b/testsuite/gnat2goto/tests/intrinsic/test.py @@ -0,0 +1,4 @@ +from test_support import * + +prove("--signed-overflow-check") + diff --git a/testsuite/gnat2goto/tests/intrinsic/use_import.adb b/testsuite/gnat2goto/tests/intrinsic/use_import.adb new file mode 100644 index 000000000..4d693f585 --- /dev/null +++ b/testsuite/gnat2goto/tests/intrinsic/use_import.adb @@ -0,0 +1,17 @@ +procedure Use_Import is + procedure P (X : Integer); + pragma Import (C, P); + + procedure Q (X : Integer); + pragma Import (Convention => C, Entity => Q); + + function "-" (X : Integer) return Integer; + pragma Import (Convention => Intrinsic, Entity => "-"); + + function "+" (Left, Right : Integer) return Integer; + pragma Import (Intrinsic, "+"); + + I : Integer := 1; +begin + I := -I; +end Use_Import;