0002471: frama-c/wp generates invalid why3 - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002471

Frama-C

Plug-in > wp

public

2019-08-13 18:54

Reporter

abakst

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

always

Status

assigned

Resolution

open

Platform

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

Issue History
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

Relationships

Notes
There are no notes attached to this issue.