Anonymous | Login | Signup for a new account | 2019-12-16 06:03 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
0002471 | Frama-C | Plug-in > wp | public | 2019-08-13 18:54 | 2019-10-17 14:29 | ||||
Reporter | abakst | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | resolved | Resolution | fixed | ||||||
Platform | OS | macOS | OS Version | 10.14 | |||||
Product Version | Frama-C 19-Potassium | ||||||||
Target Version | Fixed in Version | ||||||||
Summary | 0002471: frama-c/wp generates invalid why3 | ||||||||
Description | There appears to be an issue with some of the `why3` files that get generated from user axiomatic definitions. I've installed `frama-c` using the `nix-pkgs` on the master branch, and hence have version `19.0`, and `why3` version `1.2.0`. ```c /*@ axiomatic maps { type model_digit = octet | sextet; logic integer foo(model_digit i); } */ int foo() { //@assert \forall int i; i == foo(octet); return 0; } ``` Given the (silly) program above in `simple.c`, I get the following behavior ```bash $ frama-c -wp -wp-prover z3-ce simple.c [kernel] Parsing simple.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] WPOUT/typed/A_maps.why:13: User Error: why3 syntax error [wp] [z3-ce] Goal typed_foo_assert : Failed why3 syntax error [wp] Proved goals: 0 / 1 Why3 (z3-ce): 0 (failed: 1) [wp] User Error: Deferred error message was emitted during execution. See above messages for more information. [kernel] Plug-in wp aborted: invalid user input. ``` The A_maps.why file contains: ``` (* ---------------------------------------------------------- *) (* --- Axiomatic 'maps' --- *) (* ---------------------------------------------------------- *) theory A_maps use bool.Bool use int.Int use int.ComputerDivision use real.RealInfix use Qed.Qed use int.Abs as IAbs use map.Map type a_model_digit | c_octet | c_sextet function l_foo a_model_digit : int end ``` The error seems to be on the line (I'd imagine there should be an '=' but I am not a why3 user) ``` type a_model_digit | c_octet | c_sextet ``` | ||||||||
Steps To Reproduce | Copy the C source into a new file, simple.c, and attempt to run the command: frama-c -wp -wp-prover z3-ce simple.c | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0006875) abakst (reporter) 2019-09-30 17:21 |
Forgive the lousy formatting above. The bug can be reproduced by running e.g. frama-c -wp -wp-prover z3 bug.c. |
(0006882) correnson (manager) 2019-10-17 14:28 |
Solved in next Frama-C released. |
(0006883) correnson (manager) 2019-10-17 14:29 |
New why-3 output, fixed coq output |
![]() |
|||
Date Modified | Username | Field | Change |
2019-08-13 18:54 | abakst | New Issue | |
2019-08-13 18:54 | abakst | Status | new => assigned |
2019-08-13 18:54 | abakst | Assigned To | => correnson |
2019-09-30 17:21 | abakst | File Added: bug.c | |
2019-09-30 17:21 | abakst | Note Added: 0006875 | |
2019-10-17 14:28 | correnson | Note Added: 0006882 | |
2019-10-17 14:29 | correnson | Note Added: 0006883 | |
2019-10-17 14:29 | correnson | Status | assigned => resolved |
2019-10-17 14:29 | correnson | Resolution | open => fixed |
Copyright © 2000 - 2019 MantisBT Team |