Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assumes got status invalid

According to the chosen command-line options, Eva may emit some verbose 
messages which are not warnings and are usually not a major concern for 
users, except when debugging or trying to understand precisely what is 
going on during the evaluation. Note that the message you displayed does 
not begin with "Warning" (although some very similar messages are 
emitted as warnings, in which case they do warrant special attention).

During evaluation, Eva will consider each behavior of a function 
separately, even if it seems obvious to the user that a given behavior 
will not be activated (for instance, if your tz argument is always NULL, 
then the tz_not_null behavior will not be active). That message is just 
a verbose way of saying "this behavior is not being considered because 
its precondition is false". In the cases where such an invalid status is 
likely wrong (e.g. in a `requires` clause), Eva will report it as a 
warning/error.

I'd recommend using Eva with the 3-step approach mentioned here: 
http://blog.frama-c.com/index.php?post/2018/01/25/Analysis-scripts%3A-helping-automate-case-studies

It's a long series of posts, but the overall idea is to:
- Parse the source files, save the result to a Frama-C file (-save);
- Load the previous result in the command line (-load), run Eva, save 
its analysis to another file;
- Load the previous result in the GUI, look at the "Messages" tab to see 
what warnings were emitted, then look at the "Properties" tab to see 
which properties are unknown/invalid, and work from there.

Messages emitted in the command-line which do not show either as 
warnings (Messages tab) or as unproven alarms (Properties tab) are 
mostly for informative purposes, and rarely a concern in large case studies.

The unreachability of your impact pragma must come from some other part 
of the analysis which needs to be stubbed or refined. Note that when 
analyzing applications based on command-line inputs (i.e., using 
argc/argv), the initial state considered by Eva is very restrictive, and 
a small stub is often necessary to obtain a more representative 
analysis. An example of such a stub is present at the end of the 
following file: 
https://github.com/Frama-C/open-source-case-studies/blob/master/solitaire/solitaire.c 
, in function `eva_main`, which would then be used by adding `-main 
eva_main` to the command line.

On 16/07/18 12:34, Divya Muthukumaran wrote:
> Hello,
>
> While performing impact analysis on nginx, I get a result saying that 
> the function where I have the impact pragma *ngx_alloc* is 
> unreachable. So I looked at the output and see lots of `got status 
> invalid` messages for preconditions. This is the first one of those 
> messages.
>
> [value] src/core/ngx_times.c:91:
>
> function gettimeofday, behavior tz_not_null: assumes got status 
> invalid; behavior not evaluated
>
>
> When I look inside frama-c/libc/sys/time.h I see four behaviours 
> defined for the `getttimeofday` functions which should be the complete 
> specification for the `tz` and `tv` values, so I don't understand what 
> `assumes got invalid` here means. Could you please explain this? 
> Hopefully, this will also help me understand the others that follow.
>
> Thanks,
> Divya
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/LIST
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180717/f46ed7a8/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180717/f46ed7a8/attachment.bin>