search

Stevendeo / Pilat

Invariant generator for polynomial loops
GNU Lesser General Public License v2.1
8 stars 2 forks source link

V1.2 and 1.3 have bug for missing the parameter -pilat? #6

Closed TaihuLight closed 2 years ago

TaihuLight commented 4 years ago

@Stevendeo @vprevosto After I install Pilat V1.2 and V1.3 by executing 

opam install pilat

-pilat is missed, where the error is shown as follow.

[kernel] User Error: option `-pilat' is unknown.
  use `frama-c -help' for more information.
[kernel] Frama-C aborted: invalid user input.

Thus, the installed pilat v1.2 and v1.3 can not activate pilat plugin and generate loop invariant!

Stevendeo commented 4 years ago

Hello @TaihuLight The pilat plug-in is activated with the option -pilat-degree n with n the polynomial degree of the invariants you are trying to generate. You may find the list of pilat options with the command frama-c -pilat-h. More generally, you can find help on any Frama-C plugin with the command frama-c -plugin_name-h. Let me know if you still have troubles with Pilat.

TaihuLight commented 4 years ago

@Stevendeo Thank you. I have solved the problem with your help. However, I think there is a bug for the tip of the option -pilat-degree n . It only suggest that "sets the maximum degree of the invariants". It dose not suggest that "when on, generates polynomial invariants for each solvable loop of the program" as the original option -pilat dose. Thus, users hard to get the fact that activating the pilat plug-in with the option -pilat-degree n.

Stevendeo commented 2 years ago

I forgot to answer, but I added a -pilat option for activating the plug-in so as to make the plug-in usage consistent with the other plug-ins. Closing this issue.