Skip to content

Commit ef31ef0

Browse files
Petr BauchPetr Bauch
authored andcommitted
Add test-case for packages
Also includes cprover_start even when there is no function to call in a CU. Plus one more failing test (package function bodies are not processed).
1 parent 0e56882 commit ef31ef0

File tree

11 files changed

+50
-1
lines changed

11 files changed

+50
-1
lines changed

gnat2goto/driver/driver.adb

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -226,6 +226,17 @@ package body Driver is
226226
end;
227227

228228
if not Add_Start then
229+
Start_Symbol.Name := Start_Name;
230+
Start_Symbol.PrettyName := Start_Name;
231+
Start_Symbol.BaseName := Start_Name;
232+
233+
Set_Return_Type (Start_Type, Void_Type);
234+
235+
Start_Symbol.SymType := Start_Type;
236+
Start_Symbol.Value := Start_Body;
237+
Start_Symbol.Mode := Intern ("C");
238+
239+
Global_Symbol_Table.Insert (Start_Name, Start_Symbol);
229240
Put_Line (Sym_Tab_File,
230241
Create (SymbolTable2Json (Global_Symbol_Table)).Write);
231242
else

testsuite/gnat2goto/tests/long_integer/test_long_integer.adb

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
with Ada.Text_IO;
21
procedure Test_Long_Integer is
32
x: Long_Long_Integer := 1152921504606846976;
43
begin
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
with Test; use Test;
2+
3+
procedure Package_Type
4+
is
5+
Small_Number : Test.Range_10 := 4;
6+
begin
7+
pragma Assert (Small_Number * 2 = 8);
8+
end Package_Type;
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package Test
2+
is
3+
type Range_10 is new Positive;
4+
end Test;
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
VERIFICATION SUCCESSFUL
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
from test_support import *
2+
3+
prove()
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
with Test;
2+
3+
procedure Packages
4+
is
5+
begin
6+
pragma Assert (Test.Double (1) = 2);
7+
end Packages;
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package body Test
2+
is
3+
function Double(Input : Positive) return Positive
4+
is
5+
begin
6+
return Input + Input;
7+
end Double;
8+
end Test;
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package Test
2+
is
3+
function Double(Input : Positive) return Positive;
4+
end Test;
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
ALL XFAIL cbmc returns failed verification (calling function without body)

0 commit comments

Comments
 (0)