I get the following log when I am trying to apply Eva plugin to a C project.
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
53 functions analyzed (out of 9107): 0% coverage.
In these functions, 5300 statements reached (out of 14354): 36% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 15 warnings
by the Frama-C kernel: 0 errors 2 warnings
----------------------------------------------------------------------------
45 alarms generated by the analysis:
29 invalid memory accesses
4 accesses out of bounds index
6 invalid shifts
1 access to uninitialized left-values
5 others
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 1113 valid 18 unknown 1 invalid 1132 total
Preconditions 0 valid 0 unknown 0 invalid 0 total
98% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
Frama-C aborted the analysis after providing the analysis summary. However, it does not point out which file and which line of code that has a problem. Could you please let me know which are possible problems in this case? And is the analysis finished?
As the header of the line indicates, the message is not emitted by Eva, but by Frama-C's kernel. This error indicates that your code is violating CERT C Coding Standard, and more specifically its rule MSC-38 which basically states that it is a bad idea to declare identifiers that belong to the standard library, where they are specified as being potentially implemented as a macro. This notably includes assert and errno.
As this rule indicates that the code is not strictly ISO-C compliant, it has been decided to treat it by default as an error, but given the fact that the issue by itself is unlikely to make the analyzers crash, Frama-C does not abort as soon as it is triggered. This is why you can still launch Eva, which runs flawlessly, before being reminded by the kernel that there is an issue in your code (a first message, with Warning status, was likely output at the beginning of the log).
You can modify the severity status of CERT:MSC:38 using -kernel-warn-key CERT:MSC:38=<status>, where <status> can range from inactive (completely ignored) to abort (emit an error and abort immediately). The complete list of statuses can be found on section 6.2 of the user manual.