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

[Frama-c-discuss] three newbie questions



>
> I have a program that generates ~200 VC. Most of them are proved by
> Alt-Ergo, but none of them by Simplify. I see the "tool problem" icon on
> each VC. I ran why-config and it detected Simplify. I was able to use
> Simplify with previous versions of Frama-C/Jessie. Maybe there's a bug
> in the toolchain or the makefile. I use Boron on Ubuntu 10.
>
>
> ? ?prover ? ? ?version ? ? ? ? ? ? ?info ? invocation
> ------------------------------------------------------
> ?Alt-Ergo ? ? ? ? 0.91 ? (not supported) ? alt-ergo
> ?Simplify ? ? ? ?1.5.4 ? ? ? ? ? ? ? ? ? ? simplify

I have similar symptoms on Mac OS X Leopard and Snow Leopard (and I
did run why-config).
Launching Simplify myself gives a prompt (in which I do not know what
to type to check further that it is correctly installed).

Pascal