Skip to content

Testsuite/arrays #83

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jan 28, 2019
Merged

Testsuite/arrays #83

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7aac448
Introduce malloc building function
Jan 18, 2019
e9f1851
Add lhs to function call
Jan 18, 2019
930cd1a
Rewrite get_array_copy_function
Jan 18, 2019
bbb6646
Rewrite get_array_dup_function
Jan 18, 2019
e98f7c7
Add precondition where appropriate
Jan 18, 2019
9437f0d
Add malloc and size_t symbols
Jan 18, 2019
5241db6
Add failing test
Jan 24, 2019
007a82c
Add succeeding test
Jan 28, 2019
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
46 changes: 46 additions & 0 deletions gnat2goto/driver/driver.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,42 @@ package body Driver is
procedure Follow_Type_Declarations (Old_Table : Symbol_Table;
New_Table : in out Symbol_Table);

procedure Add_Malloc_Symbol;

procedure Add_Malloc_Symbol is
Malloc_Name : constant String := "malloc";
Malloc_Params : constant Irep := New_Irep (I_Parameter_List);
Size_Param : constant Irep :=
Create_Fun_Parameter (Fun_Name => Malloc_Name,
Param_Name => "size",
Param_Type =>
Make_Symbol_Type (Identifier => "__CPROVER_size_t"),
Param_List => Malloc_Params,
A_Symbol_Table => Global_Symbol_Table);
Malloc_Type : constant Irep :=
Make_Code_Type (Parameters => Malloc_Params,
Ellipsis => False,
Return_Type => Make_Pointer_Type (Make_Void_Type),
Inlined => False,
Knr => False);
Malloc_Symbol : Symbol;
begin
if Kind (Size_Param) = I_Code_Parameter then
Malloc_Symbol :=
New_Function_Symbol_Entry (Name => Malloc_Name,
Symbol_Type => Malloc_Type,
Value => Ireps.Empty,
A_Symbol_Table => Global_Symbol_Table);
pragma Assert (Kind (Malloc_Symbol.SymType) = I_Code_Type);
end if;
end Add_Malloc_Symbol;

procedure GNAT_To_Goto (GNAT_Root : Node_Id)
is
begin
Translate_Standard_Types;
Add_CProver_Internal_Symbols;
Add_Malloc_Symbol;
Translate_Compilation_Unit (GNAT_Root);
end GNAT_To_Goto;

Expand Down Expand Up @@ -398,6 +429,20 @@ package body Driver is
Global_Symbol_Table.Insert (Builtin.Name, Builtin);
end Add_Universal_Integer;

procedure Add_CProver_Size_T;
procedure Add_CProver_Size_T is
Builtin : Symbol;
Type_Irep : constant Irep := New_Irep (I_Unsignedbv_Type);
begin
Set_Width (Type_Irep, 64);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably shouldn't be a magic number, but for now we're probably alright in most circumstances. I can think of a few ways to make this more robust, but none of them are particularly nice. I'd just keep a reminder comment in here for now pointing out that this is an assumption, and moreover one that doesn't necessarily hold for target platforms...

Builtin.Name := Intern ("__CPROVER_size_t");
Builtin.PrettyName := Builtin.Name;
Builtin.BaseName := Builtin.Name;
Builtin.SymType := Type_Irep;
Builtin.IsType := True;

Global_Symbol_Table.Insert (Builtin.Name, Builtin);
end Add_CProver_Size_T;
begin
-- Add primitive types to the symtab
for Standard_Type in S_Types'Range loop
Expand Down Expand Up @@ -458,6 +503,7 @@ package body Driver is
end loop;
Add_Universal_Integer;
Add_Standard_String;
Add_CProver_Size_T;
end Translate_Standard_Types;

procedure Add_CProver_Internal_Symbols is
Expand Down
Loading