--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on December 2014 ---
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>