Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #410

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