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] Partial verification

  • Subject: [Frama-c-discuss] Partial verification
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Mon, 07 Nov 2011 10:10:04 +0100
  • In-reply-to: <CAC3Lx=ZOsJW=dizHx65nOve=3-rVdcy5Ff9Np-_BgJeM1EmwEA@mail.gmail.com>
  • References: <mailman.23.1320577268.22447.frama-c-discuss@lists.gforge.inria.fr> <952CD441-A699-4FB0-B725-E67977153ED7@gemalto.com> <CAC3Lx=ZOsJW=dizHx65nOve=3-rVdcy5Ff9Np-_BgJeM1EmwEA@mail.gmail.com>
Hello David and Maria,

On 06/11/2011 12:44, David MENTRE wrote:
> 2011/11/6 Christofi Maria<Maria.Christofi at gemalto.com>:
>> but, I meant without using GUI. Is there any option to use with the command?
>
> Using a combination of -lib-entry and -main? Something like "frama-c
> -lib-entry -main max".
>
> -lib-entry          run analysis for an incomplete application e.g. an API
>                      call. See the -main option to set the entry point name
> -main<f>            set to name the entry point for analysis. Use -lib-entry
>                      if this is not for a complete application. Defaults to
>                      main

-lib-entry and -main won't help here. jessie performs a modular 
analysis. Basically, each function is analyzed separately, independently 
from the contexts in which it might be called starting from the entry 
point of the program. The options you mention are mainly useful for a 
global analysis (as performed e.g. by the value analysis plugin).
The only thing that Jessie could do (it does not as far I know) with 
-main f and without -lib-entry would be to produce extra hypotheses in 
proof obligations related to f stating that the globals have their 
initial value when entering the function.

Now back to the initial problem: there is no easy way to do that with 
jessie outside of the GUI (and even that won't do exactly what you want: 
the goals are still generated, the GUI just lets you choose to launch a 
prover over them or not). A possibility would be to remove the functions 
you don't want to consider, either through #ifdef or through a copy 
visitor in Frama-C that would create a new project by erasing the 
globals that you don't want.

On the other hand, you can have a look at the WP plugin whose -wp-fct 
option does exactly what you want.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile