--- layout: fc_discuss_archives title: Message 17 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



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