Dialyzer

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Dialyzer

Schneider-3
Dear lsit,

I have the following function plus specification:

-spec new(Seq_nums, DDS_filter) -> Cfrs when
       Seq_nums :: nonempty_list(rtps:sequence_number()),
       DDS_filter :: fun((rtps:sequence_number()) -> boolean()),
       Cfrs :: nonempty_list(cfr()).

new(Seq_nums, DDS_filter) ->
     [#cfr{sequence_number = N, status = unsent,
           is_relevant = not DDS_filter(N)}
      || N <- Seq_nums].

Dialyzer complains with:

Invalid type specification for function rtps_cfr:new/2. The success
typing is ([],_) -> []

The filter is an external function,
What is wrong with the spec?

TIA

Frans
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer

Fred Hebert-2
On 01/20, Frans Schneider wrote:

>Dear lsit,
>
>I have the following function plus specification:
>
>-spec new(Seq_nums, DDS_filter) -> Cfrs when
>      Seq_nums :: nonempty_list(rtps:sequence_number()),
>      DDS_filter :: fun((rtps:sequence_number()) -> boolean()),
>      Cfrs :: nonempty_list(cfr()).
>
>new(Seq_nums, DDS_filter) ->
>    [#cfr{sequence_number = N, status = unsent,
>          is_relevant = not DDS_filter(N)}
>     || N <- Seq_nums].
>
>Dialyzer complains with:
>
>Invalid type specification for function rtps_cfr:new/2. The success
>typing is ([],_) -> []
>
>The filter is an external function,
>What is wrong with the spec?
>

You should look at the call-site. There's a possibility that the only
places that call the function use arguments that are lists of terms that
don't match the sequence number type. In doing so, dialyzer "removes"
the types with these as crashing (i.e. DDS_filter would raise an
exception).

What is left is the set of empty lists (once all the filters are done)
which only gives ([],_) -> []

That's at least my guess without seeing the calling code.
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer

Schneider-3
Yep, it were the nonempty lists which caused the problem. I used
nonempty because _I_ know that the function never is called with an
empty list, but that is not relevant for the specs of the function.

On 1/20/19 5:34 PM, Fred Hebert wrote:

> On 01/20, Frans Schneider wrote:
>> Dear lsit,
>>
>> I have the following function plus specification:
>>
>> -spec new(Seq_nums, DDS_filter) -> Cfrs when
>>      Seq_nums :: nonempty_list(rtps:sequence_number()),
>>      DDS_filter :: fun((rtps:sequence_number()) -> boolean()),
>>      Cfrs :: nonempty_list(cfr()).
>>
>> new(Seq_nums, DDS_filter) ->
>>    [#cfr{sequence_number = N, status = unsent,
>>          is_relevant = not DDS_filter(N)}
>>     || N <- Seq_nums].
>>
>> Dialyzer complains with:
>>
>> Invalid type specification for function rtps_cfr:new/2. The success
>> typing is ([],_) -> []
>>
>> The filter is an external function,
>> What is wrong with the spec?
>>
>
> You should look at the call-site. There's a possibility that the only
> places that call the function use arguments that are lists of terms that
> don't match the sequence number type. In doing so, dialyzer "removes"
> the types with these as crashing (i.e. DDS_filter would raise an
> exception).
>
> What is left is the set of empty lists (once all the filters are done)
> which only gives ([],_) -> []
>
> That's at least my guess without seeing the calling code.
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer

Stavros Aronis
On Sun, Jan 20, 2019 at 6:31 PM Frans Schneider <[hidden email]> wrote:
>
> Yep, it were the nonempty lists which caused the problem. I used
> nonempty because _I_ know that the function never is called with an
> empty list, but that is not relevant for the specs of the function.

Good, but this is not what Fred pointed out!

It is likely that this function is *never* called with values that
satisfy the specified type for `Seq_nums`, either because the calls
themselves are bad (not likely if the code is working) or because the
type definition for `Seq_nums` is wrong.

By removing the 'nonempty', you're **silencing** the warning that the
only way for the function to succeed as specified, is if passed an
empty list.

> On 1/20/19 5:34 PM, Fred Hebert wrote:
> > On 01/20, Frans Schneider wrote:
> >> Dear lsit,
> >>
> >> I have the following function plus specification:
> >>
> >> -spec new(Seq_nums, DDS_filter) -> Cfrs when
> >>      Seq_nums :: nonempty_list(rtps:sequence_number()),
> >>      DDS_filter :: fun((rtps:sequence_number()) -> boolean()),
> >>      Cfrs :: nonempty_list(cfr()).
> >>
> >> new(Seq_nums, DDS_filter) ->
> >>    [#cfr{sequence_number = N, status = unsent,
> >>          is_relevant = not DDS_filter(N)}
> >>     || N <- Seq_nums].
> >>
> >> Dialyzer complains with:
> >>
> >> Invalid type specification for function rtps_cfr:new/2. The success
> >> typing is ([],_) -> []
> >>
> >> The filter is an external function,
> >> What is wrong with the spec?
> >>
> >
> > You should look at the call-site. There's a possibility that the only
> > places that call the function use arguments that are lists of terms that
> > don't match the sequence number type. In doing so, dialyzer "removes"
> > the types with these as crashing (i.e. DDS_filter would raise an
> > exception).
> >
> > What is left is the set of empty lists (once all the filters are done)
> > which only gives ([],_) -> []
> >
> > That's at least my guess without seeing the calling code.
> _______________________________________________
> erlang-questions mailing list
> [hidden email]
> http://erlang.org/mailman/listinfo/erlang-questions
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions