Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #87
Closed
Open
Issue created Aug 13, 2019 by mantis-gitlab-migration@mantis-gitlab-migration

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

Attachments

  • bug.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking