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