Skip to content

GitLab

  • Menu
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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #410

Closed
Open
Created Aug 08, 2016 by mantis-gitlab-migration@mantis-gitlab-migration

Logic with read clauses can have their values invalidated by writes to separated memory locations

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


Id Project Category View Due Date Updated
ID0002244 Frama-C Plug-in > wp public 2016-08-08 2016-08-08
Reporter jrobbins Assigned To correnson Resolution open
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Aluminium Target Version - Fixed in Version -

Description :

In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.

Additional Information :

This bug is present on both Frama-C versions Sodium and Aluminum.

Steps To Reproduce :

== File bug.c: /*@ axiomatic Axiomatic { logic boolean property_of_buffer(char *buffer) reads *buffer; } */

/*@ assigns *buffer; ensures property_of_buffer(buffer); */ void foo(char *buffer);

/*@ requires property_of_buffer(buffer); assigns *buffer; ensures property_of_buffer(buffer); */ int bar(char *buffer);

char buf1[1]; char buf2[1];

void main() { foo(buf1); bar(buf1);

foo(buf2);
bar(buf1);

} == Command to run: frama-c -wp bug.c == Output: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing bug.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 2 goals scheduled [wp] [Qed] Goal typed_main_call_bar_pre : Valid [wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms) [wp] Proved goals: 1 / 2 Qed: 1 alt-ergo: 0 (unknown: 1) == Expected behavior: For typed_main_call_bar_pre_2 to prove valid.

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