Skip to content

Commit

Permalink
Add workaround for GNATprove issue
Browse files Browse the repository at this point in the history
Related to #46
  • Loading branch information
treiher committed Jun 2, 2020
1 parent 9aa2432 commit 2915cbc
Show file tree
Hide file tree
Showing 12 changed files with 21 additions and 15 deletions.
2 changes: 1 addition & 1 deletion generated/rflx-arrays-generic_inner_message.ads
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-arrays-generic_message.ads
Original file line number Diff line number Diff line change
Expand Up @@ -587,7 +587,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-arrays-generic_messages_message.ads
Original file line number Diff line number Diff line change
Expand Up @@ -353,7 +353,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-enumeration-generic_message.ads
Original file line number Diff line number Diff line change
Expand Up @@ -280,7 +280,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-ethernet-generic_frame.ads
Original file line number Diff line number Diff line change
Expand Up @@ -611,7 +611,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
7 changes: 5 additions & 2 deletions generated/rflx-generic_types.ads
Original file line number Diff line number Diff line change
Expand Up @@ -35,13 +35,16 @@ package RFLX.Generic_Types is
function Last_Bit_Index (Idx : Index) return Bit_Index is
((Bit_Length (Idx) - 1) * 8 + 8);

function Bytes_First (Buffer : access constant Bytes) return Index is
-- WORKAROUND: Componolit/Workarounds#17
pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Bytes_First (Buffer : Bytes_Ptr) return Index is
(Buffer'First)
with
Pre =>
Buffer /= null and then Buffer'Length > 0;

function Bytes_Last (Buffer : access constant Bytes) return Index is
function Bytes_Last (Buffer : Bytes_Ptr) return Index is
(Buffer'Last)
with
Pre =>
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-ipv4-generic_option.ads
Original file line number Diff line number Diff line change
Expand Up @@ -471,7 +471,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-ipv4-generic_packet.ads
Original file line number Diff line number Diff line change
Expand Up @@ -1260,7 +1260,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-tlv-generic_message.ads
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
2 changes: 1 addition & 1 deletion generated/rflx-udp-generic_datagram.ads
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,7 @@ private

pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is
function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
((if Buffer /= null then
Buffer'First = Buffer_First
and Buffer'Last = Buffer_Last)
Expand Down
4 changes: 2 additions & 2 deletions rflx/generator/core.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@

from rflx import __version__
from rflx.ada import (
AccessParameter,
Annotate,
ArrayType,
Assignment,
Expand Down Expand Up @@ -1788,7 +1787,8 @@ def __create_valid_context_function(
[
Parameter(["Buffer_First", "Buffer_Last"], self.types.index),
Parameter(["First", "Last"], self.types.bit_index),
AccessParameter(["Buffer"], self.types.bytes, constant=True),
# WORKAROUND: Componolit/Workarounds#17
Parameter(["Buffer"], self.types.bytes_ptr),
Parameter(["Cursors"], "Field_Cursors"),
],
)
Expand Down
7 changes: 5 additions & 2 deletions rflx/templates/generic_types.ads
Original file line number Diff line number Diff line change
Expand Up @@ -35,13 +35,16 @@ package {prefix}Generic_Types is
function Last_Bit_Index (Idx : Index) return Bit_Index is
((Bit_Length (Idx) - 1) * 8 + 8);

function Bytes_First (Buffer : access constant Bytes) return Index is
-- WORKAROUND: Componolit/Workarounds#17
pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");

function Bytes_First (Buffer : Bytes_Ptr) return Index is
(Buffer'First)
with
Pre =>
Buffer /= null and then Buffer'Length > 0;

function Bytes_Last (Buffer : access constant Bytes) return Index is
function Bytes_Last (Buffer : Bytes_Ptr) return Index is
(Buffer'Last)
with
Pre =>
Expand Down

0 comments on commit 2915cbc

Please sign in to comment.