Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
F
frama-c
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 202
    • Issues 202
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #91

Closed
Open
Opened Jan 30, 2020 by mantis-gitlab-migration@mantis-gitlab-migration

quantifiers over logic types do not restrict to valid instances

ID0002497: This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002497 Frama-C Plug-in > wp public 2020-01-30 2020-02-03
Reporter amosr Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C 20-Calcium Target Version - Fixed in Version -

Description :

Hi,

When I quantify over an unsigned char, the resulting formula uses the is_uint8 predicate to ensure that it only considers valid uint8s. However, if I define a logic type that contains an unsigned char, there is no corresponding is_ predicate for the logic type:

//@ type logic_type_with_u8 = value(unsigned char);

This type is represented in the generated formula as an unbounded int rather than an unsigned char. This means that quantifying over the logic type includes more values than are allowed - for example, \forall logic_type_with_u8 l has to prove that the predicate is true even for values that won't fit in a u8.

As a concrete example, I expect the following to hold, but it does not:

lemma u8_is_valid: \forall logic_type_with_u8 n; \exists unsigned char u; n == value(u);

Thanks, Amos

Additional Information :

PS. I could not test on the latest version from git - how do I get (read-only) access to the git repository?

Steps To Reproduce :

Download file logic_type_is_valid.c and run with WP:

frama-c -wp logic_type_is_valid.c

The lemma in this file should hold, but does not.

Attachments

  • logic_type_is_valid.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: pub/frama-c#91