--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin



Hello,

> "WHYLIB" is neither internal nor external command, not an executable program or not a batch file.
> make: *** [simplify/max_why.sx] Error 1
> Jessie subprocess failed: make -f max.makefile simplify

What is your platform, and what does "make -v" say?

When you typed "Frama-c -jessie -jessie-atp simplify Jessie/max.c, it
generated a Makefile in file max.makefile that contains:

simplify/%_why.sx: why/%.why
        @echo 'why -simplify [...] why/$*.why' && $(WHY)
$(JESSIELIBFILES) why/$*.why

and above that, at the beginning of the file, there is (on my computer):

WHYLIB ?= /usr/local/Frama-C_Be/lib/why

WHY=WHYLIB=$(WHYLIB) $(WHYEXEC) $(WHYOPT)  -split-user-conj -explain
-locs max.loc

One possibility is that "make" is confused somewhere in the
interpretation of these lines.

Pascal