--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Queries regarding WP plugin



The exact commands and outputs are as follows:
1. frama-c -wp-print test.c. Output: [kernel] preprocessing with "gcc -C -E
-I.  test.c"
2. frama-c -wp-out wptest test.c. Output: same. wptest is a directory and
after the execution of this command it contains nothing.
3. frama-c -wp-gen test.c. Output: again same.
4. frama-c -wp test.c.
output: [kernel] preprocessing with "gcc -C -E -I.  test.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_main_assert_P : Valid

Please help me to get the proof obligations. I know the gui is not being
installed. But by default gui is enabled according to the configuration
help. I tried using ./configure --enable-gui as well. Then also it is
showing some warnings. The configuration log is attached herewith. Where am
I doing wrong?



Debasmita Lohar
MS Student
Computer Science and Engineering
IIT Kharagpur


On Fri, Dec 12, 2014 at 1:08 PM, David MENTRE <dmentre at linux-france.org>
wrote:
>
> Hello,
>
> Le 12/12/2014 07:10, Debasmita Lohar a ?crit :
>
>> These options were not showing the proof obligations.
>>
>
> What is the exact command you are using and the resulting error message?
>
> The rule on this list is to give a precise example of the faced issue.
>
>  I found that the
>> configuration had some warnings.
>>
>
> The config.log is quite explicit about what is missing. You don't have the
> GUI but otherwise your installation is fine.
>
> """
> configure:9048: WARNING: ltl2ba not found.
> configure:9072: WARNING: aorai partially enabled because ltl2ba missing.
> configure:9084: WARNING: /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa not
> found.
> configure:9098: WARNING: gui disabled because
> /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa missing.
> configure:9098: WARNING: gui disabled because
> /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa missing.
> configure:2418: WARNING: security_slicing disabled because gui not enabled.
> configure:2450: WARNING: impact only partially enabled because gui not
> enabled.
> configure:2450: WARNING: metrics only partially enabled because gui not
> enabled.
> configure:2450: WARNING: occurrence only partially enabled because gui not
> enabled.
> configure:2450: WARNING: scope only partially enabled because gui not
> enabled.
> configure:2450: WARNING: slicing only partially enabled because gui not
> enabled.
> configure:2450: WARNING: syntactic_callgraph only partially enabled
> because gui not enabled.
> configure:2450: WARNING: value_analysis only partially enabled because gui
> not enabled.
> configure:2450: WARNING: wp only partially enabled because gui not enabled.
> """
>
> Best regards,
> david
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141215/524d862f/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: config.log
Type: text/x-log
Size: 21926 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141215/524d862f/attachment-0001.bin>