frama-c/wp generates invalid why3
ID0002471: This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0002471 | Frama-C | Plug-in > wp | public | 2019-08-13 | 2020-02-17 |
Reporter | abakst | Assigned To | correnson | Resolution | fixed |
Priority | normal | Severity | major | Reproducibility | always |
Platform | - | OS | macOS | OS Version | 10.14 |
Product Version | Frama-C 19-Potassium | Target Version | - | Fixed in Version | Frama-C 20-Calcium |
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
.
/*@ 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
$ 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