Range check via Cprover assert

gnat2goto/driver/goto_utils.adb

@@ -2,6 +2,8 @@ with Namet;   use Namet;
 with Nlists;  use Nlists;
 with Aspects; use Aspects;
 
+with Ada.Text_IO;           use Ada.Text_IO;
+
 package body GOTO_Utils is
 
    ---------------------
@@ -92,6 +94,100 @@ package body GOTO_Utils is
       return Ret;
    end Symbol_Expr;
 
+   --------------------------------
+   -- New_Parameter_Symbol_Entry --
+   --------------------------------
+
+   procedure New_Parameter_Symbol_Entry (Name_Id :               Symbol_Id;
+                                         BaseName :              String;
+                                         Symbol_Type :           Irep;
+                                         A_Symbol_Table : in out Symbol_Table)
+   is
+      New_Symbol : Symbol;
+   begin
+      New_Symbol.SymType := Symbol_Type;
+      New_Symbol.Name := Name_Id;
+      New_Symbol.PrettyName := Intern (BaseName);
+      New_Symbol.BaseName := Intern (BaseName);
+      New_Symbol.Mode := Intern ("C");
+
+      --  Setting it as a parameter
+      New_Symbol.IsParameter := True;
+      New_Symbol.IsLValue := True;
+      New_Symbol.IsFileLocal := True;
+      New_Symbol.IsThreadLocal := True;
+
+      if A_Symbol_Table.Contains (Key => Name_Id) then
+         Put_Line (Standard_Error,
+                   "----------At: New_Parameter_Symbol_Entry----------");
+         Put_Line (Standard_Error,
+                   "----------Trying to create known symbol.----------");
+         Put_Line (Standard_Error, "----------" & BaseName & "----------");
+      else
+         A_Symbol_Table.Insert (Name_Id, New_Symbol);
+      end if;
+   end New_Parameter_Symbol_Entry;
+
+   -------------------------------
+   -- New_Function_Symbol_Entry --
+   -------------------------------
+
+   function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
+                                       Value : Irep;
+                                       A_Symbol_Table : in out Symbol_Table)
+                                       return Symbol is
+      New_Symbol : Symbol;
+   begin
+      New_Symbol.SymType := Symbol_Type;
+      New_Symbol.Name := Intern (Name);
+      New_Symbol.PrettyName := New_Symbol.Name;
+      New_Symbol.BaseName := New_Symbol.Name;
+      New_Symbol.Mode := Intern ("C");
+      New_Symbol.Value := Value;
+
+      if A_Symbol_Table.Contains (Key => Intern (Name)) then
+         Put_Line (Standard_Error,
+                   "----------At: New_Function_Symbol_Entry----------");
+         Put_Line (Standard_Error,
+                   "----------Trying to create known symbol.----------");
+         Put_Line (Standard_Error, "----------" & Name & "----------");
+      else
+         A_Symbol_Table.Insert (Intern (Name), New_Symbol);
+      end if;
+      return New_Symbol;
+   end New_Function_Symbol_Entry;
+
+   --------------------------
+   -- Create_Fun_Parameter --
+   --------------------------
+
+   --  To be called when one needs to build a function inside gnat2goto
+   --  Modifies symbol table and Param_List as a side effect
+   --  Returns irep of type I_Code_Parameter
+   function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;
+                                  Param_Type : Irep; Param_List : Irep;
+                                  A_Symbol_Table : in out Symbol_Table;
+                                  Source_Location : Source_Ptr := No_Location)
+                                  return Irep is
+      Func_Param_Id : constant Symbol_Id := Intern (Fun_Name & Param_Name);
+      --  Create an irep for the parameter
+      Value_Arg : constant Irep :=
+        Make_Code_Parameter (Source_Location => Source_Location,
+                             Default_Value   => Ireps.Empty,
+                             I_Type          => Param_Type,
+                             Base_Name       => Param_Name,
+                             This            => False,
+                             Identifier      => Unintern (Func_Param_Id));
+   begin
+      --  Creates a symbol for the parameter
+      New_Parameter_Symbol_Entry (Name_Id        => Func_Param_Id,
+                                  BaseName       => Param_Name,
+                                  Symbol_Type    => Param_Type,
+                                  A_Symbol_Table => A_Symbol_Table);
+      Append_Parameter (Param_List, Value_Arg);
+      return Value_Arg;
+   end Create_Fun_Parameter;
+
    ---------------------
    -- Name_Has_Prefix --
    ---------------------

gnat2goto/driver/goto_utils.ads

@@ -29,6 +29,25 @@ package GOTO_Utils is
    function Symbol_Expr (Sym : Symbol) return Irep
    with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;
 
+   procedure New_Parameter_Symbol_Entry (Name_Id :               Symbol_Id;
+                                         BaseName :              String;
+                                         Symbol_Type :           Irep;
+                                         A_Symbol_Table : in out Symbol_Table);
+
+   function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
+                                       Value : Irep;
+                                       A_Symbol_Table : in out Symbol_Table)
+                                       return Symbol;
+
+   function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;
+                                  Param_Type : Irep; Param_List : Irep;
+                                  A_Symbol_Table : in out Symbol_Table;
+                                  Source_Location : Source_Ptr := No_Location)
+                                  return Irep
+     with Pre => (Kind (Param_Type) in Class_Type
+                  and then Kind (Param_List) = I_Parameter_List),
+     Post => Kind (Create_Fun_Parameter'Result) = I_Code_Parameter;
+
    function Name_Has_Prefix (N : Node_Id; Prefix : String) return Boolean;
 
    function Has_GNAT2goto_Annotation

gnat2goto/driver/range_check.adb

@@ -0,0 +1,30 @@
+with Binary_To_Hex;         use Binary_To_Hex;
+
+package body Range_Check is
+
+   -----------------
+   -- Store_Bound --
+   -----------------
+
+   function Store_Bound (Number : Bound_Type) return Integer
+   is
+      Length : constant Integer := Integer (Integer_Bounds_Table.Length);
+   begin
+      Integer_Bounds_Table.Append (Number);
+      return Length;
+   end Store_Bound;
+
+   -----------------------
+   -- Load_Bound_In_Hex --
+   -----------------------
+
+   function Load_Bound_In_Hex (Index : Integer; Bit_Width : Pos) return String
+   is
+      Bound : constant Uint := Uint (Integer_Bounds_Table.Element (Index));
+   begin
+      return Convert_Uint_To_Hex (
+                 Value     => Bound,
+                 Bit_Width => Bit_Width);
+   end Load_Bound_In_Hex;
+
+end Range_Check;

gnat2goto/driver/range_check.ads

@@ -0,0 +1,20 @@
+with Uintp;                  use Uintp;
+with Types;                  use Types;
+
+with Ada.Containers.Vectors; use Ada.Containers;
+package Range_Check is
+
+   type Bound_Type is new Uint;
+
+   package Integer_Bounds_Vector is new
+     Ada.Containers.Vectors (Index_Type   => Natural,
+                             Element_Type => Bound_Type);
+
+   function Store_Bound (Number : Bound_Type) return Integer;
+
+   Integer_Bounds_Table : Integer_Bounds_Vector.Vector;
+
+   function Load_Bound_In_Hex (Index : Integer; Bit_Width : Pos) return String
+     with Pre => Integer (Integer_Bounds_Table.Length) >= Index;
+
+end Range_Check;