Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:40 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002471Frama-CPlug-in > wppublic2019-08-13 18:542020-02-17 18:08
Reporterabakst 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSmacOSOS Version10.14
Product VersionFrama-C 19-Potassium 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002471: frama-c/wp generates invalid why3
DescriptionThere 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 ReproduceCopy the C source into a new file, simple.c, and attempt to run the command:

frama-c -wp -wp-prover z3-ce simple.c
TagsNo tags attached.
Attached Files
  • c file icon bug.c (191 bytes) 2019-09-30 17:21 - 
    /*@ axiomatic maps { 
      type model_digit = octet | sextet; 
      logic integer foo(model_digit i); 
    } 
*/ 

int foo() 
{ 
  //@assert \forall int i; i == foo(octet); 
  return 0; 
}
    c file icon bug.c (191 bytes) 2019-09-30 17:21 +

-Relationships
+Relationships

-Notes

~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

~0006940

signoles (manager)

2020-02-17 18:08

 Fixed in Frama-C 20.0 (Calcium).
+Notes

-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
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
2020-02-17 18:06 signoles Fixed in Version => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006940
+Issue History