Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion testsuite/gnat2goto/lib/python/test_support.py
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,13 @@ def filter_timing(results):

return re.sub(skip, r'', results)

def filter_gnat2goto_errout(errout_text):
lines = errout_text.splitlines()
result = ""
for line in lines:
if not line.startswith("Warning"):
result += line
return result

def process(debug, file, cbmcargs):
"""Process Ada file with gnat2goto and cbmc"""
Expand All @@ -54,7 +61,7 @@ def process(debug, file, cbmcargs):
if stdout_text != '':
print "Standard_Output from gnat2goto " + unit + ":"
print stdout_text
if errout_text != '':
if filter_gnat2goto_errout(errout_text) != '':
print "Standard_Error from gnat2goto " + unit + ":"
print errout_text
if g2go_results.status != 0:
Expand Down
6 changes: 6 additions & 0 deletions testsuite/gnat2goto/tests/pragma_export/base.adb
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
package body Base is
function Inc (Var : Integer) return Integer is
begin
return Var + 1;
end Inc;
end Base;
7 changes: 7 additions & 0 deletions testsuite/gnat2goto/tests/pragma_export/base.ads
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Base is
function Inc (Var : Integer) return Integer;
pragma Export
(Convention => C,
Entity => Inc,
External_Name => "Base_Inc" );
end Base;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/pragma_export/test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
VERIFICATION SUCCESSFUL
3 changes: 3 additions & 0 deletions testsuite/gnat2goto/tests/pragma_export/test.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
from test_support import *

prove()