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] Can't import the whole project

  • Subject: [Frama-c-discuss] Can't import the whole project
  • From: Andre.MARONEZE at cea.fr (Andre Maroneze)
  • Date: Fri, 8 Mar 2019 10:05:42 +0100
  • In-reply-to: <54438_1552035680_5C822F60_54438_12081_1_c790405d-d0ee-5b6b-67a0-6c72cde89137@cea.fr>
  • References: <2d173506.9c2e.1695c61c7f6.Coremail.newbieroc@163.com> <54438_1552035680_5C822F60_54438_12081_1_c790405d-d0ee-5b6b-67a0-6c72cde89137@cea.fr>
By the way, my recommended way to use Frama-C for large projects is the 
following:

1. Use the command-line for preprocessing and parsing, giving all files 
and parsing-related options, then adding "-save framac.sav" (or 
something similar) at the end; this will usually fail at first for large 
projects, so fixing everything in the command-line is faster;

2. Then run Frama-C again (either command-line or GUI), starting with 
"-load framac.sav" before running the analyses/plugins. If you forget 
the "-load", you may get the error message you mentioned.


On 08/03/2019 10:00, Andre Maroneze wrote:
>
> Please be specific on your questions, it helps us to understand 
> exactly what is going on and save time.
>
> "import the whole project" - there is no "import" option in the 
> Frama-C GUI. In the File menu, there are "Source files", "Load 
> session", etc. The first will open a file selector for C source files, 
> the second will open a Frama-C saved file (there is no preferred 
> extension for these files, but typical usage is ".sav").
>
> The error message you mention is a typical symptom of giving Frama-C a 
> save file without option -load, which means the file will be 
> considered as a source file, then given to gcc for preprocessing, 
> which will not recognize it, by default assume it must be a linker 
> input file, and emit the warning. But it comes from the preprocessing, 
> which is then passed on to Frama-C.
>
> Ideally, trying to perform the operations with the command-line 
> version of Frama-C is easier to understand because then we can have 
> the exact commands to reproduce them, and more complete error 
> messages. If not possible, at least please try to describe in as much 
> detail as possible the operations performed on the GUI, which speeds 
> up understanding and resolution.
>
>
> On 08/03/2019 09:18, newbieroc wrote:
>> Hi,
>>   When I try to import the whole project from frama-c-gui, it reports 
>> a warning:
>>         linker input file unused because linking not done.
>>   Shall I input files of the project single by single? But it has so 
>> many files. Or, does it have other sollutions?
>>
>> Best regards.
>> newbieroc
>>
>>
>>
>> _______________________________________________
>> 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
>
> _______________________________________________
> 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/20190308/6ea57c45/attachment.html>